Skip to main content

Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

Filter by
Sorted by
Tagged with
33 votes
3 answers

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 ...
D.W.'s user avatar
  • 161k
20 votes
3 answers

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,...
Bordaigorl's user avatar
19 votes
1 answer

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, ...
D.W.'s user avatar
  • 161k
21 votes
1 answer

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.
jkjk's user avatar
  • 311
6 votes
2 answers

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 ...
Simd's user avatar
  • 996
3 votes
2 answers

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 ...
user1843790's user avatar
10 votes
2 answers

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 ...
FELIPE N.'s user avatar
  • 135
6 votes
2 answers

Understanding DPLL algorithm

I'm trying to understand DPLL algorithm for solving SAT problem. And here it is: ...
Tikhon Belousko's user avatar
1 vote
1 answer

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 ...
onigame's user avatar
  • 203
1 vote
4 answers

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 ...
Farewell Stack Exchange's user avatar
1 vote
0 answers

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 ...
Aurelio's user avatar
  • 239
-2 votes
1 answer

How a SMT / SAT Solver Generates Valuations for this Example

First, an example of a set of constraints which turned out not to be solvable (I don't think): ...
Lance's user avatar
  • 2,243