47
votes
Accepted
Why is SAT so important in theoretical computer science?
SAT was the first problem shown to be NP-complete, in Stephen Cook's seminal paper. Even nowadays, when introducing the theory of NP-completeness, the starting point is usually the NP-completeness of ...
36
votes
Accepted
Why there are no approximation algorithms for SAT and other decision problems?
Approximation algorithms are only for optimization problems, not for decision problems.
Why don't we define the approximation ratio to be the fraction of mistakes an algorithm makes, when trying to ...

D.W.♦
- 156k
23
votes
Can anyone give me an instance of 3SAT with exactly one solution?
The empty 3SAT instance (over no variables) has one solution.
22
votes
Accepted
Is SAT an existential question?
The SAT problem is a decision problem. It means that an algorithm that solves SAT must answer true or false, and not necessarily ...
17
votes
What is wrong with this simple proof of P=NP?
The monotone version of X3SAT that your proof is based on has the nice property that setting a literal false in one clause will never cause the negation of that literal to be true in another, which ...
17
votes
Can anyone give me an instance of 3SAT with exactly one solution?
If you are seeking a formula with 3 variables $x$, $y$, $z$, then you can consider clauses $(\ell_x \vee \ell_y \vee \ell_z)$ where $\ell_x$ is either $x$ or $\neg x$ (and same thing for $\ell_y$ and $...
16
votes
Accepted
Can anyone give me an instance of 3SAT with exactly one solution?
Try this:
$$
(A \lor B \lor C)
\land
(A \lor B \lor \lnot C)
\land
(A \lor \lnot B \lor C)
\land
(A \lor \lnot B \lor \lnot C)
\land
(\lnot A \lor B \lor C)
\land
(\lnot A \lor B \lor \lnot C)
\...
15
votes
Why there are no approximation algorithms for SAT and other decision problems?
The reason you don't see things like approximation ratios in decision making problems is that they generally do not make sense in the context of the questions one typically asks about decision making ...
15
votes
Why is SAT so important in theoretical computer science?
It is worth mentioning that mathematicians cared about SAT [1] even before it was shown to be NP-complete. See for example Godel's 1956 letter to Von Neumann, where it is known that SAT is $\Omega(n)$ ...
14
votes
Deterministic SAT solver
Core algorithms like DPLL and its refinements like CDCL are completely deterministic.
Note that non-determinism doesn't necessarily mean that an algorithm may lead to a wrong result. For example we ...
14
votes
Accepted
Is a "local" version of 3-SAT NP-hard?
$(3,k)\text{-LSAT}$ is in P for all $k$. As you have indicated, locality is a big obstruction to NP-completeness.
Here is a polynomial algorithm.
Input: $\phi\in (3,k)\text{-LSAT}$, $\phi=c_1\wedge ...
13
votes
Accepted
Why the need for TSP solvers when there are SAT solvers?
TL;DR: polynomial reduction increases the size of a problem; using a specific solver allows you to exploit the structure of a problem.
When you reduce one NP-complete problem to another one, the size ...
12
votes
Why is SAT so important in theoretical computer science?
I'll add another perspective, based loosely on Andreas Blass's comment on the accepted answer: SAT is in some sense 'conceptually universal' for a broad class of NP-complete problems. To be more ...
12
votes
Is SAT an existential question?
If you have variables x1 to xn, and you decide in polynomial time whether the problem can be satisfied or not, then if it can be satisfied, you set x1 = true and check if it can still be satisfied. If ...
11
votes
Accepted
Is "Reachable Object" really an NP-complete problem?
A problem $P$ is NP-complete if:
$P$ is NP-hard and
$P \in \textbf{NP}$.
The authors give a proof of item number 1. Item number 2 is probably apparent (and should be clear to the paper's audience). ...
11
votes
Can anyone give me an instance of 3SAT with exactly one solution?
One variable: $(A \lor A \lor A)$
10
votes
P=NP, isn't it?
Every CNF is falsifiable (choose a clause and choose a truth assignment which falsifies it). Unfortunately, the opposite of "CNF $\varphi$ is satisfiable" is not "CNF $\varphi$ is falsifiable". Rather,...
10
votes
Equisatisfiability in the reduction from 4-SAT to 3-SAT
You're right in saying that they should be equisatisfiable. And they are.
I'm not sure why you think converting your unsatisfiable $4-\text{SAT}$ instance into a $3-\text{SAT}$ instance would make it ...
9
votes
Accepted
Lower Bounds for Size of Independent Set in a Graph?
The relevant result is known as Turán's theorem. It states that if a graph has less than (roughly) $n(n-1)/(2r)$ edges then it has an independent set of size $r+1$, and this is tight.
9
votes
Accepted
Can we have a poly time reduction from 2-SAT to 2-Coloring problem?
As rotia mentions in their comment, to make the question meaningful we must restrict the power of the allowable reductions. The two most obvious choices are to allow only logspace reductions or only ...
9
votes
Accepted
To prove 4-SAT CNF is NP-complete
In order to prove that 4-SAT is NP-complete, you need to prove that it is in NP and that it is NP-hard.
Prove 4-SAT $\in$ NP
Given an instance of 4-SAT and an answer that evaluates to TRUE, it's ...
9
votes
In SAT, do we require an assignment for arbitrary variables?
If the truth value of a formula is determined by setting only a subset of the variables, an author might skip describing the remaining truth values. However, by definition, a truth assignment gives a ...
9
votes
Accepted
MAXSAT approximation
I won't speculate about your teacher's reasons for including the random assignment algorithm over yours. However, one advantage of random assignment is that, if every clause has at least $k$ literals, ...
9
votes
Accepted
SAT algorithm for determining if a graph is disjoint
Given a graph $G = (V,E)$, here is a SAT instance which is satisfiable iff the graph is not connected.
Pick an arbitrary vertex $v_0 \in V$, and add the following clauses, over the variables $x_v$ ...
9
votes
Accepted
Random restarts for unsatisfiable instances
There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both ...
9
votes
Accepted
Why can't 3-SAT be solved efficiently if you convert all clauses (x ∨ y ∨ z) into (u ∨ z) by introducing a variable?
$u = (a \vee b) \iff
(u \vee \bar{a}) \wedge (u \vee \bar{b}) \wedge (\bar{u} \vee a) \wedge (\bar{u} \vee b) =1 $
Unfortunately, the equivalence above does not hold.
Let $a=\text{false}$, $b=\text{...
8
votes
Accepted
How to show ExactOneSAT is NP-Complete?
We can reduce 3SAT to ExactOneSAT (3SAT $\leq_P$ ExactOneSAT) as follows. Replace each clause $C_m$ by $(z_{m,1} \lor z_{m,2} \lor z_{m,3})$ and ensure that if $C_m$ is, say, $(v_i \lor \overline{v_j} ...
8
votes
Results on the difficulty of specific random 3-SAT problems?
Research has concentrated not on the number of satisfying assignments, but on the clause density $\alpha$. It is (more or less) known that:
Below a certain threshold, the problem is easy. Moreover, ...
8
votes
Why there are no approximation algorithms for SAT and other decision problems?
In addition to the existing answers, let me point out that there are situations where it makes sense to have an approximate solution for a decision problem, but it works different than you might think....
7
votes
Encoding 1-out-of-n constraint for SAT solvers
A paper by Magnus Björk describes two techniques that could be worth trying.
For 1-out-of-$n$, one can use both one-hot and binary encoding simultaneously. Thus, we have $x_1,\dots,x_n$ as a one-hot ...

D.W.♦
- 156k
Only top scored, non community-wiki answers of a minimum length are eligible
Related Tags
satisfiability × 661complexity-theory × 256
np-complete × 140
3-sat × 108
sat-solvers × 81
reductions × 75
logic × 71
algorithms × 66
np × 44
np-hard × 39
time-complexity × 34
propositional-logic × 32
2-sat × 30
boolean-algebra × 29
constraint-satisfaction × 28
graphs × 27
reference-request × 22
decision-problem × 22
polynomial-time × 21
optimization × 18
p-vs-np × 18
first-order-logic × 13
counting × 12
co-np × 11
smt-solvers × 11