# Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

12 questions
Filter by
Sorted by
Tagged with
7k views

### Encoding 1-out-of-n constraint for SAT solvers

I'm using a SAT solver to encode a problem, and as part of the SAT instance, I have boolean variables $x_1,x_2,\dots,x_n$ where it is intended that exactly one of these should be true and the rest ...
• 161k
1k views

### Recipe book for SAT encodings?

SAT solvers are getting more and more efficient in solving large instances and are being used as back-ends in various contexts. Every time one wants to use them to solve a problem in a specific domain,...
• 425
3k views

### When to use SAT vs Constraint Satisfaction?

If I have a hard problem, one standard approach is to express it as a SAT instance and try running a SAT solver on it. Another standard approach is to express it as a constraint satisfaction problem, ...
• 161k
4k views

### Proving that the conversion from CNF to DNF is NP-Hard

How can I prove that the conversion from CNF to DNF is NP-Hard? I'm not asking for an answer, just some suggestions about how to go about proving it.
• 311
265 views

### Convert $\sum x_i = y$ to 3-sat

I have a simple looking question. What is the most efficient conversion of $\sum_{i=1}^n x_i = y$ to 3-sat? Here $x_i$ is either $1$ or $0$ and $y$ is some positive integer. Can you do better than ...
• 996
2k views

### Best improvements to do to the DPLL SAT algorithm

As part of a college class, I'm asked to improve the performance of a basic DPLL sat solver. I'm already provided a basic, slow working version (essentially the DPLL algorithm; furthermore, to select ...
605 views

### Introduction into first order logic verification

I am trying to teach myself different approaches to software verification. I have read some articles. As far as I learned, propositional logic with temporal generally uses model checking with SAT ...
• 135
6k views

### Understanding DPLL algorithm

I'm trying to understand DPLL algorithm for solving SAT problem. And here it is: ...
1 vote
128 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
1 vote
2k views

### Is this possible to solve 3SAT in O(n^24) time and O(1) space?

Assume that n is the number variables of the given 3CNF formula (n≥3) and all clauses in the given 3CNF formula are different. That means that for each clause, each literal can be either positive ...
1 vote
143 views

### Logical formula in DIMACS, SAT, Schaefer's dichotomy theorem and software to test it

I have a very complicated formula logical (CNF) in the file DIMACS. The question is as follows. The formula has hundreds of millions of clauses (assume billion) and a lot of variables. It is a ...
• 239