More grammar fixes

called \emph{complementary}. A \emph{clause} is a finite disjunction

of literals. The empty clause is denoted by $\bot$. A formula in

the \emph{conjunctive normal form} (\cnf) is a finite conjunction of

clauses. If convinient, we will use idempotence and commutativity of

clauses. If convenient, we will use idempotence and commutativity of

disjunction and view clauses as sets of literals and therefore ignore

the order and multiple occurences of literals. Similarly, if

convinient, we will view \cnf formulas as sets of clauses. For

the order and multiple occurrences of literals. Similarly, if

convenient, we will view \cnf formulas as sets of clauses. For

example, we will write the formula

$(x \vee \overline{y}) \wedge (\overline{x} \vee z)$ as the set

$\{ \{ x , \overline{y} \}, \{ \overline{x} \vee z \} \}$.

$\{ \{ x , \overline{y} \}, \{ \overline{x}, z \} \}$.

A \emph{partial assignment} $M$ is a set of literals that does not

contain complementary literals, i.e.

is \emph{true} in the assignment $M$ if $l \in M$, \emph{false} in $M$

if $\neg l \in M$, and \emph{undefined} otherwise. A literal is

\emph{defined} in $M$ if it is true or false in $M$. We call an

asignment $M$ \emph{total} over $\P$ if all literals of $\P$ are

assignment $M$ \emph{total} over $\P$ if all literals of $\P$ are

defined in $M$. A clause is \emph{true} in $M$ if at least one of its

literals is true in $M$ and a \cnf formula is \emph{true} in $M$ if

all of its clauses are true in $M$. A clause that is false for a given

Using the same notation as in the propositional logic, a partial

assignment is a set of literals and can be therefore seen as a

conjunction of literals, i.e. a formula. If a partial assignment $M$

is a propositional model of a for a given formula $F$ and the partial

is a propositional model of a given formula $F$ and the partial

assignment $M$ is $T$-consistent, we say that $M$ is a

$T$-\emph{model} of $F$. If $F$ and $G$ are formulas such that

$F \wedge \neg G$ is $T$-inconsistent, we say that \emph{$F$ entails

\section{Propositional satisfiability}

A \emph{propositional statisfiability problem} (\sat) is for a given

formula $F$ in \cnf decide wheter it is satisfiable. The restriction

A \emph{propositional satisfiability problem} (\sat) is for a given

formula $F$ in \cnf decide whether it is satisfiable. The restriction

to formulas in \cnf is without a loss of generality, as Tseitin

transformation can be used to transform every formula to a

equisatisfiable formula in \cnf with only linear increase of its

guiding the \dpll search is the \emph{unit clause rule}, which is

based on the observation that if a formula contains a clause $C$ that

is unit in the current assignment, the only way to build a satisfying

asignment is to add the sole undefined literal of $C$ to $M$. The

assignment is to add the sole undefined literal of $C$ to $M$. The

iterated application of the unit clause rule is called \emph{unit

  propagation} or \emph{boolean constraint propagation}

  propagation} or \emph{Boolean constraint propagation}

(\bcp)~\cite{ZM88}. The \dpll search consists of decision and

propagation steps. In decision steps, a variable and its new value are

chosen and added to the current partial assignment. After the decision

chosen and added to the current partial assignment. After each decision

step, the \bcp is performed to set values of variables which are

implied by the decision. The backtracking used in \dpll is

\emph{chronological}, i.e. after the conflict the value of the last

Although the \dpll algorithm is more efficient than the original \dppr

algorithm, it may unnecessarily explore parts of the search space that

contain no solution. This problem can be partly solved by a further

contain no solution. This problem can be partially solved by a further

refinement of the \dpll algorithm called Conflict-Driven Clause

Learning (\cdcl), which was proposed by Marques-Silva and

Sakallah~\cite{MSS99} and is a base of almost all modern \sat

  graph} during the search, which records reasons for assigning the

unit-propagated literals during the search. If a conflict clause is

found, a clause which captures the reason of the conflict is computed

by analyzing of the implication graph or equivalently by the backwards

by analyzing the implication graph or equivalently by the backwards

resolution process~\cite{BKS04}. After computing the clause $C$ that

is a reason of the conflict, \cdcl based solvers \emph{learn} the

clause $C$, in order not to repeat the similar conflict in the future,

and change the value of the last decision literal that occurs in the

explains the conflict, \cdcl based solvers \emph{learn} the clause

$C$, in order not to repeat the similar conflict in the future, and

change the value of the last decision literal that occurs in the

clause $C$. Note that this literal does not have to be the last

decision literal in the search, and therefore a bigger region of the

decision literal in the search and therefore a bigger region of the

search space can be ruled out from the search, as it is known not to

contain a solution. There are multiple strategies to computing the

