School of Computing

Approximate Quantifier Elimination for Propositional Boolean Formulae

Jorg Brauer and Andy King

In Mihaela Bobaru, Klaus Havelund, Gerard Holzmann, and Rajeev Joshi, editors, Third NASA Formal Methods Symposium, volume 6617 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, April 2011.

Abstract

This paper describes an approximate quantifier elimination procedure for propositional Boolean formulae. The method is based on computing prime implicants using SAT and successively refining over-approximations of a given formula. This construction naturally leads to an anytime algorithm, that is, it can be interrupted at anytime without compromising soundness. This contrasts with classical monolithic (all or nothing) approaches based on resolution or model enumeration.

Download publication 212 kbytes (PDF)

Bibtex Record

@inproceedings{3084,
author = {Jorg Brauer and Andy King},
title = {Approximate {Q}uantifier {E}limination for {P}ropositional {B}oolean {F}ormulae},
month = {April},
year = {2011},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2011/3084},
    publication_type = {inproceedings},
    submission_id = {4158_1297856898},
    booktitle = {Third NASA Formal Methods Symposium},
    editor = {Mihaela Bobaru and Klaus Havelund and Gerard Holzmann and Rajeev Joshi },
    volume = {6617},
    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