Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
659
questions
32
votes
3
answers
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 ...
D.W.♦
- 156k
30
votes
3
answers
1k
views
Measuring the difficulty of SAT instances
Given an instance of SAT, I would like to be able to estimate how difficult it will be to solve the instance.
One way is to run existing solvers, but that kind of defeats the purpose of estimating ...
- 4,812
28
votes
4
answers
6k
views
Why is SAT so important in theoretical computer science?
In my Computability and Complexity class, we are focusing on P, NP,
NP-complete, and NP-hard problems and the one thing that keeps coming up
is the SAT problem, in the context of reduction from one ...
- 391
24
votes
3
answers
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,527
23
votes
3
answers
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 ...
- 415
22
votes
1
answer
2k
views
Classification of intractable/tractable satisfiability problem variants
Recently I found in a paper [1] a special symmetric version of SAT called the 2/2/4-SAT. But there are many $\text{NP}$-complete variants out there, for example: MONOTONE NAE-3SAT, MONOTONE 1-IN-3-SAT,...
- 12.4k
21
votes
1
answer
714
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 ...
- 393
20
votes
2
answers
22k
views
What's an example of an unsatisfiable 3-CNF formula?
I'm trying to wrap my head around an NP-completeness proof which seem to revolve around SAT/3CNF-SAT.
Maybe it's the late hour but I'm afraid I can't think of a 3CNF formula that cannot be satisfied (...
- 311
20
votes
3
answers
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
20
votes
1
answer
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.
- 301
20
votes
1
answer
3k
views
Implementing the GSAT algorithm - How to select which literal to flip?
The GSAT algorithm is, for the most part, straight forward: You get a formula in conjunctive normal form and flip the literals of the clauses until you find a solution that satisfies the formula or ...
- 303
20
votes
1
answer
952
views
Supporting data structures for SAT local search
WalkSAT and GSAT are well-known and simple local search algorithms for solving the Boolean satisfiability problem. The pseudocode for the GSAT algorithm is copied from the question Implementing the ...
- 22.5k
19
votes
3
answers
3k
views
Why there are no approximation algorithms for SAT and other decision problems?
I have an NP-complete decision problem. Given an instance of the problem, I would like to design an algorithm that outputs YES, if the problem is feasible, and, NO, otherwise. (Of course, if the ...
- 693
17
votes
2
answers
5k
views
Is generalized XOR-SAT efficiently solvable?
I've seen how XOR-3-SAT is efficiently solvable (for instance, see the "XOR-satisfiability" section in the Wikipedia entry for Boolean satisfiability problem).
I'm wondering a basic question: Is ...
- 882
17
votes
1
answer
3k
views
Planarity conditions for Planar 1-in-3 SAT
Planar 3SAT is NP-complete. A planar 3SAT instance is a 3SAT instance for which the graph built using the following rules is planar:
add a vertex for every $x_i$ and $\bar{x_i}$
add a vertex for ...
- 12.4k
16
votes
2
answers
4k
views
Poly-time reduction from ILP to SAT?
So, as is known, ILP's 0-1 decision problem is NP-complete. Showing it's in NP is easy, and the original reduction was from SAT; since then, many other NP-Complete problems have been shown to have ILP ...
- 263
16
votes
2
answers
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
16
votes
2
answers
1k
views
A dense NP complete language implies P=NP
We say that the language $J \subseteq \Sigma^{*}$ is dense if there exists a polynomial $p$ such that $$ |J^c \cap \Sigma^n| \leq p(n)$$ for all $n \in \mathbb{N}.$ In other words, for any given ...
- 2,450
15
votes
3
answers
9k
views
Prove NP-completeness of deciding satisfiability of monotone boolean formula
I am trying to solve this problem and I am really struggling.
A monotone boolean formula is a formula in propositional logic where all the literals are positive. For example,
$\qquad (x_1 \lor x_2) ...
- 153
14
votes
2
answers
30k
views
Proving DOUBLE-SAT is NP-complete
The well known SAT problem is defined here for reference sake.
The DOUBLE-SAT problem is defined as
$\qquad \mathsf{DOUBLE\text{-}SAT} = \{\langle\phi\rangle \mid \phi \text{ has at least two ...
- 753
14
votes
1
answer
2k
views
Why do Shaefer's and Mahaney's Theorems not imply P = NP?
I'm sure someone has thought about this before or immediately dismissed it, but why does Schaefer's dichotomy theory along with Mahaney's theorem on sparse sets not imply P = NP ?
Here's my ...
- 1,611
14
votes
2
answers
2k
views
MIN-2-XOR-SAT and MAX-2-XOR-SAT: are they NP-hard?
What is the complexity of $\text{MIN-2-XOR-SAT}$ and $\text{MAX-2-XOR-SAT}$? Are they in P? Are they NP-hard?
To formalize this more precisely, let
$$\Phi\left(\mathbf x\right)={\huge\wedge}_{i}^{...
D.W.♦
- 156k
13
votes
3
answers
3k
views
Is 2-SAT with XOR-relations NP-complete?
I'm wondering if there is a polynomial algorithm for "2-SAT with XOR-relations". Both 2-SAT and XOR-SAT are in P, but is its combination?
Example Input:
2-SAT part: ...
- 2,469
12
votes
3
answers
2k
views
Why does Schaefer's theorem not prove that P=NP?
This is probably a stupid question, but I just don't understand. In another question they came up with Schaefer's dichotomy theorem. To me it looks like it proves that every CSP problem is either in P ...
- 2,469
12
votes
4
answers
2k
views
Are there competitions for integer programming?
Are there competitions for integer programming like there are for SAT and MAXSAT?
- 326
11
votes
1
answer
16k
views
DNF to CNF conversion: Easy or Hard
In relation to the thread Proving that the conversion from CNF to DNF is NP-Hard (and a related Math thread):
How about the other direction, from DNF to CNF? Is it easy or hard?
On Page 2 of this ...
- 345
11
votes
1
answer
9k
views
How to prove that a constrained version of 3SAT in which no literal can occur more than once, is solvable in polynomial time?
I'm trying to work out an assignment (taken from the book Algorithms - by S. Dasgupta, C.H. Papadimitriou, and U.V. Vazirani, Chap 8, problem 8.6a), and I'm paraphrasing what it states:
Given that ...
- 592
11
votes
1
answer
552
views
If one shows that UNIQUE k-SAT is in P, does it imply P=NP?
Valiant & Vazirani proved SAT is reducible to UNIQUE SAT under randomized probabilistic reductions in polynomial time. Calabro et al. showed that UNIQUE k-SAT is as hard as k-SAT. Now the ...
- 190
11
votes
1
answer
801
views
Complexity of deciding if a formula has exactly 1 satisfying assignment
The decision problem
Given a Boolean formula $\phi$, does $\phi$ have exactly one satisfying assignment?
can be seen to be in $\Delta_2$, $\mathsf{UP}$-hard and $\mathsf{coNP}$-hard. Is anything ...
- 3,491
11
votes
1
answer
882
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 ...
- 4,812
10
votes
2
answers
3k
views
What is wrong with this simple proof of P=NP?
Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiabilty problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause ...
- 341
10
votes
2
answers
358
views
Explaining SAT to high school science teachers
I am a high school sophomore who is interested in computer science. I developed a cool algorithm for #SAT, and I'm implementing and doing a science fair project on it. My adviser, who is the best ...
9
votes
2
answers
5k
views
Is SAT an existential question?
Some sources state that an algorithm that solves the SAT problem not only needs to decide whether a given existentially-quantified formula is satisfiable or not, but, additionally, in the case where ...
- 195
9
votes
1
answer
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 ...
- 93
9
votes
2
answers
241
views
Find $\epsilon'$ s.t $L_\epsilon$ is $\mathsf{NP}$-hard for any $\epsilon<\epsilon'$
Let $L_\epsilon$ be the language of all $2$-CNF formulas $\varphi$, such that at least $(\frac{1}{2}+\epsilon)$ of $\varphi$'s clauses can be satisfied.
I need to prove that there exists $\epsilon'$ ...
- 511
9
votes
1
answer
471
views
Is weighted XOR-SAT NP-hard?
Given $n$ boolean variables $x_1,\ldots,x_n$ each of which is assigned a positive cost $c_1,\ldots,c_n\in\mathbb{Z}_{>0}$ and a boolean function $f$ on these variables given in the form
$$f(x_1,\...
- 193
9
votes
1
answer
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 ...
- 3,790
9
votes
1
answer
158
views
What is the name of the problem? (partitioning graph into three covers)
I was wondering if this problem has a name:
Given a simple graph whose edges are colored red, blue and green, $G=(V,B\cup R\cup G)$, is there a vertex-coloring $c:V\to \{B,R,G\}$ such that every edge ...
- 2,624
9
votes
1
answer
1k
views
Complexity of (SAT to 3-SAT) Problem?
It is well known that any CNF formula can be transform in polynomial time into a 3-CNF formula by using new variables (see here). If using new variables is not allowed, it is not always possible (...
- 511
9
votes
1
answer
231
views
Verify correctness of quantifier elimination, using SAT
Let $x=(x_1,\dots,x_n)$ and $y=(y_1,\dots,y_n)$ be $n$-vectors of boolean variables. I have a boolean predicate $Q(x,y)$ on $x,y$. I give my friend Priscilla $Q(x,y)$. In response, she gives me $P(...
D.W.♦
- 156k
8
votes
4
answers
791
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 ...
- 81
8
votes
2
answers
1k
views
Is SAT in P if there are exponentially many clauses in the number of variables?
I define a long CNF to contain at least $2^\frac{n}{2}$ clauses, where $n$ is the number of its variables. Let $\text{Long-SAT}=\{\phi: \phi$ is a satisfiable long CNF formula$\}$.
I'd like to know ...
- 462
8
votes
2
answers
652
views
What is a dichotomy? Whether 2-SAT itself is a dichotomy of SAT?
Recently, I am reading papers about dichotomy. I do not understant what condition can be called as a dichotomy? What is the meaning of "a question is either in P or in NP-complete"? (assume P $\neq$ ...
8
votes
2
answers
3k
views
Is "Reachable Object" really an NP-complete problem?
I was reading this paper where the authors explain Theorem 1, which states "Reachable Object" (as defined in the paper) is NP-complete. However, they prove the reduction only in one direction, i.e. ...
- 183
8
votes
2
answers
1k
views
SAT algorithm for determining if a graph is disjoint
What are some good algorithms to have a SAT (CNF) solver determine if a given graph is fully-connected or disjoint?
The best one I can think of is this:
Number the nodes 1..N, where N is the number ...
- 203
8
votes
1
answer
687
views
Is a "local" version of 3-SAT NP-hard?
Below is my simplification of part of a larger research project on spatial Bayesian networks:
Say a variable is "$k$-local" in a string $C \in 3\text{-CNF}$ if there are fewer than $k$ clauses ...
- 319
8
votes
2
answers
230
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 ...
8
votes
1
answer
394
views
How much can we reduce the number of clauses by converting from $k$-SAT to $(k+m)$-SAT?
If we suppose that we start with an instance of $k$-SAT, and try converting the problem to an instance of $(k+m)$-SAT, where there are $(k+m)$ literals per clause, can we guarantee a reduction in the ...
- 882
8
votes
2
answers
424
views
A tentative satisfiability algorithm
General satisfiability (with a few exceptions such as Horn Clauses) is not believed to have an algorithmic solution. However, the following algorithm appears to be a solution for general ...
user1422
7
votes
3
answers
431
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