contain a solution. There are multiple strategies of computing the

clausal reason for the conflict, but the majority of \cdcl based \sat

solvers are using the first \emph{unique implication point} based

solvers are using the \emph{first unique implication point} based

learning scheme, which has been shown to produce small clauses in

practice~\cite{MMZZM01}.

\sat solver are using VSIDS heuristic~\cite{MMZZM01}, which prefers

the variables which have appeared in the biggest number of recent

conflicts. More recently, new branching heuristics based on learning

rate have been proposed and shown to outperform currently used VSIDS

branching heuristics~\cite{LGPC16}.

rate have been proposed and shown to outperform the currently used

VSIDS branching heuristic~\cite{LGPC16}.

Another important part of modern \sat solvers are dynamic restarts,

which allow restarting the search from scratch in hope that clauses

learned during the conflict analyses will guide the search from

regions of the search space which contain no

solutions~\cite{GSK98}. Although most commonly used heuristic to

decide when to restart the solver is based on the Luby

sequence~\cite{LSZ93}, the recent survey has shown that it is

outperformed by a heuristic based on the concept of exponential moving

averages~\cite{BF15restarts}.\marginpar{spravit citaci, BF15a nevyšlo

  v proceedings}

learned during the conflict analyses will guide the search from regions

of the search space that contain no solutions~\cite{GSK98}. Although

most commonly used heuristic to decide when to restart the solver is

based on the Luby sequence~\cite{LSZ93}, the recent survey has shown

that it is outperformed by a heuristic based on the concept of

exponential moving averages~\cite{BF15restarts}.\marginpar{spravit

  citaci, BF15a nevyšlo v proceedings}

In addition to the mentioned heuristics, an efficient implementation

of \cdcl based \sat solver relies on lazy data structures used in

boolean constraint propagation. This is important because it has been

Boolean constraint propagation. This is important because it has been

observed that \sat solvers spend most of the computation time doing

\bcp. Therefore, most of the modern \sat solvers use \emph{two-watched

  literal scheme}~\cite{MMZZM01} to efficiently identify clauses which

Symbolic algorithms rely on a compact representation of the set of

satisfying assignments using \emph{Binary Decision Diagrams} (\bdds)

-- a data structure proposed by Bryant to represent Boolean

functions~\cite{Bry86}. In particular, symbolic \sat algorithms are

functions~\cite{Bry86}. In particular, symbolic \sat algorithms are

using Reduced Ordered \bdds, which represent the boolean functions

\emph{canonically} and allow efficient computation of boolean

using Reduced Ordered \bdds, which represent the Boolean functions

\emph{canonically} and allow efficient computation of Boolean

combinations of the represented Boolean functions using the procedure

\texttt{Apply}~\cite{Bry86}. The main idea is to convert a \cnf

formula to the corresponding \robdd and existentially quantify all

variables from it using disjunction and negation. If the resulting

expensive heuristics to guide the \dpll search to a satisfying

assignment instead of using inexpensive heuristics and learning from

the conflicts~\cite{HD04}. Therefore, while \cdcl solvers are

efficient on large industrial formulas, lookahead-based \sat solvers

efficient on large industrial formulas, look-ahead-based \sat solvers

are efficient on small hard problems, which require sophisticated

heuristics~\cite{HKWB11}. The strengths of these two approaches were

combined to a technique called \emph{cube-and-conquer}, in which a

lookahead-based solver is used to partition the formula to a many

look-ahead-based solver is used to partition the formula to many

simpler formulas, which are in turn solved by an efficient \cdcl

solver~\cite{HKWB11}. The cube-and-conquer approach has been shown to

be efficient in practice due to an easy parallelization and has been

recently used to solve a long-standing problem in the Ramsey

recently used to solve a long-standing open problem in the Ramsey

theory~\cite{HKM16}.

\section{Satisfiability modulo theories}

Similarly to \sat, the \emph{statisfiability modulo theories problem}

Similarly to \sat, the \emph{satisfiability modulo theories problem}

(\smt) is for a given a \cnf formula $F$ in a fixed theory $T$ decide

whether it is $T$-satisfiable. Depending on the the theory $T$, the

complexity of the \smt problem ranges from $\NP$-complete to

undecideable. Notable examples of decidable first-order theories

undecidable. Notable examples of decidable first-order theories

include

\begin{itemize}

\item theory of equality and uninterpreted functions,

\item theory of linear integer arithmetic,

\item theory of linear real arithmetic,

\item theory of real arithmetic,

\item theory of arrays,

\item theory of fixed-size bit-vectors.

\item the theory of equality and uninterpreted functions,

\item the theory of linear integer arithmetic,

\item the theory of linear real arithmetic,

\item the theory of real arithmetic,

