Unified Certification of Quantified Boolean Formula Evaluation

Quantified Boolean Formulas (QBFs) have been widely used in many practical applications,
such as: model checking, automated planning, non-monotonic reasoning, scheduling,
multi-agent scenarios, etc. Many effective state-of-the-art QBF tools have been developed.
However only a few of the modern solvers can certify their answer.
The importance of QBF certification is two-fold.
First, it ensures the correctness of a solver.
Second, perhaps more importantly, if the certificate is in an
appropriate form (specifically, in Skolem/Herbrand functions), it
enables certain synthesis tasks.
The accepted types of certificates are cube resolution proofs and
Skolem functions for true QBFs, and clause resolution proofs for false QBFs.
The current understanding about QBF certification is incomplete in two aspects.
First, the certificate of false QBFs has the missing Skolem-function counterpart.
Second, the connection between resolution proofs and Skolem functions remains unclear.
These two open questions are resolved in this thesis by bridging
the connection between the syntactic (resolution) certificates
and the semantic (Skolem-function) certificates, and by piecing
out the missing Herbrand-function certificates for false QBFs.
Essentially we derive Skolem models from cube resolution proofs
and Herbrand countermodels from clause resolution proofs for true and false QBFs, respectively.

Practical experience suggests that our approach in combination with some existing
QBF solvers can generate many more Skolem models and Herbrand countermodels
than prior methods. It enables applications, such as: relation determinization problems,
maximum sequential diameter problems, and other.
We hope, that this work will encourage QBF-based solving methods in modern logic-synthesis and verification
problems.