Skip to main content

Existential Quantification as Incremental SAT: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings

Brauer, Jorg and King, Andy and Kriener, Jael (2011) Existential Quantification as Incremental SAT: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. In: Gopalakrishnan, Ganesh and Qadeer, Shaz, eds. Computer Aided Verification. Lecture Notes in Computer Science, 6806 . Springer, Berlin, Germany, pp. 191-207. ISBN 978-3-642-22109-5. E-ISBN 978-3-642-22110-1. (doi:10.1007/978-3-642-22110-1_17) (KAR id:37589)

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.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-642-22110-1_17
Subjects: A General Works
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 12 Dec 2013 21:13 UTC
Last Modified: 27 Nov 2023 14:42 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/37589 (The current URI for this page, for reference purposes)

University of Kent Author Information

King, Andy.

Creator's ORCID: https://orcid.org/0000-0001-5806-4822
CReDIT Contributor Roles:

Kriener, Jael.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.