© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Existential Quantification as Incremental SAT
Jorg Brauer, Andy King, and Jael Kriener
In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Twenty Third International Conference on Computer Aided Verification, Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, July 2011.Abstract
This paper presents an elegant algorithm for existential quantifier elimination using incremental SAT solving. This approach contrasts with existing techniques in that it is based solely on manipulating the SAT instance rather than requiring any reengineering of the SAT solver or needing an auxiliary data-structure such as a BDD. The algorithm combines model enumeration with the generation of shortest prime implicants so as to converge onto a quantifier-free formula presented in CNF. We apply the technique to a number of hardware circuits and transfer functions to demonstrate the effectiveness of the method.
Download publication 317 kbytes (PDF)Bibtex Record
@inproceedings{3094, author = {Jorg Brauer and Andy King and Jael Kriener}, title = {Existential {Q}uantification as {I}ncremental {SAT}}, month = {July}, year = {2011}, pages = {182-196}, keywords = {determinacy analysis, Craig interpolants}, note = {}, doi = {}, url = {http://www.cs.kent.ac.uk/pubs/2011/3094}, publication_type = {inproceedings}, submission_id = {19108_1300882683}, booktitle = {Twenty Third International Conference on Computer Aided Verification}, editor = {Ganesh Gopalakrishnan and Shaz Qadeer}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, refereed = {yes}, }