In mathematical logic satisfiability of an expression indicates if there exists an assignment of values, or simply, an input for which such expression yields a particular result. As I like to think about it, it is a logic generalization of the common concept of solving an equation. Determining if a formula is satisfiable is a decidable problem but computationally hard. In this article we are going to focus on boolean satisfiability, which to my knowledge, is the most studied problem in computer science. It is not a purely theoretical concept, it has industrial application and it has potential to inspire you for more projects and perhaps help you solve problems in projects you are already working on. We already did demonstrate solving graph problems finds use in level design in games, same could be true for boolean satisfiability or simply SAT\text{SAT} problem.

An instance of such problem is a boolean formula expressions written in conjunctive normal form or a clausal form meaning it is a conjunction of clauses and each clause is a disjunction of literals.

Φ(x1xN)=CkC(Φ)(lCkl)(SAT)\Phi(x_1 \dots x_N) = \bigwedge\limits_{\mathfrak{C}_k \in \mathfrak{C}(\Phi)} ( \bigvee\limits_{l \in \mathfrak{C}_k} l ) \tag{SAT} CkC(Φ),lCk,l{xn1nN}{¬xn1nN}\forall \mathfrak{C}_k \in \mathfrak{C}(\Phi), \forall l \in \mathfrak{C}_k, l \in \{x_n \vert 1 \leq n \leq N \} \cup \{ \neg x_n \vert 1 \leq n \leq N\}

A conjunction is logical AND operation denoted above as \wedge and disjunction is logical OR operation denoted as \vee. Parentheses indicate clauses which consist of literals where a literal is a symbol pointing a variable or negation of variable. For the CNF expression Φ\Phi I picked a set-theoretical description which denotes the set of clauses C(Φ)\mathfrak{C}(\Phi) in which clauses are sets of literals CkC(Φ)\mathfrak{C}_k \in \mathfrak{C}(\Phi). It is allowed to have more literals than variables.

The easiest way to get started is by playing with small examples. For instance, a Φ\Phi expression is an instance of 3SAT\text{3SAT} problem when Ck=3,CkC(Φ)\vert \mathfrak{C}_k \vert = 3, \forall \mathfrak{C}_k \in \mathfrak{C}(\Phi). Such formula has exactly three literals per clause.

Φ1=(x1¬x2x3)(x1x2¬x3)(¬x1¬x2x3)\begin{aligned} \Phi_1 &= (x_1 \vee \neg x_2 \vee x_3) \wedge (x_1 \vee x_2 \vee \neg x_3) \wedge (\neg x_1 \vee \neg x_2 \vee x_3) \end{aligned}

Let us computationally solve, personally I use the MergeSat solver. First we write Φ1\Phi_1 in .cnf format which is accepted by the solver. Each line ends with 0, negative numbers are negations, each line is a clause except for first line which indicates the CNF form with number of variables and number of clauses.

p cnf 3 3
1 -2 3 0
1 2 -3 0
-1 -2 3 0

The CNF formula Φ1\Phi_1 is satisfiable, output from Mergesat indicating this as well as assignment of values to variables x1=1,x2=0,x3=0x_1 = 1, x_2 = 0, x_3 = 0 can be found in the MergeSat output. Of course this does not have to be the only solution that satisfies Φ1\Phi_1. Now, for contrast, let us consider Φ2\Phi_2 which will involve two variables and four clauses.

Φ2=(x1x2)(x1¬x2)(¬x1x2)(¬x1¬x2)\begin{aligned} \Phi_2 &= (x_1 \vee x_2) \wedge (x_1 \vee \neg x_2) \wedge (\neg x_1 \vee x_2) \wedge (\neg x_1 \vee \neg x_2) \end{aligned}
p cnf 2 4
1 2 0
1 -2 0
-1 2 0
-1 -2 0

Unlike in case of the previous form, the Φ2\Phi_2 is not satisfiable which is indicated by the MergeSat output. It can also be deduced intuitively by looking at clauses of Φ2\Phi_2, they list all the possible assignments of values for two boolean variables making it not possible to satisfy a clause without violating another. It is also worth noting that the 2SAT\text{2SAT} problem can be efficiently solved in polynomial time (linear) as it is a special case of SAT\text{SAT} (Krom, 1967; Aspvall, Plass, & Tarjan, 1979; Even, Itai, & Shamir, 1976)

