\(%\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}}\)
Overview
As our first constraint language, we’ll use
propositional satisfiability (SAT).
The SAT problem is the first problem proven to be NP-complete [Cook1971].
It has been studied intensively during the last decades,
in both theory and practice view points.
Highly efficient SAT solvers,
that can solve many problem instances with hundreds of thousands of variables
and millions of constraints, exist.
However, due to the nature of NP-complete problems,
on some hand-crafted instances with only hundreds of variables,
the very same solvers can fail badly,
meaning that their running times are so large that they do not terminate in practise.
High-level outline:
Round 1:
Propositional formulas, satisfiability
Problem solving with SAT solvers
Truth tables and normal forms
Round 2: