\(%\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.