# Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

102 questions
Filter by
Sorted by
Tagged with
35 views

### resolving in CDCL

When resolving in Conflict driven clause learning, it is the case that if you resolve a conflicting clause with the reason of the negation of one of his literals, then this results in another ...
31 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 ...
• 161
1 vote
49 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$ ...
• 161
66 views

• 549
71 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
385 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
85 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 ...
• 375
779 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
1 vote
85 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'...
208 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
103 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 ...
• 183
181 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 ...
61 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 ...
• 243
42 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 ...
• 123
146 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 ...
• 159
1 vote
77 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 ...
• 113
297 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
420 views

### Is any sudoku solver an SAT solver?

I have recently created a sudoku solver using C#, which outputs the solution to a sudoku after a reasonable amount of time in many cases. I have used the basic sudoku SAT-reduction (i.e. x111 meaning ...
1 vote
151 views

### General Understanding of SMT Solving Across Multiple Theories

My first question was a little too simplified in that it turned out to be an integer linear programming problem solvable with the Simplex Method. However, what I think I am wondering about is how to ...
• 1,911
549 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 ...
• 1,911
253 views

### How a SMT / SAT Solver Generates Valuations for this Example

First, an example of a set of constraints which turned out not to be solvable (I don't think): ...
• 1,911
1 vote
249 views

### Counting solutions of a particular type in HORN SAT

I am interested in counting the number of solutions of a particular type (say #) in HORN SAT. I have 2 questions concerning the same. Suppose we have a HORN SAT -: $(x_1) \land (x_2 \implies x_1)$, ...
69 views

### How to find a nearly-optimal covering of a set using SAT?

I have recently started thinking about application of SAT in solving different problems and how I can encode those problems into a SAT problem. I think one of the interesting problems where SAT ...
• 153
131 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
280 views

### SAT solver optimizations of DPLL for unsatisfiable formulas [duplicate]

I am implementing a SAT solver based on DPLL algorithm, and it works fine on small formulas and larger satisfiable problems. My case split is based on a tree like structure, where every branch is ...