# Circuit satisfiability and constraint satisfaction around Skolem Arithmetic

@article{Glaer2017CircuitSA, title={Circuit satisfiability and constraint satisfaction around Skolem Arithmetic}, author={Christian Gla{\ss}er and Peter Jonsson and Barnaby Martin}, journal={Theor. Comput. Sci.}, year={2017}, volume={703}, pages={18-36} }

Abstract We study interactions between Skolem Arithmetic and certain classes of Circuit Satisfiability and Constraint Satisfaction Problems (CSPs). We revisit results of Glaser et al. [1] in the context of CSPs and settle the major open question from that paper, finding a certain satisfiability problem on circuits—involving complement, intersection, union and multiplication—to be decidable. This we prove using the decidability of Skolem Arithmetic. Then we solve a second question left open in… Expand

#### Tables and Topics from this paper

#### 7 Citations

Emptiness problems for integer circuits

- Computer Science, Mathematics
- Theor. Comput. Sci.
- 2020

It turns out that the following problems are equivalent to PIT, which shows that the challenge to improve their bounds is just a reformulation of a well-studied, major open problem in algebraic computing complexity. Expand

Emptiness Problems for Integer Circuits

- Mathematics, Computer Science
- MFCS
- 2017

It turns out that the following problems are equivalent to PIT, which shows that the challenge to improve their bounds is just a reformulation of a major open problem in algebraic computing complexity. Expand

Balance problems for integer circuits

- Computer Science, Mathematics
- Theor. Comput. Sci.
- 2019

The work shows that the balance problem for { ∖, ⋅ } -circuits is undecidable which is the first natural problem for integer circuits or related constraint satisfaction problems that admits only one arithmetic operation and is proven to be Undecidable. Expand

Balance Problems for Integer Circuits

- Computer Science, Mathematics
- Electron. Colloquium Comput. Complex.
- 2018

The work shows that the balance problem for {−, ·}-circuits is undecidable which is the first natural problem for integer circuits or related constraint satisfaction problems that admits only one arithmetic operation and is proven to be Undecidable. Expand

Constraint Satisfaction Problems over Numeric Domains

- Computer Science
- The Constraint Satisfaction Problem
- 2017

A survey of complexity results for constraint satisfaction problems (CSPs) over the integers, the rationals, the reals, and the complex numbers is presented, to identify those CSPs that can be solved in polynomial time, and to distinguish them from C SPs that are NP-hard. Expand

Discrete Mutation Hopfield Neural Network in Propositional Satisfiability

- Computer Science
- 2019

This study provides a new paradigm in the field of neural networks by overcoming the overfitting issue and presents an integrated representation of k-satisfiability (kSAT) in a mutation hopfield neural network (MHNN). Expand

Systematic Boolean Satisfiability Programming in Radial Basis Function Neural Network

- Computer Science
- 2020

A comprehensive investigation of the potential effect of systematic Satisfiability programming as a logical rule, namely 2 Satisfiability (2SAT) to optimize the output weights and parameters in RBFNN and provides a new paradigm in the field feed-forward neural network by implementing a more systematic propositional logic rule. Expand

#### References

SHOWING 1-10 OF 60 REFERENCES

Emptiness Problems for Integer Circuits

- Mathematics, Computer Science
- MFCS
- 2017

It turns out that the following problems are equivalent to PIT, which shows that the challenge to improve their bounds is just a reformulation of a major open problem in algebraic computing complexity. Expand

Satisfiability of Algebraic Circuits over Sets of Natural Numbers

- Mathematics, Computer Science
- FSTTCS
- 2007

It is proved that testing satisfiability for {∩, +, ×}- circuits already is undecidable, and that in several cases, satisfiability problems are harder than membership problems. Expand

Satisfiability of algebraic circuits over sets of natural numbers

- Computer Science, Mathematics
- Discret. Appl. Math.
- 2010

This work proves that testing satisfiability for {@?,+,x}-circuits is already undecidable, and shows that satisfiability problems capture a wide range of complexity classes such as NL, P, NP, PSPACE, and beyond. Expand

Constraint Satisfaction Problem Dichotomy for Finite Templates: a Proof Via Consistency Checks

- Computer Science, Mathematics
- 2017

This article presents a proof of the Dichotomy Conjecture via local consistency and AF- consistency checks and shows that, for every Taylor domain, the original instance of the CSP is solvable if, and only if, the problem has a solution in one of those subinstances. Expand

A Proof of CSP Dichotomy Conjecture

- Computer Science, Mathematics
- 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS)
- 2017

An algorithm is presented that solves Constraint Satisfaction Problem in polynomial time for constraint languages having a weak near unanimity polymorphism, which proves the remaining part of the conjecture. Expand

The complexity of satisfiability problems

- Computer Science, Mathematics
- STOC
- 1978

An infinite class of satisfiability problems is considered which contains these two particular problems as special cases, and it is shown that every member of this class is either polynomial-time decidable or NP-complete. Expand

Complexity of subcases of Presburger arithmetic

- Mathematics
- 1984

We consider formula subclasses of Presburger arithmetic which have a simple structure in one sense or the other and investigate their computational complexity. We also prove some results on the lower… Expand

Integer circuit evaluation is PSPACE-complete

- Mathematics, Computer Science
- Proceedings 15th Annual IEEE Conference on Computational Complexity
- 2000

A polynomial-time algorithm is shown that reduces QBP (quantified Boolean formula) problem to the integer circuit problem, which complements the result of K. Wagner (1984) to show that IC problem is PSPACEcomplete. Expand

A Dichotomy Theorem for Nonuniform CSPs

- Mathematics, Computer Science
- 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS)
- 2017

The Dichotomy Conjecture for the non-uniform CSP states that for every constraint language \Gm the problem CSP is either solvable in polynomial time or is NP-complete. Expand

Schaefer's Theorem for Graphs

- Computer Science, Mathematics
- J. ACM
- 2015

It is proved that either Ψ is contained in one out of 17 classes of graph formulas and the corresponding problem can be solved in polynomial time, or the problem is NP-complete. Expand