You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
9 lines
1002 B
9 lines
1002 B
\item \self Consider the \textit{Theory of Equality} $\mathcal{T}_{E}$. We want to decide whether or not a formula $\phi$ in $\mathcal{T}_{E}$ is satisfiable with respect to the theory. To do so, we will first use a SAT solver on the propositional skeleton of $\phi$. If the SAT solver returns a satisfying model, we use a theory solver for the conjunctive fragment of the theory to check whether the truth assignment to literals is consistent with the theory. If not, we add a blocking clause to the propositional skeleton and use the SAT solver again. This is repeated until either the SAT solver reports \textit{unsatisfiable}, or the theory solver reports an assignment to be consistent with the theory. The name of this method for checking satisfiability of theory formulas is ... ?
|
|
|
|
\begin{itemize}
|
|
\item[$\square$] DPLL(T)
|
|
\item[$\square$] Lazy Encoding
|
|
\item[$\square$] Eager Encoding
|
|
\item[$\square$] Tseitin's Encoding
|
|
\item[$\square$] Ackermann's Reduction
|
|
\end{itemize}
|