Commit bcd1e724 authored by Martin Jonas's avatar Martin Jonas
Browse files

More polishing

parent a6c04467
......@@ -312,13 +312,13 @@ combinations of the represented Boolean functions using the recursive
procedure \texttt{Apply}~\cite{Bry86}. The main idea of symbolic \sat
solvers is to convert a \cnf formula to the corresponding \robdd and
check the root of the resulting \bdd. If the resulting \bdd is
equivalent to the \bdd for the constant $0$ function, the formula is
unsatisfiable, and it is satisfiable otherwise. However, in order to
keep the size of the \bdd small, it is necessary to existentially
quantify the variables during the computation. This technique is known
as \emph{early quantification}~\cite{HKB96}. A simplified symbolic
\sat algorithm can be found for example in the survey of \sat solving
by Darwiche and Pipatsriswat~\cite{DP09}.
equivalent to the \bdd for the function that is $0$ everywhere, the
formula is unsatisfiable, and it is satisfiable otherwise. However, in
order to keep the size of the \bdd small, it is necessary to
existentially quantify the variables during the computation. This
technique is known as \emph{early quantification}~\cite{HKB96}. A
simplified symbolic \sat algorithm can be found for example in the
survey of \sat solving by Darwiche and Pipatsriswat~\cite{DP09}.
Look-ahead based algorithm, in contrast to the \cdcl, are employing
expensive heuristics to guide the \dpll search to a satisfying
......
......@@ -32,8 +32,8 @@ that at least one of the last 4 bits of the variable $a$ has to be
$1$, i.e. the value of $a$ is not divisible by $16$. After conjoining
this \bdd to the \bdd for $a=16 \cdot b \,+\, 16 \cdot c$, the formula
is decided unsatisfiable, as the resulting \bdd represents the
constant $0$ function. On the other hand, if one considers only
quantifier instantiations by the subterm of the input formula,
function that is $0$ everywhere. On the other hand, if one considers
only quantifier instantiations by the subterm of the input formula,
exponentially many quantifier instances have to be added to the
formula to show its unsatisfiability, as there is no subterm of
$\varphi$ that can be instantiated as $x$ to yield an unsatisfiable
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment