\(%\usepackage{color}\) \(%\usepackage{tcolorbox}\) \(%\tcbuselibrary{skins}\) \(\usepackage{pifont}\) \(\) \(\definecolor{fakeaaltobluel}{RGB}{00,141,229} % 0065BD\) \(\definecolor{aaltoblue}{RGB}{00,101,189} % 0065BD\) \(\definecolor{aaltored}{RGB}{237,41,57} % ED2939\) \(\) \(\definecolor{MyBoxBackground}{rgb}{0.98,0.98,1.0}\) \(\definecolor{MyBoxBorder}{rgb}{0.90,0.90,1.0}\) \(\definecolor{backgroundred}{rgb}{1.0,0.98,0.98}\) \(\definecolor{shadowred}{rgb}{1.0,0.90,0.90}\) \(\) \(%\newcommand{\subheading}[1]{\textbf{\large\color{fakeaaltobluel}#1}}\) \(\newcommand{\subheading}[1]{\large{\usebeamercolor[fg]{frametitle}\sc #1}}\) \(\) \(\) \(%\newtcbox{\mybox}[1][red]{on line,arc=0pt,outer arc=0pt,colback=#1!10!white,colframe=#1!50!black,boxsep=0pt,left=1pt,right=1pt,top=2pt,bottom=2pt,boxrule=0pt,bottomrule=1pt,toprule=1pt}\) \(%\newtcbox{\mybox}[1][MyBoxBackground]{on line,arc=0pt,outer arc=0pt,colback=#1!10!white,colframe=#1!50!black,boxsep=0pt,left=1pt,right=1pt,top=2pt,bottom=2pt,boxrule=0pt,bottomrule=1pt,toprule=1pt}\) \(\) \(\newtcolorbox{MyBoxTitled}[1]{colback=MyBoxBackground!100!black,colframe=MyBoxBorder!100!black,boxsep=2pt,left=0pt,right=0pt,top=2pt,bottom=0pt,%enhanced,%\) \( coltitle=red!25!black,title=#1,boxrule=1pt}\) \(\) \(\newtcolorbox{MyBox}[1][]{colback=MyBoxBackground!100!black,colframe=MyBoxBorder!100!black,boxsep=0pt,left=2pt,right=0pt,top=0pt,bottom=0pt,%enhanced,%\) \( coltitle=red!25!black,boxrule=1pt,#1}\) \(\) \(\newenvironment{EqnBox}[1]{\begin{adjustbox}{valign=t}\begin{minipage}{#1}\begin{MyBox}[colback=backgroundred!100!black,colframe=shadowred!100!black]}{\end{MyBox}\end{minipage}\end{adjustbox}}\) \(\) \(\newenvironment{topbox}[1]{\begin{adjustbox}{valign=t}\begin{minipage}{#1}}{\end{minipage}\end{adjustbox}}\) \(\) \(\newcommand{\Blue}[1]{{\color{aaltoblue}#1}}\) \(\newcommand{\Red}[1]{{\color{aaltored}#1}}\) \(%\newcommand{\Emph}[1]{\emph{\color{aaltoblue}#1}}\) \(\newcommand{\Emph}[1]{\emph{\usebeamercolor[fg]{structure} #1}}\) \(%\newcommand{\Emp}{\usebeamercolor[fg]{structure}}\) \(\newcommand{\Emp}{\color{aaltored}}\) \(\newcommand{\TextDef}[1]{{\bf\usebeamercolor[fg]{structure} #1}}\) \(\) \(\newcommand{\todo}[1]{\textbf{\Red{\Pointer #1}}}\) \(\newcommand{\TODO}[1]{\todo{#1}}\) \(\) \(\newcommand{\Pointer}{\raisebox{-1ex}{\huge\ding{43}}\ }\) \(\) \(%\newcommand{\Follows}{\Pointer}\) \(\newcommand{\Follows}{\color{flagblue}\rightsquigarrow}\) \(\newcommand{\Property}{{\color{italygreen}\bf Property}}\) \(\) \(\) \(%\) \(% Common math definitions\) \(%\) \(\newcommand{\Set}[1]{\{#1\}}\) \(\newcommand{\Setdef}[2]{\{{#1}\mid{#2}\}}\) \(\newcommand{\PSet}[1]{\mathcal{P}(#1)}\) \(\newcommand{\Pair}[2]{(#1,#2)}\) \(\newcommand{\Card}[1]{{\vert{#1}\vert}}\) \(\newcommand{\Tuple}[1]{(#1)}\) \(\newcommand{\Seq}[1]{[#1]}\) \(\newcommand{\bbZ}{\mathbb{Z}}\) \(\newcommand{\Ints}{\mathbb{Z}}\) \(\newcommand{\Reals}{\mathbb{R}}\) \(\newcommand{\bbQ}{\mathbb{Q}}\) \(\newcommand{\Rats}{\bbQ}\) \(\) \(\newcommand{\False}{\textsf{F}}\) \(\newcommand{\True}{\textsf{T}}\) \(\) \(\newcommand{\Implies}{\rightarrow}\) \(\newcommand{\Iff}{\leftrightarrow}\) \(%\newcommand{\Implies}{\Rightarrow}\) \(%\newcommand{\Iff}{\Leftrightarrow}\) \(\newcommand{\Xor}{\oplus}\) \(\) \(\newcommand{\Equiv}{\equiv}\) \(\) \(\newcommand{\Oh}[1]{O(#1)}\) \(%\newcommand{\Theta}[1]{\Theta(#1)}\) \(\) \(\newcommand{\PHP}[2]{\mathrm{php}_{#1,#2}}\) \(\newcommand{\PH}[2]{\mathit{x}_{#1,#2}}\) \(\) \(\newcommand{\NP}{\textbf{NP}}\) \(\newcommand{\coNP}{\textbf{co-NP}}\) \(\) \(\newcommand{\bnfdef}{\mathrel{\textup{::=}}}\) \(\newcommand{\bnfor}{\mathrel{\mid}}\) \(\)

\(\newcommand{\Vars}{X}\) \(\newcommand{\VarsOf}[1]{\mathop{vars}(#1)}\) \(\) \(\newcommand{\Bool}{\Bbb{B}}\) \(\) \(\newcommand{\FF}{\bot} % Formula "False"\) \(\newcommand{\TF}{\top} % Formula "True"\) \(%\newcommand{\FF}{\mathbf{F}} % Formula "True"\) \(%\newcommand{\TF}{\mathbf{T}} % Formula "False"\) \(\) \(\newcommand{\LHS}{\alpha}\) \(\newcommand{\RHS}{\beta}\) \(\newcommand{\EHS}{\gamma}\) \(\) \(\newcommand{\Res}[2]{{#1} \otimes {#2}}\) \(\) \(\newcommand{\Gates}{{\mathcal G}}\) \(\newcommand{\Eqns}{{\mathcal D}}\) \(\newcommand{\Circuit}{{\mathcal C}}\) \(\newcommand{\GDef}{\mathrel{\mathrm{:=}}}\) \(\newcommand{\Gate}{g}\) \(\newcommand{\GateL}{g'}\) \(\newcommand{\GateR}{g''}\) \(\newcommand{\GateVar}[1]{v_{#1}}\) \(\newcommand{\ORf}{\mathbf{or}}\) \(\newcommand{\ANDf}{\mathbf{and}}\) \(\newcommand{\NOTf}{\mathbf{not}}\) \(\newcommand{\OR}[1]{\mathbf{or}(#1)}\) \(\newcommand{\AND}[1]{\mathbf{and}(#1)}\) \(\newcommand{\NOT}[1]{\mathbf{not}(#1)}\) \(\newcommand{\FG}{\mathbf{f}} % Input gate "False"\) \(\newcommand{\TG}{\mathbf{t}} % Input gate "True"\) \(\newcommand{\Tseitin}[1]{\mathop{\textrm{cnf}}(#1)}\) \(\newcommand{\Trans}{\mathrel{\rightsquigarrow}}\) \(\) \(\newcommand{\SUD}[3]{x_{#1,#2,#3}}\) \(\newcommand{\SUDClues}{H}\) \(\) \(\newcommand{\PseudoDPLL}{\mathop{\mathit{dpll}}}\) \(\newcommand{\PseudoAsgn}{\mathrel{\leftarrow}}\) \(\newcommand{\PseudoUnsat}{\mathbf{unsat}}\) \(\newcommand{\PseudoSat}{\mathbf{sat}}\) \(\newcommand{\TA}{\tau}\) \(\newcommand{\Undef}{\mathit{undef}}\) \(%\newcommand{\PseudoPropagate}{\textit{propagate}}\)

Propositional formulas: syntax and semantics

In the following, we give a formal description for the syntax and semantics of propositional formulas and define the satisfiability problem.

Syntax

We assume some countable set \( \Vars \), such as \( \Set{a,b,c,…,z,x_1,x_2,…,y_1,y_2,…} \), of Boolean variables. Boolean formulas can then be defined inductively:

• ​ Each Boolean variable in \( \Vars \) is a formula.

• ​ The Boolean constants \( \FF \) and \( \TF \) are formulas.

• ​ If \( \LHS \) and \( \RHS \) are formulas, then so are

  • ​ \( (\neg \LHS) \), the negation of \( \LHS \), read “not \( \LHS \)”,

  • ​ \( (\LHS \land \RHS) \), the conjunction of \( \LHS \) and \( \RHS \), read “\( \LHS \) and \( \RHS \)”,

  • ​ \( (\LHS \lor \RHS) \), the disjunction of \( \LHS \) and \( \RHS \), read “\( \LHS \) or \( \RHS \)”,

  • ​ \( (\LHS \Xor \RHS) \), the exclusive-or of \( \LHS \) and \( \RHS \), read “\( \LHS \) xor \( \RHS \)” or “\( \LHS \) or \( \RHS \) but not both”,

  • ​ \( (\LHS \Implies \RHS) \), the implication, read “\( \LHS \) implies \( \RHS \)”, and

  • ​ \( (\LHS \Iff \RHS) \), the bi-implication between \( \LHS \) and \( \RHS \), “\( \LHS \) if and only if \( \RHS \)”.

• ​ (There are no other formulas.)

Example

• ​ \( a \), \( b \), \( (\neg b) \), \( (a \land (\neg b)) \), and \( ((a \land (\neg b)) \Implies ((\neg a) \lor c)) \) are formulas, but

• ​ \( a \land \Implies b \) is not.

One usually defines the following precedence, from the strongest to the weakest, between the operators: \( \neg \), \( \land \), \( \lor \), \( \Xor \), \( \Implies \), \( \Iff \). Parentheses can then be omitted if the precedence makes the reading of the formula unambiguous (but use parentheses when in doubt!).

Example

\( {a \land \neg b} \Implies {\neg a \lor c} \) means \( ((a \land (\neg b)) \Implies ((\neg a) \lor c)) \).

Furthermore,

• ​ the operators \( \land \), \( \lor \), and \( \Xor \) are associative and commutative: \( a \lor b \lor c \) is the same as \( (a \lor b) \lor c \) and \( a \lor (b \lor c) \).

• ​ \( \Implies \) is right-associative: \( a \Implies b \Implies c \) means \( a \Implies (b \Implies c) \).

• ​ \( \Iff \) is left-associative and commutative: \( a \Iff b \Iff c \) means \( (a \Iff b) \Iff c \).

• ​ \( \bigvee_{i \in I} x_i \) means \( (x_{i_1} \lor … \lor x_{i_n}) \) and \( \bigwedge_{i \in I} x_i \) means \( (x_{i_1} \land … \land x_{i_n}) \) for any finite index set \( I = \Set{i_1,…,i_n} \).

Example

\( \bigvee_{i \in [1..3]}\bigwedge_{j \in [1..2]} x_{i,j} \) means \( (x_{1,1} \land x_{1,2}) \lor (x_{2,1} \land x_{2,2}) \lor (x_{3,1} \land x_{3,2}) \)

Semantics

For a formula \( \phi \), let \( \VarsOf{\phi} \) be the set of variables occurring in it. A truth assignment for \( \phi \) is a function \( \TA : \VarsOf{\phi} \to \Set{\False, \True} \), meaning that it associates each variable in the formula to a truth value \( \False \) (read “false”) or \( \True \) (read “true”). A truth assignment \( \TA \) on the variables can be extended to formulas inductively:

• ​ \( \TA(\FF) = \False \) and \( \TA(\TF) = \True \)

• ​ \( \TA((\neg \LHS)) = \True \) iff \( \TA(\LHS) = \False \)

• ​ \( \TA((\LHS \land \RHS)) = \True \) iff \( \TA(\LHS) = \True \) and \( \TA(\RHS) = \True \)

• ​ \( \TA((\LHS \lor \RHS)) = \True \) iff \( \TA(\LHS) = \True \) or \( \TA(\RHS) = \True \)

• ​ \( \TA((\LHS \Xor \RHS)) = \True \) iff either \( \TA(\LHS) = \True \) or \( \TA(\RHS) = \True \) but not both

• ​ \( \TA((\LHS \Implies \RHS)) = \True \) iff \( \TA(\LHS) = \False \) or \( \TA(\RHS) = \True \)

• ​ \( \TA((\LHS \Iff \RHS)) = \True \) iff \( \TA(\LHS) = \TA(\RHS) \)

Example

For the formula \( a \Iff (a \Xor b) \), the truth assignment \( \TA = \Set{a \mapsto \True, b \mapsto \False} \) evaluates the sub-formulas so that \( \TA(a \Xor b) = \True \) and \( \TA(a \Iff (a \Xor b)) = \True \).

The truth assignment \( \TA = \Set{a \mapsto \True, b \mapsto \True} \) evaluates the sub-formulas to \( \TA(a \Xor b) = \False \) and \( \TA(a \Iff (a \Xor b)) = \False \).

Satisfiability and validity

A formula \( \phi \) is satisfiable if there exists at least one truth assignment \( \TA \) such that \( \TA(\phi) = \True \). Such an assignment is also called a satisfying truth assignment (or model) for \( \phi \). If \( \phi \) is not satisfiable, it is called unsatisfiable.

Example

The formula \( (a \lor b) \land (a \Implies c) \land (b \Implies \neg c) \) is satisfiable as both \( \Set{a \mapsto \True, b \mapsto \False, c \mapsto \True} \) and \( \Set{a \mapsto \False, b \mapsto \True, c \mapsto \False} \) evaluate it to true.

On the other hand, the formula \( (a \land b) \land (a \Implies c) \land (b \Implies \neg c) \) is unsatisfiable.

The propositional satisfiability problem is the following computational problem:

Problem: Propositional satisfiability (SAT)

Instance: A propositional formula \( \phi \).

Question: Is \( \phi \) satisfiable?

A tool that solves the satisfiability problem is called a SAT solver.

Such a tool takes a propositional formula \( \phi \) as an input and then decides whether the formula is satisfiable or not. In addition to a simple “sat” (meaning “yes”) or “unsat” (meaning “no”) answer, a SAT solver usually also provides a satisfying truth assignment when the formula is satisfiable. If the formula is unsatisfiable, some solvers are also able to provide a machine verifiable proof of this. Such a proof is expressed in some proof system such as resolution (see The resolution proof system section) or an extension of it.

A formula \( \phi \) is valid if \( \TA(\phi) = \True \) for all truth assignments \( \TA \) for \( \phi \), meaning that there are no truth assignments that would evaluate the formula to false. Obviously, a formula \( \phi \) is valid if and only if its negation \( \neg\phi \) is unsatisfiable.

Example

The formula \( (a \lor b) \land (a \Implies c) \land (b \Implies \neg c) \) is not valid as, for instance, \( \Set{a \mapsto \True, b \mapsto \False, c \mapsto \False} \) evaluates it to false.

On the other hand, the formula \( \neg((a \land b) \land (a \Implies c) \land (b \Implies \neg c)) \) is valid.

Logical consequences and equivalence

A formula \( \RHS \) is a logical consequence of a formula \( \LHS \), denoted by \( \LHS \models \RHS \), if for all truth assignments \( \TA: (\VarsOf{\LHS} \cup \VarsOf{\RHS}) \to \Set{\False, \True} \) it holds that if \( \TA(\LHS) = \True \), then \( \TA(\RHS) = \True \). That is, \( \LHS \models \RHS \) if \( \RHS \) evaluates to true whenever \( \LHS \) does.

Example

• ​ \( (a \lor \neg b) \land (\neg a \lor c) \models (\neg b \lor c) \)

• ​ \( (a \lor \neg b) \land (\neg a \lor c) \not\models (\neg b) \)

Formula \( \LHS \) and \( \RHS \) are logically equivalent, denoted by \( \LHS \Equiv \RHS \), if for all truth assignments \( \TA: (\VarsOf{\LHS} \cup \VarsOf{\RHS}) \to \Set{\False, \True} \) it holds that \( \TA(\LHS) = \TA(\RHS) \).

Example

\( (a \Implies b \lor c) \land (\neg a \Implies b \lor c) \) and \( b \lor c \) are logically equivalent.

Observe that \( \LHS \) and \( \RHS \) are logically equivalent iff \( \LHS \Iff \RHS \) is valid iff \( \LHS \Xor \RHS \) is unsatisfiable. The following lists some commonly applied logical equivalences, some others can be found this wikipedia page.

• ​ Identity laws: \( \LHS \land \True \Equiv \LHS \) and \( \LHS \lor \False \Equiv \LHS \)

• ​ Domination laws: \( \LHS \land \False \Equiv \False \) and \( \LHS \lor \True \Equiv \True \)

• ​ Double negation law: \( \neg(\neg \LHS) \Equiv \LHS \)

• ​ Negation laws: \( \LHS \land \neg \LHS \Equiv \False \) and \( \LHS \lor \neg \LHS \Equiv \True \)

• ​ De Morgan’s laws: \( (\LHS \lor \RHS) \Equiv \neg(\neg \LHS \land \neg \RHS) \) and \( (\LHS \land \RHS) \Equiv \neg(\neg \LHS \lor \neg \RHS) \).

• ​ Distributive laws: \( \LHS \lor (\RHS_1 \land \RHS_2) \Equiv (\LHS \lor \RHS_1) \land (\LHS \lor \RHS_2) \) and \( \LHS \land (\RHS_1 \lor \RHS_2) \Equiv (\LHS \land \RHS_1) \lor (\LHS \land \RHS_2) \)

• ​ \( (\LHS \Implies \RHS) \Equiv (\neg \LHS \lor \RHS) \)

• ​ \( (\LHS \Iff \RHS) \Equiv \neg(\LHS \Xor \RHS) \)

• ​ \( \LHS \land (\LHS \Implies \RHS) \Equiv \LHS \land \RHS \)

• ​ \( (\LHS_1 \land … \land \LHS_k) \Implies (\RHS_1 \lor … \lor \RHS_m) \Equiv (\neg \LHS_1 \lor … \lor \neg \LHS_k \lor \RHS_1 \lor … \lor \RHS_m) \)

As we will see later, logical equivalences can be used to transform formulas to others as we can substitute sub-formulas with equivalent ones.

Example

The formula \( a \land (\neg a \lor (b \Iff c)) \land \neg(a \land \neg(b \Xor c)) \) can be simplified to

1. \( a \land (a \Implies (b \Iff c)) \land \neg(a \land \neg(b \Xor c)) \) by using the equivalence \( (\LHS \Implies \RHS) \Equiv (\neg \LHS \lor \RHS) \),

2. \( a \land (b \Iff c) \land \neg(a \land \neg(b \Xor c)) \) by using \( \LHS \land (\LHS \Implies \RHS) \Equiv \LHS \land \RHS \),

3. \( a \land (b \Iff c) \land \neg(\neg(\neg a \lor \neg(\neg(b \Xor c)))) \) by using De Morgan’s law,

4. \( a \land (b \Iff c) \land (\neg a \lor (b \Xor c)) \) by using the double negation law,

5. \( a \land (b \Iff c) \land (a \Implies (b \Xor c)) \) by using the equivalence \( (\LHS \Implies \RHS) \Equiv (\neg \LHS \lor \RHS) \),

6. \( a \land (b \Iff c) \land (b \Xor c) \) by using \( \LHS \land (\LHS \Implies \RHS) \Equiv \LHS \land \RHS \),

7. \( a \land \neg(b \Xor c) \land (b \Xor c) \) by using \( (\LHS \Iff \RHS) \Equiv \neg(\LHS \Xor \RHS) \)

8. \( a \land \False \) by using the negation law, and

9. \( \False \) by the domination law.

Thus the original formula is unsatisfiable.