The 2024 Developer Survey results are live! See the results

# Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

115 questions
Filter by
Sorted by
Tagged with
1 vote
42 views

### Do stably-infinite theories exclude finite sorts?

Nelson-Oppen requires theories to be stably infinite. Meaning, that each theory allows extending models to have an infinite domain. A commonly mentioned counter example is that the theory of bit ...
18 views

### Finding a common variable value among all SAT solutions

Let $F$ be a boolean formula on $n$ variables $x_1, \cdots, x_n$. $\textbf{SAT}(F)$ asks whether there exists an assignment of truth values to variables under which $F$ is true. I'm curious about ...
1 vote
18 views

### Are there ASICs optimized to solve the SAT problem?

Are there ASICs (application-specific integrated circuits) optimized to solve the SAT problem, such as by the DPLL algorithm?
• 154
165 views

### SAT solvers for counting the number of solutions

Are there existing SAT solver libraries that can count the number of solutions of a boolean formula? Can you give examples? I mean implementations more efficient than the naive approach, i.e. each ...
1 vote
91 views

### Sat solvers with backdoor set

I have large cnf with thousands of variables, but with known compact backdoor set. I think this set can be used by CDCL solvers to choose assignment variables to simplify formula much faster, but I ...
1 vote
328 views

• 135
47 views

### Can you help me find some examples of 3co-SAT for 4 variables?

I've been studying the examples of 3co-SAT recently. It's easy to find an example of one variable. $(x_1\lor x_1\lor x_1)\land (\overline{x_1}\lor \overline{x_1}\lor \overline{x_1})$ Examples of 2 ...
• 315
142 views

### what does **input** mean for the $3SAT$ question? Is it the number of variables $n$ or the number of clauses $m$

We know that $3SAT \in NP$, and the definition of $NP$ is as follows: $NP$ is the class of languages that have polynomial time verifiers. But I have a question: what does input mean for the $3SAT$ ...
• 315
473 views

• 568
196 views

### CNF satisfiability with a bound on number of clauses

Consider the CNF-sat problem with n literals and k clauses. If k scales linearly in n, we get np-completeness (e.g., 3-sat where each literal appears at most 4 times). Do we still get np-completeness ...
• 131
1k views

### Practical hard 3-sat instances

The $3-SAT$ problem is known to be NP-complete problem. Which means that (as far as I understand), unless $P \neq NP$, for every algorithm $A$ which decides $3-SAT$, $A$ runs in super polynomial time (...
• 43
136 views

### Non-Boolean SAT

I was wondering about the complexity of SAT tests with variables $x_i = 0 \lor 1 \lor 2 \dots \lor n$, with clauses being of the form $x_i = a \implies x_j \neq b$. When $n=2$, we have 2SAT, which has ...
• 405
899 views

### Random restarts for unsatisfiable instances

In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice. ...
• 386
1 vote
186 views

### Can an optimization algorithm be "universal"?

I am wondering if a Bayesian Optimization framework (e.g. Google's Vizier) can be used in lieu of a traditional solver like Gurobi or CPLEX. In trying to answer this question, I realized that I don'...
347 views

### Sum of unique integers to cnf constraint

As a study project I try to solve the kakuro puzzle problem using SAT SOLVER. I can't really find an efficient way to convert the sum of k unique integers (1...9) to a CNF constraint. What I had in ...
• 209
1 vote
129 views

### Encoding a "not-k-out-of-n" constraint for SAT solvers

I'm finding myself needing to encode a "not-k-out-of-n" constraint in a SAT solver. The "at-most-k-out-of-n" constraint for SAT solvers is something I can find research about -- this paper by Frisch ...
• 203
278 views

### Determine if a graph has exactly 1 cycle using a SAT solver

I have a connected undirected graph whose edges are either enabled or disabled. I want to create a set of clauses that are SAT iff all enabled edges are part of a single loop. If I assert that each ...
70 views

### Is there a correspondence of steps between DPLL and sequent-calculus?

Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid? And given ...
• 273