14
votes
Deterministic SAT solver
Core algorithms like DPLL and its refinements like CDCL are completely deterministic.
Note that non-determinism doesn't necessarily mean that an algorithm may lead to a wrong result. For example we ...
- 8,308
13
votes
Accepted
Why the need for TSP solvers when there are SAT solvers?
TL;DR: polynomial reduction increases the size of a problem; using a specific solver allows you to exploit the structure of a problem.
When you reduce one NP-complete problem to another one, the size ...
- 887
10
votes
Accepted
Framework or tools to generate theorem prover/solver/reasoner for new logic
There are many related ways you can mechanise your logic.
Deep embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is (almost) always possible, but makes using ...
- 8,308
9
votes
Accepted
Random restarts for unsatisfiable instances
There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both ...
- 8,011
7
votes
Accepted
Why is pure literal elimination absent in DPLL-based algorithms like Chaff?
Solvers that use the two-watched-literals algorithm to implement unit propagation don't keep track of which clauses have been deleted (by implication) to produce the subformula implied by the current ...
- 8,011
7
votes
Encoding 1-out-of-n constraint for SAT solvers
A paper by Magnus Björk describes two techniques that could be worth trying.
For 1-out-of-$n$, one can use both one-hot and binary encoding simultaneously. Thus, we have $x_1,\dots,x_n$ as a one-hot ...
D.W.♦
- 154k
7
votes
How to use an old SAT solver to discover a new one, as is done in The Golden Ticket?
Actually, probably you can't use a SAT solver to find another SAT solver, unless something surprising happens.
If P = NP, then you can. If P = NP, then the polynomial hierarchy collapses (i.e., P = ...
D.W.♦
- 154k
6
votes
Accepted
Why do all recent SAT solvers work on CNF instead of circuit SAT?
there are a lot of different angles on your question. generally agreed with your premise that looking at "structural information" in a SAT formulation ought to be an excellent research area.
SAT ...
- 11k
6
votes
Deterministic SAT solver
That's correct. DPLL exhaustively explores the space. If it returns 'unsat' then certainly no satisfying assignment exists.
More recently, researchers have developed certifying SAT solvers that ...
D.W.♦
- 154k
6
votes
Accepted
What are the differences between symbolic execution and SAT solvers?
TL;DR: They differ in their basic input and output. SAT and SMT solvers don't know what programs are; they are tools that answer yes or no questions about mathematical formulas. Symbolic execution, on ...
- 6,873
6
votes
Are there competitions for integer programming?
There are no competitions targeting general integer programming or mixed integer programming, but there are (or were) benchmarks, such as the MIPLIB (linear) and the MINLPLIB (nonlinear).
There are ...
- 475
6
votes
Why is this SAT problem hard and what can I do about it?
Why is this SAT problem hard?
A change in perspective may be helpful. It is expected that some SAT problems are extraordinarily hard: if the strong exponential time hypothesis is true, then for any ...
- 6,873
5
votes
How to Modify SAT Solvers to Produce Resolution Refutations for Unsatisfiable Instances?
A clause-learning SAT solver can be described approximately as follows. There is a stash of learned clauses, which starts empty. We run a recursive procedure, which at each point in time, first checks ...
- 275k
5
votes
Deterministic SAT solver
A keyword you might be missing is completeness. In general, a search algorithm is said to be complete if it finds a solution given it exists (given enough time). In particular, DPLL is an example of a ...
- 22.4k
5
votes
Accepted
What's the average number of clauses modern SAT solvers can handle?
You're asking two questions. I'll answer your first question.
There's no simple answer. It depends on the structure of the problem. There are problems with millions of clauses that can be handled ...
D.W.♦
- 154k
5
votes
Accepted
Are there competitions for integer programming?
There are competitions for constraint satisfaction solvers. Some problems there can be readily translated to IP solvers as well. See e.g., MiniZinc challenge which has taken place yearly since 2008 or ...
- 22.4k
4
votes
Accepted
Bit Blasting Algorithm
I assume the formula is
$$(x \ne 0) \land (y|2 = z) \land (1<3).$$
We can handle each clause of the conjunction separately. If $x=(b_3,b_4)$, then $x \ne 0$ translates to
$$b_3 \lor b_4.$$
If $...
D.W.♦
- 154k
4
votes
Another way to solve SAT. Was it known?
You haven't really specified an algorithm, but a similar idea is used by random walk algorithms for SAT such as Schöning's algorithm (see for example Giurgiu's Master thesis or one of the many online ...
- 275k
4
votes
Accepted
How the Abstract DPLL Algorithm Works in SAT Solving
Describing DPLL as a series of state-transition rules is the worst way I've ever seen to aid understanding the algorithm. The pseudocode provided in the WIkipedia article on DPLL is much easier to ...
- 8,011
4
votes
Accepted
Sum of unique integers to cnf constraint
Here's a strategy for solving Kakuro with a SAT solver.
Make a nine variables for each cell, each variable indicating whether that cell contains $1$, $2$, etc.
Add a exactly-one-out-nine constraint ...
- 12.6k
4
votes
Accepted
Solving largely monotone SAT formulas
The theory probably depends on the details. In practice, if you're only interested in solving an instance, here are a some thoughts:
Most literals should be eliminated in presolve of today's solvers. ...
- 232
3
votes
Accepted
Is this possible to solve 3SAT in O(n^24) time and O(1) space?
You are correct in your assumption that your algorithm correctly identifies some unsatisfiable instances, but for the general case it does not work.
For instance, you can always rewrite a clause $\{A,...
- 48
3
votes
Deterministic SAT solver
SAT solvers can be deterministic or not depending on how they are implemented. Note that the nondeterminism here can only affect the generated model not the answer (SAT or UNSAT) of the solver! For ...
- 332
3
votes
Accepted
Is this possible to solve SAT in polynomial time by reducing it to the problem of solving system of nonlinear equations?
It is not currently known whether or not a polynomial algorithm exists to solve these systems of nonlinear equations because, as the reduction provided shows, if such a thing were to exist, it would ...
- 2,002
3
votes
Is this possible to solve 3SAT in O(n^24) time and O(1) space?
The operative phrase is "at least 8"! The funny thing about 3SAT is that every clause with 3 distinct variables eliminates a full 1/8th of the model space. So how is it that you can have a formula ...
- 1,127
3
votes
How to Modify SAT Solvers to Produce Resolution Refutations for Unsatisfiable Instances?
The simplest method of modifying a typical DPLL-based CDCL solver is to have it output every clause it learned while deciding a formula is unsatisfiable. Such a list of clauses constitutes a RUP ...
- 8,011
3
votes
How to choose between UC and PL when using the DPLL algorithm?
If you use the original specification of the DPLL algorithm, in which the unit rule is applied to a fixed point and then the pure literal rule, then only the unit rule is needed to reach a satisfying ...
- 8,011
3
votes
Accepted
If a CNF contains only Horn and Xor clauses, then what is the complexity of determining Satisfiability?
Hint: Using XOR clauses you can express "$x = \lnot y$", and this allows you to simulate general clauses by Horn clauses.
- 275k
3
votes
Accepted
How a SMT / SAT Solver Generates Valuations for this Example
The Simplex algorithm solves the linear programming problem.
Linear programming is the problem of optimizing a linear function with inputs $x_1, x_2, \dots, x_n$ subject to a system of linear ...
- 1,003
3
votes
Accepted
Is any sudoku solver an SAT solver?
Your program is not a SAT solver. A SAT solver takes as input a SAT formula and outputs whether it is satisfiable or not. Your program doesn't take as input a SAT formula, so it isn't a SAT solver....
D.W.♦
- 154k
Only top scored, non community-wiki answers of a minimum length are eligible