\item the theory of arrays,

\item the theory of fixed-size bit-vectors.

\end{itemize}

For a detailed description of these theories and implementation of the

respective $T$-solvers, we refer the reader for example to the book of

of the theory of uninterpreted functions and the theory of Presburger

arithmetic with ordering~\cite{LS04}.

\paragraph{Offline approach} On the other hand, the lazy \smt approach

uses a \sat solver to reason about the boolean structure of the

formula and a specialized $T$-solver to reason about conjunctions of

$T$-literals. In particular, the input formula $\varphi$ is first

converted to a propositional formula $\varphi^p$ called \emph{boolean

On the other hand, the lazy \smt approach uses a \sat solver to reason

about the Boolean structure of the formula and a specialized

$T$-solver to reason about conjunctions of $T$-literals. There are two

variants of the lazy approach to the \smt solving -- \emph{online} and

\emph{offline}~\cite{FJOS03}.

\paragraph{Offline approach}

In the offline approach, the input formula $\varphi$ is first

converted to a propositional formula $\varphi^p$ called \emph{Boolean

  abstraction} by treating each atom as a propositional variable and

then the \sat solver is asked to decide satisfiability of

$\varphi^p$. If $\varphi^p$ is unsatisfiable, the input formula

$T$-satisfiable, the formula $\varphi$ is also $T$-satisfiable. If the

propositional model is not $T$-satisfiable, the corresponding theory

lemma $\neg M^p$ is added to the formula and the procedure is

repeated. This variant of the lazy \smt approach is sometimes called

\emph{offline}~\cite{FJOS03}, because it uses the \sat solver as a

black box and employs the \smt solver only to check satisfiability of

a complete boolean assignment.

\paragraph{Online approach} In contrast to the offline approach, the

\sat and \smt solvers can cooperate more tightly, resulting in a

\emph{online} variant of the lazy \smt approach, which outperforms the

offline approach in most of the cases~\cite{FJOS03}. In the online

variant, \smt solver is used not only to check validity of the total

boolean assignment, but it is used to check the validity of the

partial assignment during the \dpll search (known as \emph{early

  pruning}~\cite{ABCKS02}), to assign values of literals which are

$T$-entailed by the current assignment (known as \emph{theory

  propagation}~\cite{ACG99}), and to provide smaller theory lemmas

that explain the conflict. In order for this combination to be

efficient, the $T$-solver should provide several important

features. Namely, it should be \emph{incremental}, so it does not

restart the computation after every decided literal, it should be able

to provide small theory lemmas explaining conflicts and theory

propagation, so the \sat solver can backtrack to a relevant decision

literal, and it should be able to efficiently unassign the values of

literals during backtracking. In most of the cases, the $T$-solver is

also required to be able to provide models for the satisfiable

formulas.

repeated. This variant of the lazy \smt approach is called offline,

because it uses the \sat solver as a black box and employs the \smt

solver only to check satisfiability of a complete Boolean assignment.

\paragraph{Online approach}

In contrast to the offline approach, the \sat and \smt solvers can

cooperate more tightly, resulting in a online variant of the lazy \smt

approach, which outperforms the offline approach in most of the

cases~\cite{FJOS03}. In the online variant, the \smt solver is used

not only to check validity of the total Boolean assignment, but it is

also used to check the validity of the partial assignment during the

\dpll search (known as \emph{early pruning}~\cite{ABCKS02}), to assign

values of literals which are $T$-entailed by the current assignment

(known as \emph{theory propagation}~\cite{ACG99}), and to provide

smaller theory lemmas that explain the conflict. In order for this

combination to be efficient, the $T$-solver should provide several

important features. Namely, it should be \emph{incremental}, so it

does not restart the computation after every decided literal, it

should be able to provide small theory lemmas explaining conflicts and

theory propagation, so the \sat solver can backtrack to a relevant

decision literal, and it should be able to efficiently unassign the

values of literals during backtracking. In most of the cases, the

$T$-solver is also required to be able to provide models for the

satisfiable formulas.

This approach of \smt approach, in which the $T$-solver is used to

guide the search of the underlying \dpll solver has ben named

\dpllt~\cite{NOT06}. For detailed description of \dpllt and further

improvements, we refer the reader to survey on the topic~\cite{Seb07},

or to the abstract description of the underlying transition

system~\cite{NOT06}. The \dpllt approach is used in the majority

of modern \smt solvers, including Barcelogic~\cite{Barcelogic},

CVC4~\cite{CVC4}, MathSAT~\cite{MathSAT}, OpenSMT~\cite{OpenSMT},

guide the search of the underlying \dpll solver has been named

\dpllt~\cite{NOT06}. For the detailed description of \dpllt and

further improvements, we refer the reader to survey on the

topic~\cite{Seb07}, or to the abstract description of the underlying

transition system~\cite{NOT06}. The \dpllt approach is used in the

majority of modern \smt solvers, including

Barcelogic~\cite{Barcelogic}, CVC4~\cite{CVC4},

MathSAT~\cite{MathSAT}, OpenSMT~\cite{OpenSMT},

Simplify~\cite{Simplify}, Yices~\cite{Yices}, or Z3~\cite{Z3}.

\subsection{Natural domain \smt}

Although the separation of the boolean and theory reasoning in the

Although the separation of the Boolean and theory reasoning in the

\dpll approach allows the solver to be modular, it can be also

restricting in some cases. In particular, the \dpllt based solver can

not directly reason about values of first-order variables, but has to

rely on the $T$-solver guiding the search over boolean

restricting in some cases. In particular, the \dpllt based solvers can

not directly reason about values of first-order variables, but have to

rely on the $T$-solver guiding the search over Boolean

valuations. While there are some techniques like \emph{splitting on

  demand}~\cite{BNOT06} , which allow the $T$-solver to add new atoms

to the formula and delegate the case splitting to the \sat solver,

their performance depends on the internal heuristics of the \sat

solver. To overcome this issue, Cotton has proposed \emph{Natural

to the formula and delegate the case splitting to the underlying \sat

solver, their performance depends on the internal heuristics of the

\sat solver. To overcome this issue, Cotton has proposed \emph{Natural

  domain \smt} approach, which allows the \smt solver to reason

directly about the natural domains of variables like integers or reals

instead of merely choosing boolean valuations~\cite{Cot10}. This has

instead of merely choosing Boolean valuations~\cite{Cot10}. This has

led to two main techniques of \smt solving -- \emph{abstract

  conflict-driven clause learning} and \emph{model-constructing

  satisfiability calculus}~\cite{Mon16}.

point computation of this abstract model transformer, decisions are

downward extrapolations, and conflict analysis corresponds to

computing an under-approximation of the conflict transformer. Further,

clause learning can be seen as learning of a new transformer, computed

by the conflict analysis.

clause learning can be seen as learning of a new transformer, which is

computed by the conflict analysis.

In thus specified framework, an abstract domain can be replaced by an

arbitrary domain that satisfies a certain set of requirements and thus

\paragraph{Model-constructing satisfiability calculus} The other

approach to the natural \smt solving is the model-constructing

satisfiability calculus (\mcsat), proposed by de Moura and

Jovanović~\cite{MJ13, JMB13}. \mcsat is based on \dpll style search,

but in addition to assigning values of boolean variables, it can

assign the value of theory variables and it can generate new literals

not occuring in the original formula. De Moura et al. have implemented

the \mcsat solver supporting linear real arithmetic and uninterpreted

function, which uses model-driven Fourier-Motzkin

ellimination~\cite{Dan63} to learn new predicates from arithmetic

Jovanović~\cite{MJ13, JMB13}. \mcsat is based on the \dpll style

search, but in addition to assigning values of Boolean variables, it

can assign the value of theory variables and it can generate new

literals not occurring in the original formula. De Moura et al. have

implemented the \mcsat solver supporting linear real arithmetic and

uninterpreted function, which uses model-driven Fourier-Motzkin

elimination~\cite{Dan63} to learn new predicates from arithmetic

conflicts and model-driven Ackermannization~\cite{MB08, Ack54} to

learn new predicates from conflicts involving uninterpreted

functions. This solver has shown to have performance comparable with

In the context of \sat and \smt solving, an unsatisfiable core is a

subset of clauses of a unsatisfiable formula that is already

unsatisfiable~\cite{CGS07}. We will mention three main approaches for

unsatisfiable core computation in \smt-solving~\cite{BSST09}. First,

if a solver can compute resolution proofs for unsatisfiable formulas,

the clauses that occur in the proof can be returned as a unsatisfiable

core. In the second approach each clause can be represented by a fresh

selector variable and after a top level conflict, clauses whose

selector variable appears in the final conflict clause are returned as

an unsatisfiable core. Third approach consists in combination of an

\smt solver with an external propositional core~\cite{CGS07}.

the unsatisfiable core computation in \smt~\cite{BSST09}. In the

first, if a solver can compute resolution proofs for unsatisfiable

formulas, the clauses that occur in the proof can be returned as a

unsatisfiable core. In the second approach each clause can be

represented by a fresh selector variable and after a top level

conflict, clauses whose selector variable appears in the final

conflict clause are returned as an unsatisfiable core. Third approach

consists in combination of an \smt solver with an external

propositional core~\cite{CGS07}.

A (Craig) interpolant for a pair of formulas $F$ and $G$ such that

$F \wedge G$ is unsatisfiable is a formula $I$ such that