ToySolver.SAT.ExistentialQuantification

References:

• [BrauerKingKriener2011] Jörg Brauer, Andy King, and Jael Kriener, "Existential quantification as incremental SAT," in Computer Aided Verification (CAV 2011), G. Gopalakrishnan and S. Qadeer, Eds. pp. 191-207. https://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bkk11a.pdf

Documentation

project

Arguments

:: VarSet

\(X\)

-> CNF

\(\phi\)

-> IO CNF

\(\psi\)

Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\), this function computes a CNF formula \(\psi\) that is equivalent to \(\exists X. \phi\) (i.e. \((\exists X. \phi) \leftrightarrow \psi\)).

shortestImplicants

Arguments

:: VarSet

\(X\)

-> CNF

\(\phi\)

-> IO [LitSet]

Deprecated: Use shortestImplicantsE instead

Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\), this function computes shortest implicants of \(\phi\) in terms of \(X\). Variables except \(X\) are treated as if they are existentially quantified.

Resulting shortest implicants form a DNF (disjunctive normal form) formula that is equivalent to the original (existentially quantified) formula.

shortestImplicantsE

Arguments

:: VarSet

\(X\)

-> CNF

\(\phi\)

-> IO [LitSet]

Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\), this function computes shortest implicants of \(\exists X. \phi\).

Resulting shortest implicants form a DNF (disjunctive normal form) formula that is equivalent to the original formula \(\exists X. \phi\).

negateCNF

Arguments

:: CNF

\(\phi\)

-> IO CNF

\(\psi \equiv \neg\phi\)

Given a CNF formula \(\phi\), this function returns another CNF formula \(\psi\) that is equivalent to \(\neg\phi\).