Reconstructing and Utilizing Circuit Information in Quantified Boolean Formula Solving
Date Issued
2016
Date
2016
Author(s)
Hsu, Tzu-Chien
Abstract
Quantified Boolean Satisfiability (QSAT) is a powerful representation since any problem in PSPACE can be encoded naturally and compactly as QSAT. Due to its representational power, QSAT is gaining increasing research attention, and many effective quantified Boolean formula(QBF) solvers have been developed recently, yet these solvers remain premature and awaits further breakthroughs for industrial applications. There are two main procedures used for QBF solver, including solution learning and conflict learning. One of the main researches about conjunctive normal form based (CNF-based) solver focuses on how to bridge the duality gap between solution learning and conflict learning, while the duality gap results from the empty initial cube database. Recent research shows that circuit information can be used as initial cube database to bridge the gap, and such technique is implemented in two state-of-the-art QBF solvers, including OOQ and QELL. OOQ is the first QBF solver to propose the definition of usable circuit information for initial cube database, and how to utilize circuit information during solution learning in resolution-based solving style. On the other hand, QELL provides a more general characterization about usable circuit information and integrate circuit information with solution learning in an expansion-based solving style. Both solvers show how circuit information helps achieve exponential speed-up. However, the circuit information reconstruction and utilization are still incomplete in three aspects: First, the reconstructible circuit information is still restricted. Second, only circuit information can be used as initial cube database. Third, circuit information is not fully utilized in the solution learning of QELL. This thesis proposes improvement methods for these three aspects. This thesis shows how to recover more hidden circuit information in addition to Tseitin transformation pattern, and proposes a method to recover initial cubes uncovered by circuit information. This thesis also gives a modified solution learning method to utilize circuit information for QELL. The new proposed methods for reconstructing and utilizing circuit information are implemented in QELL solver, and instances are provided to evidence the contribution of this thesis.
Subjects
QBF solving
levelized solution learning
circuit reconstruction
initial cube recovery
levelized solution learning with circuit
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-105-R02943082-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):214511a679ee87dda45848fabc881dc6