# Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

110 questions
Filter by
Sorted by
Tagged with
1 vote
49 views

### How to find the learned clause from a UIP cut

I would guess that this question is going to make some people wonder how I haven't already found a solution looking through papers -- but I do not see a clear algorithm. In implementing CDCL, I read ...
1 vote
34 views

### Showing SAT is auto-reducible

I am trying to wrap my head around the concepts of auto-reducibility and having access to an Oracle. The way I understand is that a language is auto-reducible iff there is a Turing Machine $M^{L}(x)=1$...
1 vote
84 views

### Specialized SAT solver (?)

(Context) Given two byte arrays of length 16, say $L$ and $H$, one can define a mapping $M$ from the set of all bytes to itself in the following way. If $0 \le b \lt 256$ is a byte, let $\text{lo}(b)$ ...
66 views

### Could SAT solvers be significantly more efficient if they allowed for non-CNF formula?

SAT Solvers focus on CNF formulas. For many implications it is much mroe natural to use implications and conjunctions to encode problems, and when converting to CNFs, information is lost, and the ...
13 views

### Reference request for Unit Clause Based SAT Reduction Rules

I tested my XSAT solver using the 4 pigeons in 3 holes problem converted to XSAT. The pigeon hole instance I give below had 108 variables and 88 clauses after being converted to monotone XSAT. My ...
16 views

### Complexity Class of the Problem: Existence of Unsatisfying Interpretations in Boolean Formulas

What is the complexity class of the problem if there exist two different interpretations that do not satisfy a given Boolean formula? I believe the problem of existence of an interpretation that does ...
44 views

### What's the relation between DPLL and BDDs?

BDDs are a way of representing Boolean formulas. DPLL is an algorithm to determine satisfiability of Boolean formulas. My understanding is that the two are used for SAT solving. How are they combined?
31 views

### CDCL SAT solvers and don't cares

Modern CDCL SAT solvers often can return partial assignments where missing literals mean that the value of that variable is not important for the satisfaction of the formula (i.e. it is a don't care). ...
46 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 ...
10 views

46 views

### Can you help me find some examples of 3co-SAT for 4 variables?

I've been studying the examples of 3co-SAT recently. It's easy to find an example of one variable. $(x_1\lor x_1\lor x_1)\land (\overline{x_1}\lor \overline{x_1}\lor \overline{x_1})$ Examples of 2 ...
93 views

### what does **input** mean for the $3SAT$ question? Is it the number of variables $n$ or the number of clauses $m$

We know that $3SAT \in NP$, and the definition of $NP$ is as follows: $NP$ is the class of languages that have polynomial time verifiers. But I have a question: what does input mean for the $3SAT$ ...
298 views

170 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 ...
738 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 (...
120 views

### Non-Boolean SAT

I was wondering about the complexity of SAT tests with variables $x_i = 0 \lor 1 \lor 2 \dots \lor n$, with clauses being of the form $x_i = a \implies x_j \neq b$. When $n=2$, we have 2SAT, which has ...
854 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. ...
1 vote
142 views

### Can an optimization algorithm be "universal"?

I am wondering if a Bayesian Optimization framework (e.g. Google's Vizier) can be used in lieu of a traditional solver like Gurobi or CPLEX. In trying to answer this question, I realized that I don'...
313 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 ...
1 vote
122 views

### 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 ...
255 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 ...
69 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 ...
47 views

### Translation of diagnosis problem to SAT

I have the following diagnosis problem: h(A): z1 = not(in1) h(D): z2 = not(in2) h(B): z3 = z1 or z2 h(C): out1 = not(z3) h(E): out2 = not(z3) This is an image of the system: I have an observation ...
223 views

### Fine-grained complexity of 3-CNF formula evaluation

It's well known that 3-SAT is in NP, which means that one can evaluate a 3-CNF formula in polynomial time. However, I was wondering what the tightest upper bound is for formula verification, expressed ...
1 vote
87 views

### Why not do these checks on the number of clauses in 3-SAT?

I've been writing a 3-SAT solver for fun and comparing its performance against the solver pycosat. My solver vastly outperforms pycosat in two special cases, where I solve by doing simple, obvious ...
342 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: ...