# Questions tagged [satisfiability]

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

70 questions
Filter by
Sorted by
Tagged with
5k 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 ...
3k 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 ...
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 ...
806 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

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

1k views

### Is this possible to solve 3SAT in O(n^24) time and O(1) space?

Assume that n is the number variables of the given 3CNF formula (n≥3) and all clauses in the given 3CNF formula are different. That means that for each clause, each literal can be either positive ...
8k views

### To prove 4-SAT CNF is NP-complete [closed]

To answer the question below, 4-SAT: Given a formula in Conjunctive Normal Form, where each clause contains exactly 4 literals, does it have a satisfying truth assignment? I was going to prove that ...
183 views

### Is there an instance of 3-SAT in less than 100 variables that no one has been able to solve?

In number theory, progress is sometimes guided by people stating a specific Diophantine equation that they don't know how to solve. Is there anything similar in the field of Boolean satisfiability? ...
### 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 ...