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, ...


28

Here is one solution: Clearly Double-SAT belongs to ${\sf NP}$, since a NTM can decide Double-SAT as follows: On a Boolean input formula $\phi(x_1,\ldots,x_n)$, nondeterministically guess 2 assignments and verify whether both satisfy $\phi$. To show that Double-SAT is ${\sf NP}$-Complete, we give a reduction from SAT to Double-SAT, as follows: On input $\...


21

Counting in the general case The problem you are interested in is known as #SAT, or model counting. In a sense, it is the classical #P-complete problem. Model counting is hard, even for $2$-SAT! Not surprisingly, the exact methods can only handle instances with around hundreds of variables. Approximate methods exist too, and they might be able to handle ...


20

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. ...


18

Informally: In DNF, you can pick any clause to be true, to make the formula true. This means that a DNF that is equivalent to a certain CNF, is basically an enumeration of all the solutions to boolean sat on the CNF. Note, there can be an exponential number of solutions. Since solving boolean sat for CNF for a single solution is NP-complete, converting to ...


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 ...


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

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/...


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

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, ...


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 ...


12

Logic with unary predicates (not operators), is called monadic. The thing that is called propositional logic only has nullary predicates, i.e., constants true and false, and no quantifiers. The undecidability of predicate logic follows because predicate logic (with at least one binary predicate) is powerful enough to describe how a Turing machine works, and ...


12

Unless I'm missing something, it's trivially in P as the length of the formula is exponential in the number of variables. Hence all $2^{n}$ truth assignments can be generated and checked in polynomial time in the length of the formula.


12

If you are referring to the problem of deciding whether a formula given in $2-DNF$ form is satisfiable, then it is in $P$, as well as general $DNF$ satisfiability. Indeed, such a formula is satisfiable iff there is a clause that does not contain an inner contradiction. That is, a clause that does not contain both $p$ and $\neg p$ for some atomic proposition $...


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

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 ...


11

There is no need to simplify the formula, you just evaluate it recursively according to the definition of the boolean operators in use. Let $\varphi$ a boolean formula and $a : X_\varphi \to \{0,1\}$ an assignment of all variables that occur in $\varphi$. Now we define the evaluation function $\operatorname{eval}_a$ on variable-free boolean expressions in ...


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

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 ...


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