For now let us ommit the CNF form and define the circuit satisfiability problem in a similar way, a boolean formula Φcircuit(x1xN)\Phi_\text{circuit}(x_1 \dots x_N) is a word of a formal context-free grammar of a form reassembling to the syntax trees involving boolean operators \wedge, \vee and ¬\neg with literals as terminal symbols. Formal language is defined by a quadruple (V,N,,S)(V, N, {, S}) where NN is a finite set of non-terminal symbols, VV is a finite set of terminal symbols, PP is a set of production rules and finally SS is the start symbol.

G=(V,N,P,S)N={S}V={xn1nN}{¬,,,(,)}P={S(SS),S(SS),S¬S}{Sxn1nN}S={S}(CSAT grammar)\begin{aligned} G &= (V, N, P, S) \tag{CSAT grammar} \\ N &= \{\mathfrak{S}\} \\ V &= \{x_n \vert 1 \leq n \leq N \} \cup \{ \neg, \vee, \wedge, (, )\}\\ P &= \{\mathfrak{S} \rightarrow (\mathfrak{S} \wedge \mathfrak{S}), \mathfrak{S} \rightarrow (\mathfrak{S} \vee \mathfrak{S}), \mathfrak{S} \rightarrow \neg \mathfrak{S} \} \cup \{ \mathfrak{S} \rightarrow x_n \vert 1 \leq n \leq N \} \\ S &= \{\mathfrak{S}\} \end{aligned}

Worth noting that CSAT\text{CSAT} is a generalization of SAT\text{SAT} meaning that every possible Φ(x1xN)\Phi(x_1 \dots x_N) is a word of CSAT grammar\text{CSAT grammar} and this is because every boolean formula in conjunctive normal form forms a valid syntax tree described by the CSAT grammar\text{CSAT grammar}.

simplest satisfiability circuits
Φ3=(x1x2)Φ4=(x1¬x1)\begin{aligned} \Phi_3 &= ( x_1 \wedge x_2) \\ \Phi_4 &= ( x_1 \wedge \neg x_1) \end{aligned}

The circuit Φ3\Phi_3 is satisfied by an assignment of values to variables x1=x2=1x_1 = x_2 = 1. In the case of Φ4\Phi_4 which involves only a single boolean variable x1x_1 and none of its values satisfies the circuit.

The SAT\text{SAT} problem might be the most studied problem so far, the number of available solvers and heuristics is vast and it makes it attractive to formalize our formal satisfaction problems as SAT\text{SAT} formulas and take advantage of decades of research and use those solvers to process them efficiently. What about the CSAT\text{CSAT}? We made a formal argument that every SAT\text{SAT} is CSAT\text{CSAT} but what about the other way around?

We could apply DeMorgan’s Law and the distributive property to simplify formula generated by the CSAT grammar\text{CSAT grammar} and eventually rewriting it into CNF form. This unforuntately could lead to exponential growth of formula size. This is where the discovery of Tseytin Transformation (Tseitin, 1983) which is an efficient way of converting disjunctive normal form DNF into conjuctive normal form CNF. We can imagine a sequence of algebraic transformations such as variables substitutions in order to translate an arbitrary Φcircuit(x1xN)\Phi_\text{circuit}(x_1 \dots x_N) into Φ(x1xN)\Phi(x_1 \dots x_N). Problem with that is the number of involved variables would grow quadratically and this is an NP-Complete problem, every extra variable is increasing the number of required steps to solve by an order of magnitude. The advantage of Tseytin Transformation is that CNF formula grows linearly compared to input CSAT\text{CSAT} instance expression. It consists of assigning outputs variables to each component of the circuit and rewriting them according to the following rules of gate sub-expressions.

AB=C(¬A¬BC)(A¬C)(B¬C)A+B=C(AB¬C)(¬AC)(¬BC)¬A=C(¬A¬C)(AC)(Tseytin)\begin{aligned} A \cdot B = C &\equiv (\neg A \vee \neg B \vee C) \wedge (A \vee \neg C) \wedge (B \vee \neg C) \\ A + B = C &\equiv (A \vee B \vee \neg C) \wedge (\neg A \vee C) \wedge (\neg B \vee C) \\ \neg A = C &\equiv (\neg A \vee \neg C) \wedge (A \vee C) \tag{Tseytin} \end{aligned}

