Skip to main content
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 ...
Martin Berger's user avatar
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 ...
Ivan Smirnov's user avatar
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 ...
Martin Berger's user avatar
10 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 ...
Kyle Jones's user avatar
  • 8,101
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.'s user avatar
  • 162k
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 ...
vzn's user avatar
  • 11.1k
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.'s user avatar
  • 162k
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 ...
Caleb Stanford's user avatar
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 ...
Ggouvine's user avatar
  • 485
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 ...
Caleb Stanford's user avatar
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 ...
Juho's user avatar
  • 22.6k
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.'s user avatar
  • 162k
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 ...
Juho's user avatar
  • 22.6k
4 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 ...
Kyle Jones's user avatar
  • 8,101
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.'s user avatar
  • 162k
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 ...
Yuval Filmus's user avatar
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 ...
Kyle Jones's user avatar
  • 8,101
4 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.'s user avatar
  • 162k
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 ...
orlp's user avatar
  • 13.8k
4 votes
Accepted

Practical hard 3-sat instances

do we know for which $n_0$ these assumptions "kick in" in the case of $3-SAT$? Can we generate, or at least be confident of the existence of a relatively small formula ($< 200$), such that every ...
Tom van der Zanden's user avatar
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. ...
Simon's user avatar
  • 232
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 ...
Curtis F's user avatar
  • 1,043
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 ...
mhum's user avatar
  • 2,146
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 ...
Lawnmower Man's user avatar
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.
Yuval Filmus's user avatar
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,...
Max's user avatar
  • 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 ...
RTK's user avatar
  • 332
3 votes
Accepted

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

Assuming you work in CNF, construct "at least $k+1$-out-of-$n$" and add "or $p$" to each disjunction. Do the same for "at most $k-1$-out-of-$n$" and add "or $q$" to each disjunction. Then add one ...
orlp's user avatar
  • 13.8k
3 votes
Accepted

Is it feasible to solve this subset cover problem with SAT solver?

Optimization with SAT is usually referred as MaxSAT instead of Min SAT. In particular, I suggest looking for solvers for "weighted partial MaxSAT", for example MaxHS and RC2. The problem size you ...
Laakeri's user avatar
  • 1,339
3 votes

Is it feasible to solve this subset cover problem with SAT solver?

With SAT, it can be challenging to predict what will be feasible and what won't. It's worth a try. I would suggest that, instead of MinSAT, you first try using binary search on $n=|\mathcal{S}|$, ...
D.W.'s user avatar
  • 162k

Only top scored, non community-wiki answers of a minimum length are eligible