Professor Jie-Hong Roland Jiang

Mr. Valeriy Balabanov

Dept. of Electrical Engineering, National Taiwan University

Speech Title: Resolution Proofs and Skolem Functions in QBF Evaluation and Applications

Abstract:
Quantified Boolean formulas (QBFs) allow compact encoding of many decision problems. Their importance motivated the development of fast QBF solvers. Certifying the results of a QBF solver not only ensures correctness, but also enables certain synthesis and verification tasks particularly when the certificate is given as a set of Skolem functions. To date the certificate of a satisfiable formula can be in the form of either a (term) resolution proof or a Skolem-function model whereas that of an unsatisfiable formula is in the form of a (clause) resolution proof. The resolution proof and Skolem-function model are somewhat unrelated. We strengthen their connection by showing that, given a satisfiable QBF, its Skolem-function model is derivable from its term-resolution proof of satisfiability as well as from its clause-resolution proof of unsatisfiability under formula negation. Consequently Skolem-function derivation can be decoupled from Skolemization-based solvers and computed from standard search-based ones. Fundamentally different from prior methods, our derivation in essence constructs Skolem functions following the variable quantification order. It permits constructing a subset of Skolem functions of interests rather than the whole, and is particularly desirable in many applications. Experimental results show the robust scalability and strong benefits of the new method.