Copyright	(c) Masahiro Sakai 2017
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	BangPatterns

ToySolver.SAT.ExistentialQuantification

Description

[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.cs.kent.ac.uk/pubs/2011/3094/content.pdf

Synopsis

project :: VarSet -> CNF -> IO CNF
shortestImplicantsE :: VarSet -> CNF -> IO [LitSet]
negateCNF :: CNF -> IO CNF

Documentation

project Source #

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\)).

shortestImplicantsE Source #

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 Source #

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\).