# Tag Info

### 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 ...
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 ...
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 ...
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 ...
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 ...

### 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 ...

### 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 = ...
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 ...

### 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 ...
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 ...

### 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 ...

### 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 ...

### 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 ...

### 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 ...
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 ...
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 ...
Accepted

### 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 ...
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 ...

### 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 ...

### 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 ...

### 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 ...
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.
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 ...