As of May 31, 2023, we have updated our Code of Conduct.

# Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

105 questions
Filter by
Sorted by
Tagged with
6k views

### Encoding 1-out-of-n constraint for SAT solvers

I'm using a SAT solver to encode a problem, and as part of the SAT instance, I have boolean variables $x_1,x_2,\dots,x_n$ where it is intended that exactly one of these should be true and the rest ...
680 views

### Why do all recent SAT solvers work on CNF instead of circuit SAT?

After the release of the AIGER library to handle and-inverter graphs sometime in 2006 (I think), some circuit SAT solvers were released in 2006-2008, and in a few SAT Races/Competitions there were AIG ...
4k views

### Proving that the conversion from CNF to DNF is NP-Hard

How can I prove that the conversion from CNF to DNF is NP-Hard? I'm not asking for an answer, just some suggestions about how to go about proving it.
966 views

### Recipe book for SAT encodings?

SAT solvers are getting more and more efficient in solving large instances and are being used as back-ends in various contexts. Every time one wants to use them to solve a problem in a specific domain,...
3k views

### When to use SAT vs Constraint Satisfaction?

If I have a hard problem, one standard approach is to express it as a SAT instance and try running a SAT solver on it. Another standard approach is to express it as a constraint satisfaction problem, ...
541 views

### Multicore SAT Solver

I am trying to solve a 25k clauses 5k variables SAT problem. As it has been running for an hour (precosat) and I'd like to solve bigger ones afterwards, I'm looking for a multi-core SAT-Solver. As ...
837 views

### Unification vs. SAT solver

I read on Wikipedia that unification is a process of solving the satisfability problem. At the same time, I know that such solvers are called "SAT solvers" or "SMT solvers". So, are they different ...
2k views

### Are there competitions for integer programming?

Are there competitions for integer programming like there are for SAT and MAXSAT?
847 views

### Can top SAT-solvers factor easy numbers?

Modern SAT-solvers are very good at solving many real-world examples of SAT instances. However, we know how to generate hard ones: for instance use a reduction from factoring to SAT and give the RSA ...
552 views

### Introduction into first order logic verification

I am trying to teach myself different approaches to software verification. I have read some articles. As far as I learned, propositional logic with temporal generally uses model checking with SAT ...
2k views

### Why the need for TSP solvers when there are SAT solvers?

Concorde TSP is a solver for TSP. SAT solvers are solvers for boolean satisfiability. TSP and SAT are NP-complete. Hence, why spent the time to develop Concorde TSP when there is an abundance of SAT ...
1k views

### Conflict Driven Clause Learning backtracking clarification

On the wikipedia page here it describes pretty well the CDCL algorithm (and it seems the pictures were taken from slides created by Sharad Malik at Princeton). However when describing how to backtrack ...
768 views

### Deterministic SAT solver

I have the following question. Is the SAT solvers are deterministic? I mean, for example, about miniSAT and DPLL algorithm. Are they completely deterministic? If these algorithms will return unSAT ...
226 views

### Assignment to make formula unsatisfiable

Lets imagine we have a satisfiable formula $F(A_0, A_1,...A_k,S_0,...,S_n)$ The problem to solve is "Is there an assignment for variables $(S_0,...,S_n)$ which will make F unsatisfiable?". One way of ...
249 views

### Framework or tools to generate theorem prover/solver/reasoner for new logic

I have new logic which has syntax and semantics in usual natural languages and I have to create theorem prover/solver/reasoner for this logic. Is there framework or tool set that can generate such ...
171 views

### Common method for solving satisfiability problems which lie in P

I know from Schaefer's Dichotomy Theorem that only a few types of satisfiability problems are in P and any other problem is NP-complete. However, all of the algorithms I know for them use specific ...
824 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. ...
283 views

### How to use an old SAT solver to discover a new one, as is done in The Golden Ticket?

In Lance Fortnow's book The Golden Ticket, he mentions that once you have a polynomial-time algorithm for an NP-complete problem, you can use it to find a faster algorithm. Can you tell me how that is ...
2k views

### Why is pure literal elimination absent in DPLL-based algorithms like Chaff?

I'm looking into various SAT-solvers and trying to understand how they work and why they are designed in certain ways. (But I'm not in a university at the moment and I do not know anyone who is a ...
238 views

### Convert $\sum x_i = y$ to 3-sat

I have a simple looking question. What is the most efficient conversion of $\sum_{i=1}^n x_i = y$ to 3-sat? Here $x_i$ is either $1$ or $0$ and $y$ is some positive integer. Can you do better than ...
5k views

### Understanding DPLL algorithm

I'm trying to understand DPLL algorithm for solving SAT problem. And here it is: ...
2k views

### Why don't modern SAT solvers use the notion of a "watched clause", in the same way they use the notion of a "watched literal"?

Modern SAT solvers use the notion of "watched literals": when a value is chosen for a literal $l$, the solver only checks whether that falsifies clauses with $l$ in them if $l$ is one of the watched ...
767 views

### Why is DPLL better than brute force?

I understand that by being clever about the way we navigate the search space of the SAT problem we're going to get better performance than by randomly choosing and testing solutions, though of course ...
7k views

### Forward checking vs arc consistency on 3-SAT

If I were to let the variables be the propositions and, constraint be all clauses being satisfied, which technique would be more effective in solving 3-SAT? Forward checking or arc consistency? From ...
125 views

### Why is this SAT problem hard and what can I do about it?

For a graph theory problem I need to solve hundreds of millions of CNF problems that typically have around 200 variables and 15,000 clauses no larger than 10. By default I use glucose, which usually ...
299 views

### Detection of redundant boolean constraints

I'm trying to solve a constraint programming problem using a SAT solver. I have set of constraints in the form of propositional logic statements, which are converted to CNF using Tseitin ...
1k views

### Running time of CDCL compared to DPLL

What's the complexity of Conflict-Driven Clause Learning SAT solvers, compared to DPLL solvers? Was it proven that CDCL is faster in general? Are there instances of SAT that are hard for CDCL but easy ...
1k views

### Are there any open source SAT solvers with UNSAT core extraction algorithm built in?

Just like the title says. I need to use a SAT solver on a series of CNF formulas but not only do I need an answer of the type satisfiable/unsatisfiable but also some subset of clauses whose ...
186 views

### Introduction to bounded model checking that describes model generation

Most of the tutorials I have found on model checking and bounded model checking start with, the model is given as a Kripke Structure M = (S,I,T,L) where S is a set of states, I is a set of initial ...
586 views

### How to Modify SAT Solvers to Produce Resolution Refutations for Unsatisfiable Instances?

In recent SAT competitions, there is a Certified UNSAT track. The problem instances are all unsatisfiable and the solvers are asked to produce certificates for unsatisfiability. One way is to produce ...
248 views

### Solving SAT using tableau calculus

I've learned about tableau calculus which is a decision procedure solving the problem of satisfiability of a first order logic formula. Now I'm wondering why this technique can't be used to solve the ...
388 views

208 views

### If a CNF contains only Horn and Xor clauses, then what is the complexity of determining Satisfiability?

If a CNF contains only Horn and Xor clauses, and does not contain clauses of other types, then can its Satisfiability be determined in polynomial time?
136 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 ...
2k views

### CSP Forward checking with n-ary (and binary) constraints

I have implemented my own CSP solver using a Backtracking algorithm. Within the Backtracking algorithm I apply a Forward Checking algorithm (reducing domains of connected, unnasigned variables) that ...
329 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: ...