Commit 6c77a4bf by Martin Jonáš

 ... ... @@ -4,7 +4,7 @@ \section{Preliminaries} This section introduces the notation which is used in the rest of this This section introduces the notation used in the rest of this chapter. The exposition of the propositional logic is mainly based on the work of Nieuwenhuis et al.~\cite{NOT06}. The exposition of the first-order logic is partly based on the same source, but the ... ... @@ -72,16 +72,16 @@ contain free variables. For example, if we consider a set of atoms $\P = \{ x \geq y + 1, x = 4 \}$, where $x, y, 1$, and $4$ are constant symbols, $x \geq y + 1~\vee~\neg (x = 4)$ is a clause. A \emph{theory} $T$ is a set of first-order structures. A formula $\varphi$ is $T$-\emph{satisfiable} or $T$-\emph{consistent} if there is a structure $M \in T$ in which the formula $F$ holds in the standard first-order sense. The formula $\varphi$ is $T$-\emph{unsatisfiable} or $T$-\emph{inconsistent} otherwise. If the distinction is necessary, we call literals over a specific background theory $T$-literals. In the rest of this chapter, we consider only theories for which the satisfiability of conjunctions of literals is decidable and we call any decision procedure for conjunctions of $T$-literals over a $T$-\emph{solver}. A \emph{theory} $T$ is a set of first-order structures. A formula $\varphi$ is $T$-\emph{satisfiable} or $T$-\emph{consistent} if there is a structure $M \in T$ in which the formula $F$ holds in the standard first-order sense. The formula $\varphi$ is $T$-\emph{unsatisfiable} or $T$-\emph{inconsistent} otherwise. If the distinction is necessary, we call literals over a specific background theory $T$-literals. In the rest of this chapter, we consider only theories for which the satisfiability of conjunctions of literals is decidable and we call any decision procedure for conjunctions of $T$-literals a $T$-\emph{solver}. Using the same notation as in the propositional logic, a partial assignment is a set of literals and can be therefore seen as a ... ... @@ -107,11 +107,11 @@ functions; this process is known as \emph{Skolemization}. \section{Propositional satisfiability} A \emph{propositional satisfiability problem} (\sat) is for a given formula $\varphi$ in \cnf decide whether it is satisfiable. The A \emph{propositional satisfiability problem} (\sat) is, for a given formula $\varphi$ in \cnf, to 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 the Tseitin transformation can be used to transform every formula to an equisatisfiable formula in \cnf with only linear increase of its size~\cite{Tse68}. \subsection{Davis--Putnam--Logemann--Loveland algorithm} ... ... @@ -145,7 +145,7 @@ 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 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 backtracking used in \dpll is \emph{chronological}, i.e. after a conflict the value of the last decided literal is changed. %It has been observed that \dpll based solver spends the ... ... @@ -177,7 +177,7 @@ 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 search space can be ruled out from the search, as it is known not to contain a solution. There are multiple strategies of computing the contain any solution. There are multiple strategies of computing the clausal reason for the conflict, but the majority of \cdcl based \sat solvers are using the \emph{first unique implication point} based learning scheme, which has been shown to produce small clauses in ... ... @@ -195,13 +195,14 @@ 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 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} 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 \emph{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 the ... ...