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


20

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


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


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

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


9

One variable: $(A \lor A \lor A)$


5

TL;DR: They differ in their basic input and output. SAT and SMT solvers don't know what programs are; they are tools that answer yes or no questions about mathematical formulas. Symbolic execution, on the other hand, is a method of analyzing programs. Symbolic execution usually relies on SAT and SMT solvers, but not the other way around. SAT and SMT solvers ...


5

There are no competitions targeting general integer programming or mixed integer programming, but there are (or were) benchmarks, such as the MIPLIB (linear) and the MINLPLIB (nonlinear). There are competitions for subsets (PB, SAT, max-SAT) and for constraint programming, as you and other answers pointed out. You can find many competitions (DIMACS ...


5

There are competitions for constraint satisfaction solvers. Some problems there can be readily translated to IP solvers as well. See e.g., MiniZinc challenge which has taken place yearly since 2008 or the XCSP competition.


5

Let me recap the proof. We are given a sparse NP-hard language $A$: for each length $n$, there are at most $n^c$ strings of length $n$ in $A$. For a satisfiable CNF $\varphi$, let $a(\varphi)$ be the lexicographically first satisfying assignment for $\varphi$. We consider the NP language $B$, which consists of all pairs $(\varphi,w)$ such that $\varphi$ is ...


5

You've gotten a number of good answers already so I hesitate to try to contribute more, but I see two more factors that I think make SAT particularly interesting to a lot of people. "Nearly" Polynomial The first factor is the "proximity" between 2SAT and 3SAT. We know how to solve 2SAT problems in polynomial time, and have proven that ...


5

A CNF which is not satisfiable is usually called unsatisfiable. A CNF which is unsatisfiable but becomes satisfiable if we drop any clause is minimally unsatisfiable. Papadimitrious and Wolfe constructed, in their paper The complexity of facets resolved (Lemma 1), a polynomial time reduction $f$ from CNFs to CNFs such that: If $\varphi$ is satisfiable then $...


4

The result you are trying to prove is known as Mahaney's theorem. It is covered by textbooks on complexity theory, and in many online lecture notes. The proof in Jonathan Katz' lecture notes indeed uses LEXSAT.


4

You can always satisfy at least half of clauses: for each variable $x$, find the number of clauses that contain $x$ and the number of clauses that contain $\lnot x$. Select the one which satisfies the most clauses. Remove clauses containing $x$ and $\lnot x$. Repeat for other variables. Since for each $x$ we satisfy at least half of removed clauses, we ...


4

The theory probably depends on the details. In practice, if you're only interested in solving an instance, here are a some thoughts: Most literals should be eliminated in presolve of today's solvers. They eliminate all positive-only (or negative-only) literals. Next, your setup implies that most literals should be set to $true$. Many solvers allow you to ...


4

Usually, when we talk about the complement of a set we have some reference set to compare to. In the setting of languages over some alphabet $\Sigma$, this means that the complement of some language $L$ would be $\overline L = \Sigma^\ast \setminus L$, i.e. the set of all strings over $\Sigma$ which are not in $L$. In the particular case of $$\mathrm{Sat} = \...


4

I don't know precisely how Bob works, but let's talk about clause learning. Suppose you have a set of variable assignments, $A$, say $x_1 = 0$, $x_2 = 1$, $x_3 = 0$. This is a single clause in disjunctive normal form: $$A = \neg x_1 \wedge x_2 \wedge \neg x_3$$ The negation of this set of assignments is a single clause in conjunctive normal form: $$\neg A = ...


3

Lower bound. For $g \le c \cdot \sqrt{\log n}$ there exists a polynomial-time algorithm. The idea is the following: if some clauses have too many variables, then it should be trivial to select some variable to satisfy this clause, without hurting clauses with few variables. We repeat the following: Find the clause with the smallest number of variables. Let $...


3

There was a Pseudo-Boolean solver competition from 2005-2012, but (as far as I can tell) nothing since then. Integer Linear Programming is a subset of Pseudo-Boolean programming. See the 2012 competition page for results and links to other competition results.


3

This sounds to me like the Knapsack problem where $z$ is the weight of each item, $Z$ is the capacity of the knapsack, $g$ the value of the item, and $G$ the value to be achieved. The problem is NP-complete but solvable, using dynamic programming, in pseudo-polynomial time $O(n \cdot W)$ where $W = \max_{(z,g) \in R}(g)$. You can prove that the Knapsack ...


3

No. The gamer will basically have to work out the SAT problem in their head. Think of any video game puzzle you've solved that wasn't easy. You probably solved it by working out a simpler version of the problem and then solving that. If you "complexify" SAT into a video game level, the best way to solve the video game level will be to simplify it ...


3

Just about every puzzle game can be formulated as a 3SAT with a unique solution. Sudoku is perhaps the canonical example.


3

Semiprime factoring. Define an unsigned integer multiplication circuit such that X * Y = P. Define P as a constant equal to an arbitrary semiprime number (there are an infinity of such numbers). Define X and Y as free variables such that they have one less bit than P (to ban the solution 1 * P and P * 1). Add the constraint that X <= Y (to ban the ...


3

You are describing the Resolution refutation system, which is complete in the sense that if a CNF is unsatisfiable, then it can be proven using Resolution. Resolution is also implicitly used in most SAT solvers. The width of a Resolution refutation is the maximal number of literals in a clause encountered during the refutation. There are 3CNFs on $n$ ...


3

You can naively compute ALL-SAT in $2^npoly(n,m)$ time, where $n$ is the number of variables and $m$ is the number of clauses. You clearly need $\Omega(2^n)$ time in the worst case just to write down the assignments (in the case of a tautology). If the strong exponential time hypothesis (SETH) holds, then this is not much harder than SAT itself, so under ...


2

If you want to know whether there exists a general method/algorithm which can convert any given mathematical statement (by which you mean statements written in logic (say first-order logic, second-order logic ... etc)) to a SAT formula which is True iff that statement is True, then the answer is No. The reason being that evaluating whether an SAT formula ...


2

This problem is NP-hard (and in addition hard to approximate and W[1]-hard), because maximum independent set can be reduced to it. Reduction: Each variable represents a vertex and each clause represents an edge.


2

No, you can't. If each clause has at least one positive literal, then, by assigning TRUE to all variables, one gets all clauses satisfied.


2

You're treating resolution as if it were a purely syntactic rule. It works that way with traditional CNF clauses because that corresponds with the underlying rule of inference. But a CNF clause with the added restriction of only one literal allowed to be true no longer corresponds to what the resolution rule can be validly applied to. The Boolean ...


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