Where AB=CA \cdot B = C, A+B=CA + B = C and ¬A=C\neg A = C are AND\text{AND}, OR\text{OR} and NOT\text{NOT} classical gates with CC as a single output. I will not provide a rigorous proof for those sub-expressions, rather provide some intuition, which is if we think of satisfying all the clauses then each of the gate sub-expressions becomes a logic description of the gate consisting of relevant cases, which are clauses, of how the inputs A,BA, B affect the output CC. Let us analyse clasuses of the AND\text{AND} gate. Clause (¬A¬BC)(\neg A \vee \neg B \vee C) indicates that if both AA and BB are true, then the only way to satisfy this clause is to assign CC to true as well, which already seems to implement AND\text{AND} pretty well. The remaining case to ensure is enforcing CC to false when at least one of inputs is false and this is done by clauses (A¬C)(B¬C)(A \vee \neg C) \wedge (B \vee \neg C).

Let us examine an example of CSAT\text{CSAT} circuit converted into SAT\text{SAT} problem using Tseytin transformation. The example circuit consists of three inputs x1,x2,x3x_1, x_2, x_3, a single output yy and seven logic gates. Circuit takes the following form.

satisfiability circuit

Note that one of the gates has two outputs. Formula corresponding to this circuit can be written in a predicate form which is recognizable by the CSAT grammar\text{CSAT grammar} which is no longer in CNF form.

Φ5=(((¬x1x2)(x1¬x2))(¬x2x3))\begin{aligned} \Phi_5 &= ( ( ( \neg x_1 \wedge x_2 ) \vee ( x_1 \wedge \neg x_2 ) ) \vee ( \neg x_2 \wedge x_3 ) ) \end{aligned}

Applying the Tseytin transformation to this circuit leads to expression with more variables but in conjunctive normal form. It requires to apply the gate sub-expressions to each of gates of the circuit leading us to following CNF form.

ΦN1=(z1x1)(¬z1¬x1)ΦN2=(z2x2)(¬z2¬x2)(z3x2)(¬z3¬x2)ΦA1=(¬z1¬x2z4)(z1¬z4)(x2¬z4)ΦA2=(¬x1¬z2z5)(x1¬z5)(z2¬z5)ΦA3=(¬z3¬x3z6)(z3¬z6)(x3¬z6)ΦR1=(z4z5¬z7)(¬z4z7)(¬z5z7)ΦR2=(z7z6¬y)(¬z7y)(¬z6y)\begin{aligned} \Phi_\text{N1} &= (z_1 \vee x_1) \wedge (\neg z_1 \vee \neg x_1) \\ \Phi_\text{N2} &= (z_2 \vee x_2) \wedge (\neg z_2 \vee \neg x_2) \wedge (z_3 \vee x_2) \wedge (\neg z_3 \vee \neg x_2) \\ \Phi_\text{A1} &= (\neg z_1 \vee \neg x_2 \vee z_4) \wedge (z_1 \vee \neg z_4) \wedge (x_2 \vee \neg z_4) \\ \Phi_\text{A2} &= (\neg x_1 \vee \neg z_2 \vee z_5) \wedge (x_1 \vee \neg z_5) \wedge (z_2 \vee \neg z_5) \\ \Phi_\text{A3} &= (\neg z_3 \vee \neg x_3 \vee z_6) \wedge (z_3 \vee \neg z_6) \wedge (x_3 \vee \neg z_6) \\ \Phi_\text{R1} &= (z_4 \vee z_5 \vee \neg z_7) \wedge (\neg z_4 \vee z_7) \wedge (\neg z_5 \vee z_7) \\ \Phi_\text{R2} &= (z_7 \vee z_6 \vee \neg y) \wedge (\neg z_7 \vee y) \wedge (\neg z_6 \vee y) \end{aligned}

Each of ΦN1,ΦN2ΦR2\Phi_\text{N1}, \Phi_\text{N2} \dots \Phi_\text{R2} is an individual CNF form corresponding to particular gate of the circuit. The penalty for such convenient notation is in the extra variables ziz_i that have to be introduced. We can assemble those forms into Φ4Φ4\Phi_4^\prime \equiv \Phi_4 and the cnf file is also provided.

Φ5=ΦN1ΦN2ΦA1ΦA2ΦA3ΦR1ΦR2(y)\begin{aligned} \Phi_5 &= \Phi_\text{N1} \wedge \Phi_\text{N2} \wedge \Phi_\text{A1} \wedge \Phi_\text{A2} \wedge \Phi_\text{A3} \wedge \Phi_\text{R1} \wedge \Phi_\text{R2} \wedge (y) \end{aligned}

