School of Computing

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},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014