Questions tagged [sat-solvers]
Questions regarding solver programs for the boolean satisfiability problem.
105
questions
32
votes
3
answers
6k
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 ...
D.W.♦
- 152k
21
votes
1
answer
680
views
Why do all recent SAT solvers work on CNF instead of circuit SAT?
After the release of the AIGER library to handle and-inverter graphs sometime in 2006 (I think), some circuit SAT solvers were released in 2006-2008, and in a few SAT Races/Competitions there were AIG ...
- 393
20
votes
1
answer
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.
- 301
19
votes
3
answers
966
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,...
- 415
19
votes
1
answer
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, ...
D.W.♦
- 152k
13
votes
3
answers
541
views
Multicore SAT Solver
I am trying to solve a 25k clauses 5k variables SAT problem. As it has been running for an hour (precosat) and I'd like to solve bigger ones afterwards, I'm looking for a multi-core SAT-Solver.
As ...
- 131
13
votes
1
answer
837
views
Unification vs. SAT solver
I read on Wikipedia that unification is a process of solving the satisfability problem.
At the same time, I know that such solvers are called "SAT solvers" or "SMT solvers". So, are they different ...
- 1
12
votes
4
answers
2k
views
Are there competitions for integer programming?
Are there competitions for integer programming like there are for SAT and MAXSAT?
- 326
11
votes
1
answer
847
views
Can top SAT-solvers factor easy numbers?
Modern SAT-solvers are very good at solving many real-world examples of SAT instances. However, we know how to generate hard ones: for instance use a reduction from factoring to SAT and give the RSA ...
- 4,792
9
votes
2
answers
552
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 ...
- 125
9
votes
1
answer
2k
views
Why the need for TSP solvers when there are SAT solvers?
Concorde TSP is a solver for TSP. SAT solvers are solvers for boolean satisfiability. TSP and SAT are NP-complete.
Hence, why spent the time to develop Concorde TSP when there is an abundance of SAT ...
- 93
9
votes
1
answer
1k
views
Conflict Driven Clause Learning backtracking clarification
On the wikipedia page here it describes pretty well the CDCL algorithm (and it seems the pictures were taken from slides created by Sharad Malik at Princeton). However when describing how to backtrack ...
- 3,760
8
votes
4
answers
768
views
Deterministic SAT solver
I have the following question. Is the SAT solvers are deterministic?
I mean, for example, about miniSAT and DPLL algorithm. Are they completely deterministic?
If these algorithms will return unSAT ...
- 81
8
votes
2
answers
226
views
Assignment to make formula unsatisfiable
Lets imagine we have a satisfiable formula $F(A_0, A_1,...A_k,S_0,...,S_n)$ The problem to solve is "Is there an assignment for variables $(S_0,...,S_n)$ which will make F unsatisfiable?". One way of ...
7
votes
1
answer
249
views
Framework or tools to generate theorem prover/solver/reasoner for new logic
I have new logic which has syntax and semantics in usual natural languages and I have to create theorem prover/solver/reasoner for this logic. Is there framework or tool set that can generate such ...
- 1,381
7
votes
2
answers
171
views
Common method for solving satisfiability problems which lie in P
I know from Schaefer's Dichotomy Theorem that only a few types of satisfiability problems are in P and any other problem is NP-complete. However, all of the algorithms I know for them use specific ...
- 1,601
7
votes
1
answer
824
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
7
votes
1
answer
283
views
How to use an old SAT solver to discover a new one, as is done in The Golden Ticket?
In Lance Fortnow's book The Golden Ticket, he mentions that once you have a polynomial-time algorithm for an NP-complete problem, you can use it to find a faster algorithm. Can you tell me how that is ...
- 940
7
votes
1
answer
2k
views
Why is pure literal elimination absent in DPLL-based algorithms like Chaff?
I'm looking into various SAT-solvers and trying to understand how they work and why they are designed in certain ways. (But I'm not in a university at the moment and I do not know anyone who is a ...
6
votes
2
answers
238
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 ...
- 860
6
votes
2
answers
5k
views
Understanding DPLL algorithm
I'm trying to understand DPLL algorithm for solving SAT problem. And here it is:
...
- 163
6
votes
2
answers
2k
views
Why don't modern SAT solvers use the notion of a "watched clause", in the same way they use the notion of a "watched literal"?
Modern SAT solvers use the notion of "watched literals": when a value is chosen for a literal $l$, the solver only checks whether that falsifies clauses with $l$ in them if $l$ is one of the watched ...
- 641
6
votes
1
answer
767
views
Why is DPLL better than brute force?
I understand that by being clever about the way we navigate the search space of the SAT problem we're going to get better performance than by randomly choosing and testing solutions, though of course ...
6
votes
2
answers
7k
views
Forward checking vs arc consistency on 3-SAT
If I were to let the variables be the propositions and, constraint be all clauses being satisfied, which technique would be more effective in solving 3-SAT? Forward checking or arc consistency? From ...
- 373
6
votes
1
answer
125
views
Why is this SAT problem hard and what can I do about it?
For a graph theory problem I need to solve hundreds of millions of CNF problems that typically have around 200 variables and 15,000 clauses no larger than 10.
By default I use glucose, which usually ...
- 161
6
votes
3
answers
299
views
Detection of redundant boolean constraints
I'm trying to solve a constraint programming problem using a SAT solver. I have set of constraints in the form of propositional logic statements, which are converted to CNF using Tseitin ...
- 327
5
votes
1
answer
1k
views
Running time of CDCL compared to DPLL
What's the complexity of Conflict-Driven Clause Learning SAT solvers, compared to DPLL solvers? Was it proven that CDCL is faster in general? Are there instances of SAT that are hard for CDCL but easy ...
- 53
5
votes
2
answers
1k
views
Are there any open source SAT solvers with UNSAT core extraction algorithm built in?
Just like the title says. I need to use a SAT solver on a series of CNF formulas but not only do I need an answer of the type satisfiable/unsatisfiable but also some subset of clauses whose ...
- 53
5
votes
0
answers
186
views
Introduction to bounded model checking that describes model generation
Most of the tutorials I have found on model checking and bounded model checking start with, the model is given as a Kripke Structure M = (S,I,T,L) where S is a set of states, I is a set of initial ...
4
votes
4
answers
586
views
How to Modify SAT Solvers to Produce Resolution Refutations for Unsatisfiable Instances?
In recent SAT competitions, there is a Certified UNSAT track. The problem instances are all unsatisfiable and the solvers are asked to produce certificates for unsatisfiability. One way is to produce ...
- 940
4
votes
1
answer
248
views
Solving SAT using tableau calculus
I've learned about tableau calculus which is a decision procedure solving the problem of satisfiability of a first order logic formula.
Now I'm wondering why this technique can't be used to solve the ...
- 143
4
votes
2
answers
388
views
Is it feasible to solve this subset cover problem with SAT solver?
The problem is to find $\mathcal{S}$, a minimal collect of subsets of $\{1,\dots, 17\}$ such that the two conditions are satisfied:
if $S \subseteq \mathcal{S}$ then $|S|=6$;
for any $A \subseteq \{1,...
- 559
4
votes
1
answer
782
views
What's the average number of clauses modern SAT solvers can handle?
It's already known that size doesn't matter always (for SAT problems).
But is there evidence (from real data from: benchmarks or real cases) on how many clauses an average SAT solver can handle ...
- 43
4
votes
1
answer
1k
views
Resolution complexity versus a constrained SAT algorithm
EDIT: ad hoc speed-ups are excluded.
We have the result that propositional resolution requires exponential time. The resolution result uses the proof of the pigeonhole principle as an example of a ...
- 911
4
votes
1
answer
325
views
What are efficient approaches to implement unit propagation in DPLL-based SAT solvers?
I'm trying to decompose deduction steps of DPLL algorithm -- unit propagation and pure literal elimination -- for parallelization. However, I want a baseline and asymptotic analysis to compare to my ...
- 43
4
votes
0
answers
28
views
Benchmark of SAT solvers on random k-SAT instances at satisfiability threshold
I am looking for a solid reference (peer-reviewed publication) on the design and/or benchmarking of SAT solvers for random k-SAT ($4 \leq k \leq 8$) operating at satisfiability threshold.
The majority ...
- 41
4
votes
0
answers
66
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 ...
- 263
4
votes
0
answers
195
views
Why Is Alloy not an Answer Set Programming system?
Alloy's front page doesn't mention ASP, but the description sounds like ASP (finding solutions consistent with a logical spec). And Alloy isn't listed in the Wikipedia ASP article. Yet ASP systems ...
- 153
3
votes
1
answer
266
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
3
votes
1
answer
602
views
How the Abstract DPLL Algorithm Works in SAT Solving
I have come across many definitions of the DPLL algorithm but haven't been able to follow them. The ones that are closest to making sense to me are the ones based on state-transition systems with ...
- 2,103
3
votes
1
answer
60
views
Stalmarck's method: x ≡ x → z, does z have to be true?
I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that:
y $\to$ z $\equiv$ x
where x, y and z are booleans which ...
- 53
3
votes
1
answer
48
views
How to leverage the fact that I'm solving 1000's of very similar SMT instances?
I have a core SMT solver problem consisting of 100,000 bit-vector array clauses, and one 10000-dimensional bit-vector array. Then, my program takes as input k << 100,000 new clauses, and adds ...
- 225
3
votes
1
answer
108
views
Clarification on "clause learning" in DPLL algorithm
I am struggling to understand the idea of conflict-driven clause learning, in particular, I can not understand why the clause we 'learned' is a substantially new (i.e. the clause database does not ...
- 687
3
votes
1
answer
559
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 (...
- 33
3
votes
1
answer
208
views
If a CNF contains only Horn and Xor clauses, then what is the complexity of determining Satisfiability?
If a CNF contains only Horn and Xor clauses, and does not contain clauses of other types, then can its Satisfiability be determined in polynomial time?
- 321
3
votes
1
answer
136
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
3
votes
2
answers
2k
views
CSP Forward checking with n-ary (and binary) constraints
I have implemented my own CSP solver using a Backtracking algorithm.
Within the Backtracking algorithm I apply a Forward Checking algorithm (reducing domains of connected, unnasigned variables) that ...
- 31
3
votes
1
answer
329
views
Detect non existence of a cycle in a graph using Datalog : SMTLIB Format for Z3
I want to detect the non existence of a cycle in a graph using Datalog (which is a declarative logic programming language).
The proposed solution was:
...
- 31
3
votes
0
answers
222
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 ...
- 31
3
votes
0
answers
145
views
How hard is APPROXIMATE-#SAT? [closed]
It is well known that the problem of counting the satisfying assignments of SAT, namely the problem #SAT, is #P-complete.
It is also suspected (somewhat less widely) that even deciding SAT should ...
- 31