Tag Info

46

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 SAT. SAT is also amenable to surprisingly successful heuristic algorithms, implemented by software known as SAT solvers. As a result, there is a lot of ...

35

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 solve some decision problem? Because "the approximation ratio" is a term with a well-defined, standard meaning, one that means something else, and it would be ...

31

Technically, you can write $x\wedge \neg x$ in 3-CNF as $(x\vee x\vee x)\wedge (\neg x\vee \neg x\vee \neg x)$, but you probably want a "real" example. In that case, a 3CNF formula needs at least 3 variables. Since each clause rules out exactly one assignment, that means you need at least $2^3=8$ clauses in order to have a non-satisfiable formula. Indeed, ...

21

Chapter 2 of the SAT Handbook (by Steven Prestwich) covers how to turn discrete decision problems into CNF, in some depth. (Unfortunately, I don't think there is a draft version online -- probably best to consult your local library.) Several of the other references cited in Magnus Björk's quirky overview Successful SAT Encoding Techniques are also useful. ...

20

The empty 3SAT instance (over no variables) has one solution.

16

If you are willing to introduce additional variables, you can convert from DNF to CNF form in polynomial time by using the Tseitin transform. The resulting CNF formula will be equisatisfiable with the original DNF formula: the CNF formula will be satisfiable if and only if the original DNF formula was satisfiable. See also https://en.wikipedia.org/wiki/...

15

Unless you're translating mathematical problems to SAT instances as a learning exercise, your time will be much more fruitfully spent learning about satisfiability modulo theories. SMT will allow you to express equations and other constraints much more naturally than as Boolean SAT instances. Some SMT solvers support existential and universal quantifiers, ...

15

As mentioned in a comment, any method of determining satisfiability of a Boolean formula can be easily converted into a method for finding the satisfying variable assignment. This is because all NP-complete problems are downward self-reducible. From Wikipedia: Self-reducibility The SAT problem is self-reducible, that is, each algorithm which correctly ...

15

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 means you can say The only way a conflict can occur is when all literals in a clause are set to false. and it will be true because forcing two literals false ...

15

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)$ (which I believe is still the best lower bound known, although we know explicit constant factors for some lower bound at least), and discussed that if SAT is $... 15 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$\ell_z$). There is a total of 8 such clauses. If you consider a conjunction of all 8 clauses and remove exactly one of them, you get a 3-CNF formula with ... 14 0-1 ILP formulated as: Does there exist a vector$\mathbf{x}$, subject to constraints: $$\left.\begin{array}{rrrrr|rr} a_{11} x_1 & + &a_{12} x_2 & ... + & a_{1n} x_n\le b_1 \\ a_{21} x_1 & + &a_{22} x_2 & ... + & a_{2n} x_n\le b_2 \\ ...\\ a_{m1} x_1 & + &a_{m2} x_2 & ... + & a_{mn} x_n\... 14 Schaefer's theorem applies only to a specific type of languages, those of the form \mathrm{SAT}(S) for a finite set of relations over the Boolean domain or \mathrm{CSP}(\Gamma) for a finite constraint language over the Boolean domain (the two notations are equivalent; see the Wikipedia page for a description). Any other language is not covered by the ... 14 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 problems. In an optimization setting, it makes sense because it's useful to be "close." In many environments, it doesn't make sense. It doesn't make sense to ... 14 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 can distinguish between Monte Carlo algorithms, which are randomised algorithms whose output may be incorrect with some probability. Las Vegas algorithms, ... 14 (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 c_2\cdots \wedge c_m, where c_i is the i-th clause. Output: true if \phi becomes 1 under some assignment of all variables. Procedure: Construct set B_i... 13 For the special case of k out of n variables true where k = 1, there is commander variable encoding as described in Efficient CNF Encoding for Selecting 1 to N Objects by Klieber and Kwon. Simplified: Divide the variables into small groups and add clauses that cause a commander variable's state to imply that a group of variables is either all false or all-... 13 A (coarse) dichotomy theorem states that in a certain class of problems, each problem is either in P or NP-hard. For example, Schaefer's dichotomy theorem concerns the class of problems of the form \mathrm{SAT}(S). Here S is a collection of Boolean relations, and \mathrm{SAT}(S) is the problem of deciding satisfiability of propositions which are ... 13 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) \land (\lnot A \lor \lnot B \lor C) $$12 The "parent" of the problem you're looking at is sometimes called Weighted Satisfiability (WSAT, particularly in parameterized complexity) or Min-Ones (though this is normally an optimization version, but near enough). These problems have the "at most k variables set to true" restriction as their defining feature. The restriction to monotone formulae is ... 12 The confusion arises from a misunderstanding of what being polynomial in the size of the largest instance means. It does not mean that polynomial growth of the compressor's output is allowed as the number of instances (t) increases. Rather it means the compressor's output is allowed to grow only as the maximum instance size grows, independent of t, and ... 12 It looks like the Wikipedia article you linked to says that XORSAT (not just 3-XORSAT) is in P. The method by which they are solving that 3-XORSAT formula in their example very easily generalizes to formulas in which the clauses can have arbitrarily large numbers of variables and differing numbers of variables. You just look at the formula as a system of ... 12 2-SAT-with-XOR-relations can be proven NP-complete by reduction from 3-SAT. Any 3-SAT clause$$(x_1 \lor x_2 \lor x_3)$$can be rewritten into the equisatisfiable 2-SAT-with-XOR-relations expression$$(x_1 \lor \overline{y}) \land (y \oplus x_2 \oplus z) \land (\overline{z} \lor x_3)$$with$y$and$z$as new variables. 12 Schaefer's theorem covers a very specific situation: you are given a finite set$\Gamma$of relations, and are interested in the complexity of$\mathrm{CSP}(\Gamma)$. Schaefer's theorem gives you an algorithm to decide whether this problem is NP-complete or in P. It doesn't cover any other situation. When you translate a problem like integer factorization ... 12 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 specific, I'd argue that SAT captures the essence of Constraint Satisfaction Problems: find a configuration that satisfies a given set of conditions. Sudoku is a ... 11 Your problem is known as the$\text{UNIQUE-SAT}$problem which is$\mathsf{US}$-complete. The problem is in$\mathsf{D^p}$but not known to be$\mathsf{D^p}$-hard under deterministic polynomial time reductions, where the class$\mathsf{D^p} = \{ L_1 \cap \overline{L_2} \mid L_1,L_2 \in \mathsf{NP} \}$. It was shown by Papadimitriou and Yannakis [1] that ... 11 You can prove it by contradiction: Suppose that$P \neq NP$and there is a polynomial-time reduction from 3-SAT to 2-SAT; then 2-SAT is NP-complete, but 2-SAT is also solvable in polynomial time, so for all decision problems$A \in NP$you can decide$x \in A$reducing$x$to the corresponding 2-SAT instance in polynomial time and solve it in polynomial ... 11 This is still an open question; UP is not known to be equivalent to NP. In the paper "NP Might Not Be As Easy As Detecting Unique Solutions," Beigel, Burhman and Fortnow construct an oracle under which P contains UP but P is still not equivalent to NP. 11 A typical SAT solver notices that a satisfying assignment has been found when there are no more variables to assign. So the only time that a SAT solver would save by early notification is the time it would take to assign values to any remaining unassigned variables. This is a one-time cost linear in the number of variables in the formula. It's linear ... 11 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 of the problem usually grows polynomially. For example, when you reduce a HAMPATH on a graph with$n$nodes to SAT, the resulting formula has size of$\Theta(n^...

Only top voted, non community-wiki answers of a minimum length are eligible