This circuit outputs true if given one of the following four inputs (x1,x2,x3){(0,0,1),(0,1,0),(1,0,0),(1,0,1),(0,1,1)}(x_1, x_2, x_3) \in \{(0, 0, 1), (0, 1, 0), (1, 0, 0), (1, 0, 1), (0, 1, 1)\}. We can enumerate all the solutions by appending a clause that is invalid if given a previous solution until the formula becomes unsatisfiable. For instance if we append clauses (x1x2¬x3)(x1¬x2x3)(¬x1x2x3)(x_1 \vee x_2 \vee \neg x_3) \wedge (x_1 \vee \neg x_2 \vee x_3) \wedge (\neg x_1 \vee x_2 \vee x_3) we will get the following form.

Φ5=ΦN1ΦN2ΦA1ΦA2ΦA3ΦR1ΦR2(y)(x1x2¬x3)(x1¬x2x3)(¬x1x2x3)\begin{aligned} \Phi_5^\prime &= \Phi_\text{N1} \wedge \Phi_\text{N2} \wedge \Phi_\text{A1} \wedge \Phi_\text{A2} \wedge \Phi_\text{A3} \wedge \Phi_\text{R1} \wedge \Phi_\text{R2} \wedge (y) \wedge (x_1 \vee x_2 \vee \neg x_3) \wedge (x_1 \vee \neg x_2 \vee x_3) \wedge (\neg x_1 \vee x_2 \vee x_3) \end{aligned}

Which is satisfiable only by solutions (x1,x2,x3){(1,0,1),(0,1,1)}(x_1, x_2, x_3) \in \{(1, 0, 1), (0, 1, 1)\} as assignments {(0,0,1),(0,1,0),(1,0,0)}\{(0, 0, 1), (0, 1, 0), (1, 0, 0)\} have been excluded by the appended clauses. Following this logic the following formula includes clauses from all the solutions and is unsatisfiable. The formula file is also provided.

Φ5=ΦN1ΦN2ΦA1ΦA2ΦA3ΦR1ΦR2(y)(x1x2¬x3)(x1¬x2x3)(¬x1x2x3)(¬x1x2¬x3)(x1¬x2¬x3)\begin{aligned} \Phi_5^{\prime\prime} = &\Phi_\text{N1} \wedge \Phi_\text{N2} \wedge \Phi_\text{A1} \wedge \Phi_\text{A2} \wedge \Phi_\text{A3} \wedge \Phi_\text{R1} \wedge \Phi_\text{R2} \wedge (y) \\ &\wedge (x_1 \vee x_2 \vee \neg x_3) \wedge (x_1 \vee \neg x_2 \vee x_3) \wedge (\neg x_1 \vee x_2 \vee x_3) \wedge (\neg x_1 \vee x_2 \vee \neg x_3) \wedge (x_1 \vee \neg x_2 \vee \neg x_3) \end{aligned}

Let Φ(x1xN)\Phi(x_1 \dots x_N) be an arbitrary SAT\text{SAT} instance formula and we want to find an instance of (MIS)(\text{MIS}) maximum independent set as defined in Vertex Covers and Independent Sets in game level design. We know both of those problems are NP-Complete thus by (Karp, 1972) there must exist a transformation, or a polynomial reduction which transforms one instance into another in polynomial number of steps in terms of data size. As a brief reminder, the target instance of (MIS)(\text{MIS}) takes form of a graph G=(E(G),V(G))G = (E(G), V(G)) where E(G)E(G) is set of edges of GG and V(G)V(G) is a set of vertices of GG. We construct GG from Φ(x1xN)\Phi(x_1 \dots x_N) according to the following definition.

G=(E,V)E={{lα,lβ}(CkC(Φ),{lα,lβ}Ck)(Ck,CkC(Φ),kk,lαCk,lβCk,lα=¬lβ)}V={lkmlkmCk,CkC(Φ)}\begin{aligned} G &= (E, V) \\ E &= \{\{l_\alpha, l_\beta\} \vert (\exists \mathfrak{C}_k \in \mathfrak{C}(\Phi), \{l_\alpha, l_\beta\} \subseteq \mathfrak{C}_k) \vee (\exists \mathfrak{C}_k, \mathfrak{C}_{k^\prime} \in \mathfrak{C}(\Phi), k \neq k^\prime, l_\alpha \in \mathfrak{C}_k, l_\beta \in \mathfrak{C}_{k^\prime}, l_\alpha = \neg l_\beta)\} \\ V &= \{l_{km} \vert l_{km} \in \mathfrak{C}_k, \forall \mathfrak{C}_k \in \mathfrak{C}(\Phi) \} \end{aligned}

