\(%\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}}\)

References

Cook1971

Stephen A. Cook: The Complexity of Theorem-Proving Procedures, Proc. ACM STOC 1971, pages 151–158. ACM, 1971.

DavisEtAl1962

Martin Davis, George Logemann, and Donald W. Loveland: A machine program for theorem-proving. Communications of the ACM 5(7): 394–397, 1962.

DavisPutnam1960

Martin Davis and Hilary Putnam: A Computing Procedure for Quantification Theory. Journal of the ACM 7(3):201–215, 1960.

Haken1985

Armin Haken: The Intractability of Resolution. Theoretical Computer Science 39:297–308, 1985.

Kullmann1999

Oliver Kullmann: On a Generalization of Extended Resolution. Discrete Applied Mathematics 96–97:149–176, 1999.

PipatsrisawatDarwiche2011

Knot Pipatsrisawat and Adnan Darwiche: On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence 175(2):512–525, 2011.