# Questions tagged [satisfiability]

Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

85 questions
Filter by
Sorted by
Tagged with
7k 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 ...
• 162k
4k views

### Converting (math) problems to SAT instances

What I want to do is turn a math problem I have into a boolean satisfiability problem (SAT) and then solve it using a SAT Solver. I wonder if someone knows a manual, guide or anything that will help ...
• 415
4k views

### Is finding a solution of a satisfiability problem harder than deciding satisfiability?

Is the problem of determining whether or not a given Boolean expression is satisfiable computationally distinct from actually finding a solution to the expression? In other words, is there another ...
• 171
2k views

### Is there a sometimes-efficient algorithm to solve #SAT?

Let $B$ be a boolean formula consisting of the usual AND, OR, and NOT operators and some variables. I would like to count the number of satisfying assignments for $B$. That is, I want to find the ...
• 1,537
1k 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,...
• 425
10k views

436 views

### What is wrong with this seeming contradiction with a paper about AND-compression of SAT?

Got a simple construction seemingly contradicting a paper assuming plausible conjecture. Since it is unlikely the conjecture to be false, what is wrong with the argument? From a paper An AND-...
• 175
433 views

### An Exact Method for Solving Small Instances of XORSAT

I have a couple of small instances for XORSAT for which I am to design and implement an exact method. However, there are a few catches. It is guaranteed that there always exists and answer but I need ...
• 63
6k views

### Understanding DPLL algorithm

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

### Complexity of deciding the satisfiability of a quasi-monotone CNF formula

A quasi-monotone CNF formula is a formula where each variable appears at most once as a positive literal (and any number of times as a negative literal). What is the complexity of deciding its ...
4k views

### Find hamilton cycle in a directed graph reduced to sat problem

I need to find a Hamiltonian cycle in a directed graph using propositional logic, and to solve it by sat solver. So after I couldn't find a working solution, I found a paper that describes how to ...