If the maximum independent set of the graph described above is of size equal to number of clauses of the CNF formula Φ(x1xN)\Phi(x_1 \dots x_N) then Φ\Phi is satisfiable, i.e C(Φ)=VMIS(G)\vert \mathfrak{C}(\Phi) \vert = V_\text{MIS}(G). Reason for that is all the literals inside of clause are coupled together making it impossible to select more than one vertex without violating the independent set constraint. The lowest number of violations is zero and this corresponds to exactly one literal per clause.

Reduction from SAT to MIS

The process illustrated on figure above consisists of assigning a graph vertex for each literal, then connecting the vertices corresponding to literals of same clasuses with an edge - this creates the clause clusters. Then we join with an edge all vertices corresponding to negation of corresponding variables, those we call conflict links. The graph obtained from the method above can be re-arranged for better aesthetics.

Reduction from SAT to MIS

If you read the Vertex Covers and Independent Sets in game level design article you know that maximum independent set problem is semantically equivalent to minimum vertex cover problem thus this reduction can be treated as reduction to either of those problems. Moreover, if you checked the using Quantum Adiabatic Optimization article you know that such problem could be solved using a quantum adiabatic processor, which already reveals one of possible options of solving SAT\text{SAT} problems using a quantum machine.

We also can connect this problem to our constraint programming post. The CSAT\text{CSAT} is essentially a predicat and could implement a constraint. Thus an instance of CSP\text{CSP} could be used to design a boolean circuit which is satisfied when the CSP\text{CSP} instance is satisfied, then via Tseytin transformation we can convert it to CNF formula and even reduce to MIS\text{MIS} instance. As long as the domains of variables of your CSP\text{CSP} are boolean this should be relatively straightforward process, but once your constraints involve integer domain your circuits would start to look like computer processor circuits, they would involve arithmetic-logic components and grow beyond what is currently trackable.

Another interesting thing we can think about is, as the SAT\text{SAT} and CSAT\text{CSAT} instances are described using a context-free grammar CSAT grammar\text{CSAT grammar} determining if any Φ\Phi is an instance of boolean satisfiability can be done efficiently by checking if Φ\Phi is a word described by CSAT grammar\text{CSAT grammar}. Yet if we introduce a subtle change in the definition and claim that CSAT grammar\text{CSAT grammar} describes only formulas Φ\Phi^\prime which are satisfiable, suddenly checking if Φ\Phi is a word of this grammar becomes computationally hard problem. My conclusion from this is quite direct and philosophical - that finding an example of a hard problem is equivalent of solving a hard problem.

This blog post barely scratches the surface of decades of research on the concept of satisfiability and logic programming, but it does provide the necessary definitions and gives us foundations to proceed to many other interesting concepts. One possible direction I consider at the moment of writing this post are hashing functions, cryptography and blockchains, another one is computational complexity theory and yet another one is formalizing satisfiability of circuits from category-theoretical perspective. If you have any preferences regarding the direction this blog goes or if you have any questions or find errors or typos please do not hesitate to let me know via Twitter or GitHub. All the .cnf files from this post are available in this public gist repository.

  1. Krom, M. R. (1967). The Decision Problem for a Class of First-Order Formulas in Which all Disjunctions are Binary. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 13(1-2), 15–20. 10.1002/malq.19670130104
  2. Aspvall, B., Plass, M. F., & Tarjan, R. E. (1979). A linear-time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters, 8(3), 121–123. 10.1016/0020-0190(79)90002-4
  3. Even, S., Itai, A., & Shamir, A. (1976). On the Complexity of Timetable and Multicommodity Flow Problems. SIAM Journal on Computing, 5(4), 691–703. 10.1137/0205048
  4. Tseitin, G. S. (1983). On the Complexity of Derivation in Propositional Calculus. In J. H. Siekmann & G. Wrightson (Eds.), Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970 (pp. 466–483). Berlin, Heidelberg: Springer Berlin Heidelberg. 10.1007/978-3-642-81955-1_28
  5. Karp, R. (1972). Reducibility among combinatorial problems. In R. Miller & J. Thatcher (Eds.), Complexity of Computer Computations (pp. 85–103). Plenum Press.

[Back to Top]