Certification in Quantified Decision Procedures
Date Issued
2015
Date
2015
Author(s)
Balabanov, Valeriy
Abstract
Satisfiability (SAT) plays one of the key roles in the modern automated reasoning. For the past decade a huge success in SAT solving was achieved by researchers, and nowadays SAT-based decision algorithms scale well for many real-world applications. Quantified Boolean Formulas (QBFs) extend formulas of propositional logic by allowing existential and universal quantifications over variables. Quantifiers make QBF more expressive and allow a more compact constraints representation compared to SAT. In addition to problems encountered in formal verification, QBF has applications in planning, two-player games, electronic design automation, and other fields of computer science. Many methods have been proposed for efficient SAT solving, including search-based solving with different learning techniques (e.g., conflict driven clause learning), syntactic rewriting methods (e.g., resolution rules), various preprocessing techniques (e.g., variable elimination), and so on. Many of these techniques were then adapted for QBF evaluation (e.g., extensions of search-based algorithms, introduction of Q-resolution, etc). Despite its similarities to SAT solving, evaluating QBFs has its unique features related to the quantification nature. Certification of QBFs is of a great interest: Not only it confirms the answer provided by the solver (e.g., by providing syntactic Q-resolution proof), but more importantly directly provides information required in many synthesis applications (e.g., by returning a semantic model). Semantic QBF certificates can serve as a winning strategy in two-player games, the functional representation of a relation in a determinization problem, and other applications. Despite the importance of QBF evaluation and certification, solving algorithms remain immature, and many related issues are not well studied yet. In this work we provide an overview of different QBF solving and certifying techniques, and propose novel approaches that experimentally show improvements over existing ones. Our main contributions include developing new QBF proof systems and building corresponding syntactic certificates based on Q-resolution, providing efficient algorithms for semantic certificates extraction from various syntactic proofs, introducing new optimization heuristics for semantic certificates minimization, and a semantic classification method for dependency QBFs (DQBFs). Along with theoretical achievements, conducted experiments show that proposed methods can be useful in modern applications, therefore forming solid practical values.
Subjects
Quantified Boolean Formula
QBF evaluation
certificate
q-resolution
Skolem function
Herbrand function
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-104-D00943039-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):e01b0b41606229075164616df09d8a15