Publications
Yannet Interian, Gabriel Corvera, Bart Selman and Ryan Williams
Finding small unsat cores to prove unsatisfiability of QBF's. In Proceedings of the Ninth International Symposium on Artificial Intelligence and Mathematics 2006, Fort Lauderdale, Florida
Abstract: We present a new approach to prove unsatisfiability for two-alternation Quantified Boolean Formulas (QBFs). Our solver WalkMinQBF combines the power of stochastic local search methods and complete SAT solvers. The solver we present is incomplete and outputs UNSAT if a certificate for unsatisfiability is found otherwise it outputs UNKNOWN.
Our solver has two main components, the first one is a local search algorithm that finds an assignment to the universal variables (a witness for unsatisfiability). The second one is a complete SAT solver (kcnfs ) that gets the subformula that results from assigning the universal variables and returns TRUE or FALSE. The algorithm finishes either after an UNSAT subformula has been found or when the cutoff time has been reached. To test our approach, we use the model for random formulas introduced in (Chen and Interian 2005).
We compare WalkMinQBF with the state-of-the-art QBF solver Ssolve. We show that WalkMinQBF outperforms Ssolve in time and in the number of formulas solved.
As a side result we have developed a stochastic local search algorithm for the minimum unsatisfiability problem (Min-SAT).
|
|
