\(%\usepackage{color}\)
\(%\usepackage{tcolorbox}\)
\(%\tcbuselibrary{skins}\)
\(\usepackage{pifont}\)
\(\)
\(%\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}}\)
\(\)
\(\newcommand{\AAccess}[1]{{\footnotesize[\href{https://libproxy.aalto.fi/login?url=#1}{Aalto lib access}]}}\)
\(%\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=italyGreen!10!white,colframe=italyGreen!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{finnishBlue}#1}}\)
\(\newcommand{\Red}[1]{{\color{italyRed}#1}}\)
\(%\newcommand{\Emph}[1]{\emph{\color{aaltoblue}#1}}\)
\(\newcommand{\Emph}[1]{\emph{\usebeamercolor[fg]{structure} #1}}\)
\(%\newcommand{\Emp}{\usebeamercolor[fg]{structure}}\)
\(\newcommand{\Emp}{\color{italyRed}}\)
\(\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{finnishBlue}\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}}\)
Truth tables
A truth table for a set of formulas over \(n\) variables
is a table that enumerates all the possible truth assignments over the variables
and
the corresponding evaluated values of the formulas in its rows.
In practise,
building truth tables is only applicable for formulas with few variables because a truth table for formulas involving \(n\) variables has \(2^n\) rows.
Example
Consider the formula
\[(a \land b) \Xor \neg c\]
and its non-variable sub-formulas \((a \land b)\) and \(\neg c\).
Let’s build the truth table for them, step-by-step.
We start with the table below that lists in
its rows all the 8 possible value combinations (i.e., truth assignments)
for the variables \(\Set{a,b,c}\) appearing in the formulas.
\begin{array}{ccc|c|c|c@{}}
a & b & c & (a \land b) & \neg c & (a \land b) \Xor \neg c \\ \hline
\False & \False & \False & & & \\
\False & \False & \True & & & \\
\False & \True & \False & & & \\
\False & \True & \True & & & \\
\True & \False & \False & & & \\
\True & \False & \True & & & \\
\True & \True & \False & & & \\
\True & \True & \True & & & \\
\end{array}
Based on the columns for \(a\), \(b\) and \(c\),
it is easy to next evaluate the values in the columns \(a \land b\) and \(\neg c\).
\begin{array}{ccc|c|c|c@{}}
a & b & c & (a \land b) & \neg c & (a \land b) \Xor \neg c \\ \hline
\False & \False & \False & \False & \True & \\
\False & \False & \True & \False & \False & \\
\False & \True & \False & \False & \True & \\
\False & \True & \True & \False & \False & \\
\True & \False & \False & \False & \True & \\
\True & \False & \True & \False & \False & \\
\True & \True & \False & \True & \True & \\
\True & \True & \True & \True & \False & \\
\end{array}
Finally, we can evaluate the values in the column
\((a \land b) \Xor \neg c\) by using the ones in the columns
\((a \land b)\) and \(\neg c\).
\begin{array}{ccc|c|c|c@{}}
a & b & c & (a \land b) & \neg c & (a \land b) \Xor \neg c \\ \hline
\False & \False & \False & \False & \True & \True \\
\False & \False & \True & \False & \False & \False \\
\False & \True & \False & \False & \True & \True \\
\False & \True & \True & \False & \False & \False \\
\True & \False & \False & \False & \True & \True \\
\True & \False & \True & \False & \False & \False \\
\True & \True & \False & \True & \True & \False \\
\True & \True & \True & \True & \False & \True \\
\end{array}
Observe that if we have a truth table for a formula,
then it is easy to manually check whether the formula is satisfiable
(at least one row contains \(\True\) in the column of the formula)
or valid (all rows contain \(\True\)).
For instance,
we see that the formula \((a \land b) \Xor \neg c\) is satisfiable but not valid.
In addition, it is easy to enumerate all its satisfying truth assignments
by using the truth table.