The Stack Overflow podcast is back! Listen to an interview with our new CEO.

Tag Info

Hot answers tagged satisfiability

32

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

27

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

24

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 $\... 22 In general, this is a very relevant and interesting research question. "One way is to run existing solvers..." and what would this even tell us exactly? We could see empirically that an instance seems hard for a specific solver or a specific algorithm/heuristic, but what does it really tell about the hardness of the instance? One way that has been pursued ... 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 ... 18 Classic, well-known results As mentioned by Standa Zivny on the related question of CSTheory, Which SAT problems are easy?, there's a well-known result by Schaefer from 1978 (quoting the answer of Zivny): If SAT is parametrised by a set of relations allowed in any instance, then there are only 6 tractable cases: 2-SAT (i.e. every clause is binary), Horn-... 15 I believe 3-SAT was originally reduced from the more general SATISFIABILITY in Karp's paper that outlined 21 NP-complete problems. Wikipedia has a description of how to show that SATISFIABILITY is NP-complete, a result that's known as the Cook-Levin theorem. The idea of this proof is to show that any polynomial time nondeterministic Turing machine can be ... 14 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 ... 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 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, ... 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 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 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 ... 13 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 ... 13$(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$... 12 Isn't the maximum number of satisfied clauses what we're looking for? Yes, we're looking for an assignment that satisfies the maximum number of clauses (that is all of them, preferably). And to that end we ask ourselves "Which single variable will bring us closest to this goal when flipping it?" and then flip it. It seems to me that we're trying to use ... 12 Without loss of generality, we can assume that each variables appears exactly once positively and exactly once negatively (if a variable only appears once set its value to satisfy the clause and remove the clause). We can also assume that a variable does not appear in a clause more than once (if a variable appears both positively and negatively in a clause, ... 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 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 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

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

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

11

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

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

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

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