Jie-Hong Roland Jiang, National Taiwan University

July 6, 15:00 (CEST)

A Sharp Leap from (D)QBF to (D)SSAT

Quantified Boolean formula (QBF) and Dependency QBF (DQBF) are powerful formalisms to encode and resolve decision problems in PSPACE and NEXPTIME, respectively. However, in recent AI and VLSI design applications, challenging issues emerge beyond the deterministic regime and require making decisions under uncertainty. Such tasks require not only satisfiability (SAT) solving but also model counting, a.k.a. Sharp-SAT. This talk will present our recent results in developing an SSAT solver based on integrating QBF techniques and model counting, and in generalizing DQBF to its SSAT version, namely, Dependency SSAT (DSSAT).

Randal Bryant, Carnegie Mellon University

July 6, 17:00 (CEST)

Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver

Existing proof-generating quantified Boolean formula (QBF) solvers must construct a different type of proof depending on whether the formula is false refutation) or true (satisfaction). We show that a QBF solver based on ordered binary decision diagrams (BDDs) can emit a single dual proof as it operates, supporting either outcome. This form consists of a sequence of equivalencepreserving clause addition and deletion steps in an extended resolution framework. For a false formula, the proof terminates with the empty clause, indicating conflict. For a true one, it terminates with all clauses deleted, indicating tautology. Both the length of the proof and the time required to check it are proportional to the total number of BDD operations performed. We evaluate our solver using a scalable benchmark based on a two-player tiling game.