Flexibility and Optimization of QBF Skolem-Herbrand Certificates

Skolem and Herbrand functions are important certificates validating the truth and falsity, respectively, of quantified Boolean formulas (QBFs). They are essential in various synthesis and verification applications. Recent advancement established a linear time extraction of Skolem/Herbrand functions...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on computer-aided design of integrated circuits and systems 2016-09, Vol.35 (9), p.1557-1568
Main Authors: Balabanov, Valeriy, Shuo-Ren Lin, Jiang, Jie-Hong R.
Format: Article
Language:English
Subjects:
Arrays
Certificates
Certification
Circuits
Complexity theory
Flexibility
Indexes
Mathematical analysis
Mathematical models
Optimization
quantified Boolean formula (QBF)
Reactive power
satisfiability (SAT)
Semantics
Simplification
Syntactics
Synthesis
verification
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Skolem and Herbrand functions are important certificates validating the truth and falsity, respectively, of quantified Boolean formulas (QBFs). They are essential in various synthesis and verification applications. Recent advancement established a linear time extraction of Skolem/Herbrand functions from QBF consensus/resolution proofs. However, the obtained functions are often excessively large and improper for practical applications. To overcome this limitation, this paper characterizes various flexibilities of QBF certificates, and exploits them for certificate simplification. Experiments show substantial reduction on QBF certificates in terms of circuit size and depth, which are of primary concerns for synthesis applications.
ISSN:0278-0070
1937-4151
DOI:10.1109/TCAD.2015.2512906