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.
69 lines
3.6 KiB
69 lines
3.6 KiB
\newcommand{\dpllDescription}[1]{Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{#1} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
|
|
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.}
|
|
|
|
\newcommand{\dpllDescriptionAssignmentSheet}{Use the DPLL algorithm with the rules as described above to check whether the following formula in CNF is satisfiable}
|
|
|
|
\newcommand{\ndDescription}{ For each of the following sequents, either provide a natural deduction proof, or a counter-example that proves the sequent invalid. \\
|
|
|
|
\noindent For proofs, clearly indicate which rule, and what assumptions/premises/\\intermediate results you are using in each step. Also clearly indicate the scope of any boxes you use. \\
|
|
|
|
\noindent For counterexamples, give a complete model. Show that the model satisfies
|
|
the premise(s) of the sequent in question, but does not satisfy the respective conclusion.}
|
|
|
|
\newcommand{\tseitinRules}{%
|
|
We list the \emph{Tseitin-rewriting rules} to be applied for the following examples.
|
|
\begin{align*}
|
|
\chi \leftrightarrow (\phi \lor \psi) \quad &\Leftrightarrow \tseitinOr{\chi}{\phi}{\psi} \\
|
|
\chi \leftrightarrow (\phi \land \psi) \quad &\Leftrightarrow \tseitinAnd{\chi}{\phi}{\psi} \\
|
|
\chi \leftrightarrow \lnot \phi \quad &\Leftrightarrow \tseitinNot{\chi}{\phi}
|
|
\end{align*}
|
|
}
|
|
|
|
\newcommand{\constructROBDD}[2]{%
|
|
Construct the reduced and ordered BDD for the formula%
|
|
$$#1$$%
|
|
using #2.
|
|
Compute the needed cofactors.
|
|
You may add function nodes representing all cofactors to the final BDD.
|
|
Use complemented edges and one terminal node representing the truth value $\T$. To simplify drawing, you may assume that dangling edges point to the constant node.}
|
|
|
|
\newcommand{\BDDToROBDD}{%
|
|
Transform the given Binary Decision Diagram into a reduced and ordered BDD.}
|
|
|
|
\newcommand{\BDDToDNF}{%
|
|
Given the following Binary Decision Diagram that represents the formula $f$. Compute its disjunctive normal form \DNF{f}.}
|
|
|
|
|
|
\newcommand{\computeCNFDNF}[1][\varphi]{%
|
|
Compute \DNF{#1} and \CNF{#1} using a truth table.
|
|
}
|
|
\newcommand{\CNFfromCircuit}{%
|
|
Compute the propositional formula $\varphi$ represented by the following circuit. Furthermore, compute an equisatisfiable formula $\varphi'$ using the Tseitin transformation.
|
|
}
|
|
\newcommand{\applyTseitin}[1]{%
|
|
Apply the Tseitin transformation to #1. For each variable you introduce, clearly indicate which subformula it represents.
|
|
}
|
|
\newcommand{\applyCC}[1]{%
|
|
Consider the following formula in the conjunctive fragment of $\mathcal{T}_{EUF}$.
|
|
#1
|
|
Use the congruence closure algorithm to determine whether this formula is satisfiable.
|
|
}
|
|
|
|
\newcommand{\applyAckermann}[1]{%
|
|
Given the formula
|
|
#1
|
|
Apply the Ackermann reduction to compute an equisatisfiable formula in $\mathcal{T}_{E}$.
|
|
}
|
|
\newcommand{\applyGB}[1]{%
|
|
Perform the graph-based reduction to translate the following formula in $\mathcal{T}_{E}$ into an
|
|
equisatisfiable formula in propositional logic.
|
|
#1
|
|
}
|
|
\newcommand{\applyEagerEUF}[1]{%
|
|
Consider the following formula in $\mathcal{T}_{EUF}$.
|
|
#1
|
|
\begin{itemize}
|
|
\item Use Ackermann's reduction to compute an equisatisfiable formula in $\mathcal{T}_{E}$.
|
|
\item Then perform the graph-based reduction on the outcome of Ackermann's reduction to construct an equisatisfiable propositional formula $\phi_{prop}$.
|
|
\end{itemize}
|
|
}
|