\(%\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} #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{\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}}\ }\)
\(\)
\(\)
\(%\)
\(% 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{\bbN}{\mathbb{N}}\)
\(\newcommand{\Nats}{\bbN}\)
\(\)
\(\newcommand{\Floor}[1]{\lfloor #1 \rfloor}\)
\(\newcommand{\Ceil}[1]{\lceil #1 \rceil}\)
\(\)
\(\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{\Def}{\mathrel{:=}}\)
\(\)
\(\newcommand{\LSF}{\alpha}\)
\(\newcommand{\RSF}{\beta}\)
\(\newcommand{\SF}{\phi}\)
\(\newcommand{\MF}{\gamma}\)
\(%\newcommand{\Abbrv}{\equiv}\)
\(\newcommand{\Abbrv}{\Def}\)
\(\newcommand{\AbbrvEq}{\equiv}\)
\(\newcommand{\Exists}[2]{\exists{#1}.\,#2}\)
\(%\newcommand{\E}[3]{\exists{#1{:}#2}.\,#3}\)
\(\newcommand{\E}[3]{\exists{#1{:}\,#3}}\)
\(\newcommand{\Forall}[2]{\forall{#1}.\,#2}\)
\(%\newcommand{\Furall}[3]{\forall{#1{:}#2}.\,#3}\)
\(%\newcommand{\A}[3]{\forall{#1{:}#2}.\,#3}\)
\(\newcommand{\A}[3]{\forall{#1{:}\,#3}}\)
\(\newcommand{\Models}{\models}\)
\(\newcommand{\NotModels}{\not\models}\)
\(\)
\(\newcommand{\Substf}[3]{#1[#2 \mapsto #3]}\)
\(\newcommand{\Functions}[2]{[#1 \to #2]}\)
\(\)
\(\)
\(\newcommand{\Eq}{\approx}\)
\(\newcommand{\EqS}[1]{\approx_{#1}}\)
\(\newcommand{\Neq}{\not\approx}\)
\(\)
\(%\newcommand{\Th}{\mathcal{T}}\)
\(\newcommand{\Th}{T}\)
\(\newcommand{\ThI}[1]{\Th_{#1}}\)
\(\)
\(\newcommand{\Sig}{\Sigma}\)
\(\newcommand{\SigI}[1]{\Sigma_{#1}}\)
\(\newcommand{\Interp}{I}\)
\(%\newcommand{\Interp}{{\mathcal{I}}}\)
\(\newcommand{\InterpOf}[1]{#1^\Interp}\)
\(\newcommand{\InterpIOf}[2]{#2^{#1}}\)
\(\newcommand{\InterpRestr}[1]{\Interp^{#1}}\)
\(\newcommand{\InterpI}[1]{I_{#1}}\)
\(%\newcommand{\InterpI}[1]{{\mathcal{I}_{#1}}}\)
\(%\newcommand{\InterpIOf}[2]{#2^{\InterpI{#1}}}\)
\(\newcommand{\InterpDom}{D_{\Interp}}\)
\(\newcommand{\InterpSubst}[2]{\Interp[{#1}\mapsto{#2}]}\)
\(\newcommand{\ThModels}{\mathrel{\models_{\Th}}}\)
\(\newcommand{\ThIModels}[1]{\mathrel{\models_{\ThI{#1}}}}\)
\(\)
\(% Example interpretations\)
\(\newcommand{\IInts}{\InterpI{\textrm{ints}}}\)
\(\newcommand{\IIntsOf}[1]{\InterpIOf{\IInts}{#1}}\)
\(\newcommand{\IMods}{\InterpI{\textrm{mod7}}}\)
\(\newcommand{\IModsOf}[1]{\InterpIOf{\IMods}{#1}}\)
\(\newcommand{\ISilly}{\InterpI{\textrm{silly}}}\)
\(\newcommand{\ISillyOf}[1]{\InterpIOf{\ISilly}{#1}}\)
\(\)
\(\)
\(%\newcommand{\El}[1]{\textup{e}_{#1}}\)
\(\)
\(\newcommand{\ElemI}{\textup{\ding{40}}}\)
\(\newcommand{\ElemII}{\textup{\ding{41}}}\)
\(\newcommand{\ElemIII}{\textup{\ding{46}}}\)
\(\)
\(\newcommand{\ElemA}{\circ}\)
\(\newcommand{\ElemB}{\bullet}\)
\(\)
\(\newcommand{\AxiomMarg}[1]{\makebox{}\hfill(\Blue{#1})}\)
\(\newcommand{\Comment}[1]{\makebox{}\hfill\Blue{#1}}\)
\(\)
\(\newcommand{\DLZ}{\mathit{DL}(\bbZ)}\)
\(\newcommand{\DLQ}{\mathit{DL}(\bbQ)}\)
\(\newcommand{\EUF}{\mathit{EUF}}\)
\(\newcommand{\TEUF}{\ThI{\mathit{EUF}}}\)
\(\newcommand{\LIA}{\mathit{LIA}}\)
\(\newcommand{\TLIA}{\ThI{\mathit{LIA}}}\)
\(\newcommand{\TNRA}{\ThI{\mathit{NRA}}}\)
\(\newcommand{\TNIA}{\ThI{\mathit{NIA}}}\)
\(\newcommand{\LRA}{\mathit{LRA}}\)
\(\newcommand{\TLRA}{\ThI{\mathit{LRA}}}\)
\(\newcommand{\IDL}{\mathit{IDL}}\)
\(\newcommand{\RDL}{\mathit{RDL}}\)
\(\newcommand{\EUFModels}{\mathrel{\models_{\TEUF}}}\)
\(\newcommand{\EUFModelsNot}{\mathrel{{\not\models}_{\TEUF}}}\)
\(\newcommand{\LIAModels}{\mathrel{\models_{\LIA}}}\)
\(\newcommand{\LIANotModels}{\mathrel{\not\models_{\LIA}}}\)
\(\newcommand{\LIAEntails}{\mathrel{\models_{\LIA}}}\)
\(\newcommand{\IDLEntails}{\mathrel{\models_{\IDL}}}\)
\(\newcommand{\NIAModels}{\mathrel{\models_{\TNIA}}}\)
\(\newcommand{\Div}[2]{{{#1}\mid{#2}}}\)
\(\)
\(\newcommand{\Sort}{s}\)
\(\newcommand{\SortI}[1]{s_{#1}}\)
\(\newcommand{\Sorts}{S}\)
\(\newcommand{\Func}{f}\)
\(\newcommand{\Funcs}{F}\)
\(\newcommand{\Pred}{p}\)
\(\newcommand{\Preds}{P}\)
\(\newcommand{\SortName}[1]{\textsf{#1}}\)
\(\)
\(\newcommand{\Var}{x}\)
\(\newcommand{\Vars}{X}\)
\(\newcommand{\BVar}{a}\)
\(\newcommand{\BVars}{\mathcal{B}}\)
\(\newcommand{\Val}{v}\)
\(\)
\(\newcommand{\DomOf}[1]{D_{#1}}\)
\(\)
\(\newcommand{\Term}{t}\)
\(\newcommand{\TermI}[1]{t_{#1}}\)
\(\newcommand{\TermP}[1]{t'}\)
\(\newcommand{\Atom}{A}\)
\(\)
\(\)
\(%\)
\(% EUF\)
\(%\)
\(\newcommand{\UFEq}{\equiv}\)
\(\newcommand{\UFEqP}{\mathrel{\equiv'}}\)
\(\newcommand{\UFEqNot}{\not\equiv}\)
\(\newcommand{\UFNeq}{\not\equiv}\)
\(\)
\(\)
\(\)
\(%\)
\(% Arithmetics\)
\(%\)
\(\newcommand{\IntsSort}{\textrm{Int}}\)
\(\newcommand{\IntsSig}{\SigI{\textrm{Int}}}\)
\(\newcommand{\RealsSort}{\textrm{Real}}\)
\(\newcommand{\Mul}{\mathbin{*}}\)
\(\)
\(%\)
\(% Arrays\)
\(%\)
\(\newcommand{\IndexSort}{\SortName{idx}}\)
\(%\newcommand{\IndexSort}{\SortName{index}}\)
\(\newcommand{\ElemSort}{\SortName{elem}}\)
\(%\newcommand{\ArraySort}{\SortName{array}}\)
\(\newcommand{\ArraySort}{\SortName{arr}}\)
\(\newcommand{\ArrSig}{\Sigma_{\mathit{arrays}}}\)
\(\newcommand{\ArrE}[1]{\textrm{a}_{#1}}\)
\(\)
\(\)
\(\newcommand{\TArrays}{\ThI{\mathit{arrays}}}\)
\(\newcommand{\TArraysExt}{\ThI{\mathit{arrays}}^{=}}\)
\(\newcommand{\ArrModels}{\mathrel{{\models_\mathit{arrays}}}}\)
\(\)
\(\)
\(%\)
\(% Theories of Lisp-like lists\)
\(%\)
\(\newcommand{\ThCons}{\ThI{\textrm{cons}}}\)
\(\newcommand{\ThConsAcyclic}{\ThI{\textrm{cons+}}}\)
\(\newcommand{\SigCons}{\SigI{\textrm{cons}}}\)
\(\newcommand{\Cons}{\FuncName{cons}}\)
\(\newcommand{\Car}{\FuncName{car}}\)
\(\newcommand{\Cdr}{\FuncName{cdr}}\)
\(\newcommand{\LAtom}{\PredName{atom}}\)
\(% Sorted version additions\)
\(\newcommand{\ListSort}{\SortName{list}}\)
\(\newcommand{\Nil}{\FuncName{nil}}\)
\(\newcommand{\Length}{\FuncName{length}}\)
\(\)
\(\)
\(\newcommand{\BVT}{\ThI{\mathsf{BV}}}\)
\(\newcommand{\BVSig}{\SigI{\mathsf{BV}}}\)
\(\newcommand{\BVS}[1]{\SortName{[}#1\SortName{]}}\)
\(%\newcommand{\BVS}[1]{[{#1}]}\)
\(\newcommand{\BVAdd}[1]{\mathbin{{+}_{\BVS{#1}}}}\)
\(\newcommand{\BVLE}[1]{\mathbin{{\le}_{\BVS{#1}}}}\)
\(\newcommand{\BVGE}[1]{\mathbin{{\ge}_{\BVS{#1}}}}\)
\(\newcommand{\BVSL}[1]{\mathbin{{\ll}_{\BVS{#1}}}}\)
\(\newcommand{\BVTermB}[1]{\hat{t}_{(#1)}}\)
\(%\newcommand{\BVTermBI}[2]{\hat{t}_{#1}^{(#2)}}\)
\(\newcommand{\BVAtom}{\hat{A}}\)
\(\newcommand{\BVXB}[1]{\hat{x}_{(#1)}}\)
\(\newcommand{\BVYB}[1]{\hat{y}_{(#1)}}\)
\(\newcommand{\BVVar}[1]{\hat{x}_{(#1)}}\)
\(\)
\(\)
\(% SMTLIB logics\)
\(\newcommand{\SMTLIBLogic}[1]{\textrm{#1}}\)
\(\newcommand{\QFUF}{\SMTLIBLogic{QF\_UF}}\)
\(\newcommand{\QFLIA}{\SMTLIBLogic{QF\_LIA}}\)
\(\newcommand{\QFUFLRA}{\SMTLIBLogic{QF\_UFLRA}}\)
\(\newcommand{\SMTLIBLIA}{\SMTLIBLogic{LIA}}\)
\(\)
\(\newcommand{\CG}[1]{G_{#1}}\)
\(\newcommand{\DiffEdge}[1]{\overset{#1}{\longrightarrow}}\)
\(\)
\(\newcommand{\FuncName}[1]{\textsf{#1}}\)
\(\newcommand{\PredName}[1]{\textsf{#1}}\)
\(\newcommand{\ReadF}{\FuncName{read}}\)
\(\newcommand{\Read}[2]{\ReadF(#1,#2)}\)
\(\newcommand{\WriteF}{\FuncName{write}}\)
\(\newcommand{\Write}[3]{\WriteF(#1,#2,#3)}\)
\(\)
\(\newcommand{\Abs}[1]{\alpha_{#1}}\)
\(\)
\(\newcommand{\Expl}[1]{\textit{explain}(#1)}\)
\(\)
\(\newcommand{\SMTAssertF}{\textsf{assert}}\)
\(\newcommand{\SMTAssert}[1]{\SMTAssertF(#1)}\)
\(\)
\(\newcommand{\UFRoot}{\textit{parent}}\)
\(\newcommand{\UFRootOf}[1]{{#1}.\UFRoot}\)
\(\newcommand{\UFRank}{\textit{rank}}\)
\(\newcommand{\UFRankOf}[1]{{#1}.\UFRank}\)
\(\newcommand{\UFFind}[1]{\textsf{find}(#1)}\)
\(\newcommand{\UFMerge}[2]{\textsf{merge}(#1,#2)}\)
\(\)
\(\newcommand{\CCPending}{\textit{pending}}\)
\(\)
\(\)
\(%\)
\(% Theory solver interface\)
\(%\)
\(\newcommand{\TSinit}[1]{\mathop{init}(#1)}\)
\(\newcommand{\TSassert}[1]{\mathop{assert}(#1)}\)
\(\newcommand{\TSretract}{\mathop{retract}()}\)
\(\newcommand{\TSisSat}{\mathop{isSat}()}\)
\(\newcommand{\TSgetModel}{\mathop{getModel}()}\)
\(\newcommand{\TSgetImplied}{\mathop{getImplied}()}\)
\(\newcommand{\TSexplain}[1]{\mathop{explain}(#1)}\)
\(\)
\(\)
\(\newcommand{\VarsOf}[1]{\mathop{vars}(#1)}\)
\(\)
\(\newcommand{\Dist}[1]{\mathit{dist}(#1)}\)
\(%\newcommand{\Dist}[1]{\mathit{dist}(#1)}\)
\(\)
\(%\)
\(% Nelson-Oppen\)
\(%\)
\(\newcommand{\TComb}{\cup}\)
\(\newcommand{\NOShared}[1]{\mathop{\textrm{shared}}(#1)}\)
\(\newcommand{\NOPart}{P}\)
\(\newcommand{\NOPartI}[1]{P_{#1}}\)
\(%\newcommand{\NOEq}{\mathrel{\approx}}\)
\(%\newcommand{\NOEqNot}{\mathrel{\not\approx}}\)
\(\newcommand{\NOEq}{\mathrel{{\equiv_{P}}}}\)
\(%\newcommand{\NOEq}{\stackrel{\NOPart}{\equiv}}\)
\(\newcommand{\NOEqNot}{\mathrel{\not\equiv_{\NOPart}}}\)
\(%\newcommand{\NOEqNot}{\stackrel{\NOPart}{\not\equiv}}\)
\(\newcommand{\NOArr}{\mathop{arr}(P)}\)
\(\newcommand{\NOArrI}[1]{\mathop{arr}(P_{#1})}\)
\(\)
\(%\)
\(% Example formulas in Nelson-Oppen part\)
\(%\)
\(\newcommand{\NOF}{\phi}\)
\(%\newcommand{\NOFA}{\phi_1}\)
\(%\newcommand{\NOFB}{\phi_2}\)
\(%\newcommand{\NOTA}{\ThI{1}}\)
\(%\newcommand{\NOTB}{\ThI{2}}\)
\(\newcommand{\NOFEUF}{\phi_\mathit{EUF}}\)
\(\newcommand{\NOFLIA}{\phi_\mathit{LIA}}\)
\(\newcommand{\NOFLRA}{\phi_\mathit{LRA}}\)
\(\newcommand{\NOFCons}{\phi_\textup{cons}}\)
\(\)
\(%\newcommand{\Asgn}{\mathrel{:=}}\)
\(\newcommand{\Asgn}{\mathrel{\leftarrow}}\)
\(\)
\(%\newcommand{\Engl}[1]{(engl.\ #1)}\)
\(\)
\(\newcommand{\Ack}[1]{\mathop{ack}(#1)}\)
\(\newcommand{\VVar}[1]{v_{#1}}\)
\(\newcommand{\FVar}[2]{{#1}_{#2}}\)
\(\newcommand{\PVar}[2]{{#1}_{#2}}\)
\(\newcommand{\Flat}{{\phi_\textrm{flat}}}\)
\(\newcommand{\Cong}{{\phi_\textrm{cong}}}\)
\(\)
\(\newcommand{\In}{\mathit{in}}\)
\(\newcommand{\Out}{\mathit{out}}\)
\(\)
\(\newcommand{\SubType}{\FuncName{subtype}}\)
\(\)
\(%\)
\(% Fourier-Motzkin elimination\)
\(%\)
\(\newcommand{\FM}{\phi}\)
\(\newcommand{\FMup}{\phi^\textrm{up}}\)
\(\newcommand{\FMlo}{\phi^\textrm{low}}\)
\(%\newcommand{\FMup}{\phi^{\le}}\)
\(%\newcommand{\FMlo}{\phi^{\ge}}\)
\(\newcommand{\FMindep}{\phi^{\ast}}\)
\(\newcommand{\Nup}{n^\textrm{up}}\)
\(\newcommand{\Nlo}{n^\textrm{low}}\)
\(%\newcommand{\Nup}{n^{\le}}\)
\(%\newcommand{\Nlo}{n^{\ge}}\)
\(\newcommand{\Rup}[1]{A^\textrm{up}_{#1}}\)
\(\newcommand{\Rlo}[1]{A^\textrm{low}_{#1}}\)
\(%\newcommand{\Rup}[1]{A^{\le}_{#1}}\)
\(%\newcommand{\Rlo}[1]{A^{\ge}_{#1}}\)
\(%\newcommand{\FMless}{\mathrel{\triangleleft}}\)
\(%\newcommand{\FMmore}{\mathrel{\triangleright}}\)
\(\)
\(\)
\(\)
\(\newcommand{\ProblemName}[1]{\textup{#1}}\)
\(\newcommand{\ATM}{A_\textup{TM}}\)
\(\newcommand{\PCP}{\ProblemName{PCP}}\)
\(\newcommand{\MPCP}{\ProblemName{MPCP}}\)
\(\newcommand{\PCPAst}{\star}\)
\(\)
\(\newcommand{\Eps}{\varepsilon}\)
\(\)
\(\newcommand{\List}[1]{[#1]}\)
\(\newcommand{\Strings}[1]{\{#1\}^\star}\)
\(\newcommand{\StringsOver}[1]{{#1}^\star}\)
\(\newcommand{\SigmaStrings}{\Sigma^\star}\)
\(\newcommand{\GammaStrings}{\Gamma^\star}\)
\(\newcommand{\Complement}[1]{\overline{#1}}\)
\(\)
\(\)
\(%\)
\(% SSA example\)
\(%\)
\(\newcommand{\In}{\mathit{in}}\)
\(\newcommand{\Out}{\mathit{out}}\)
\(\)
\(%\)
\(%\)
\(%\)
\(\newcommand{\DA}{♠}\)
\(\newcommand{\DB}{♣}\)
\(\newcommand{\DC}{♥}\)
\(\newcommand{\DD}{♦}\)
\(\)
\(%\)
\(% Jobshop example\)
\(%\)
\(\newcommand{\JSJobs}{J}\)
\(\newcommand{\JSJob}[1]{J_{#1}}\)
\(\newcommand{\JSForm}{\phi(\JSJobs)}\)
\(\newcommand{\JSNofTasks}[1]{N_{#1}}\)
\(\newcommand{\JSTask}[2]{T_{#1,#2}}\)
\(\newcommand{\JSMach}[2]{M_{#1,#2}}\)
\(\newcommand{\JSDur}[2]{D_{#1,#2}}\)
\(\newcommand{\JSStart}[2]{s_{#1,#2}}\)
\(\newcommand{\JSBudget}{\mathit{budget}}\)
Theory Solvers for Other Theories
In the following we provide a brief overview and some references for
theory solvers of other theories.
Linear Arithmetic
A linear arithmetic theory solver has to
decide the satisfiability of conjunctions of atoms such as
$$(x + 3y + 2z \le 0.5) \land (-y + 2z + w = 4) \land …$$
Over reals, the satisfiability can be solved in polynomial time but
usually variants of the simplex algorithm are used in practise although their worst-case time complexity is exponential.
Simplex algorithms in the SMT context are designed to allow efficient backtracking, see especially the Dutertre and de Moura CAV 2006 paper in the list below.
Over integers it is NP-complete to determine the satisfiability of
a conjunction of atoms.
The theory solvers thus use search and cutting planes.
Some references:
M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. van Rossum, S. Schulz, R. Sebastiani:
An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic, Proc. TACAS 2005, pp 317–333
B. Dutertre and L. de Moura:
A Fast Linear-Arithmetic Solver for DPLL(T), Proc. CAV 2006, pp 81–94
G. Faure, R. Nieuwenhuis, A. Oliveras, and E. Rodríguez-Carbonell:
SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers, Proc. SAT 2008, pp 77–90
A. Griggio:
A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic, J. Satisf. Boolean Model. Comput. 8(1/2):1–27, 2012
D. Jovanović, L. de Moura:
Cutting to the Chase — Solving Linear Integer Arithmetic, J. Autom. Reasoning 51:79–108, 2013
Nonlinear Arithmetic
Deciding the satisfiability of conjunctions of non-linear arithmetic atoms
over integers is undecidable (see Hilbert’s tenth problem).
Deciding the satisfibility of non-linear arithmetic over reals is decidable but
non-trivial.
To do it, one can use the cylindrical algebraic decomposition method.
Some references:
G. Passmore:
Combined Decision Procedures for Nonlinear Arithmetics, Real and Complex, PhD Thesis, Univ. Edinburgh, 2011
D. Jovanovic and L. de Moura:
Solving Non-linear Arithmetic, Proc. IJCAR 2012, pp 339–354
S. Gao, J. Avigad and E. Clarke: Delta-Decidability over the Reals, Proc. LICS 2012, pp 305–314
B. Akbarpour, L. Paulson:
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions,
J. Automated Reasoning 44(3):175–205, 2010
The QEPCAD solver.
Lazy Approaches for Bit-Vectors
The lazy CDCL(\( \Th \)) approach can also be applied to bit-vector satisfiability,
please see the following references:
Clark W. Barrett, David L. Dill, Jeremy R. Levitt:
A Decision Procedure for Bit-Vector Arithmetic,
Proc. DAC 1998, pp 522–527
Anders Franzén:
Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT,
Doctoral dissertation, Univ. Trento, 2010
L. Hadarean, K. Bansal, D. Jovanovic, C. Barrett, C. Tinelli:
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors,
Proc. CAV 2014, pp 680–695
Arrays
Some references:
R. Brummayer, A. Biere: Lemmas on Demand for the Extensional Theory of Arrays, JSAT 6(1–3): 165–201, 2009
L. de Moura and N. Bjørner:
Generalized, efficient array decision procedures, Proc. FMCAD 2009, pp 45–52
M. Bofill, R. Nieuwenhuis, A. Oliveras, E. Rodríguez-Carbonell, A. Rubio:
A Write-Based Solver for SAT Modulo the Theory of Arrays,
Proc. FMCAD 2008, pp 1–8