William Klieber

AIJ Journal 2016 Journal Article

Solving QBF with counterexample guided refinement

• Mikoláš Janota
• William Klieber
• Joao Marques-Silva
• Edmund Clarke

SAT Conference 2012 Conference Paper

Solving QBF with Counterexample Guided Refinement

• Mikolás Janota
• William Klieber
• João Marques-Silva 0001
• Edmund M. Clarke

Abstract We propose two novel approaches for using Counterexample-Guided Abstraction Refinement (CEGAR) in Quantified Boolean Formula (QBF) solvers. The first approach develops a recursive algorithm whose search is driven by CEGAR (rather than by DPLL). The second approach employs CEGAR as an additional learning technique in an existing DPLL-based QBF solver. Experimental evaluation of the implemented prototypes shows that the CEGAR-driven solver outperforms existing solvers on a number of families in the QBF-LIB and that the DPLL solver benefits from the additional type of learning. Thus this article opens two promising avenues in QBF: CEGAR-driven solvers as an alternative to existing approaches and a novel type of learning in DPLL.

SAT Conference 2010 Conference Paper

A Non-prenex, Non-clausal QBF Solver with Game-State Learning

• William Klieber
• Samir Sapra
• Sicun Gao
• Edmund M. Clarke

Abstract We describe a DPLL-based solver for the problem of quantified boolean formulas (QBF) in non-prenex, non-CNF form. We make two contributions. First, we reformulate clause/cube learning, extending it to non-prenex instances. We call the resulting technique game-state learning. Second, we introduce a propagation technique using ghost literals that exploits the structure of a non-CNF instance in a manner that is symmetric between the universal and existential variables. Experimental results on the QBFLIB benchmarks indicate our approach outperforms other state-of-the-art solvers on certain benchmark families, including the tipfixpoint and tipdiam families of model checking problems.