The sKizzo/ozziKs couple (here) allows you to produce and verify certificates of satisfiability for QBFs (see Item 1 below).
A certificate of satisfiability for a QBF is a compact representation of one of its models providing solver-independent evidence of satisfiability (see Item 2). In addition, it can be inspected to gather explicit information about the
semantics of the formula (see Item 3).
One last thing: You are likely to find alternative names for referring to QBF certificates
in the literature.
A few of such names are: strategies, models, policies.
- Within the sKizzo suite, instance evaluation is decoupled from model reconstruction, with
almost no overhead for the former, and a clear semantics for the latter. The two meshes of the chain are connected
through an inference log, produced by the solver (sKizzo), and subsequently read by the model/certificate
The log contains all the information necessary to perform the inductive model reconstruction procedure (as published here):
rollback/commit entries to trace the status of the transactional inference
engine of sKizzo, a detailed representation of all the (ground and symbolic) instantiations of inference rules exercised, context switches
among inference styles, working hypotheses addition/withdrawal for branching reasoning, a representation of inverse groundization
functions to interpret propositional models of SAT sub-instances, and more.
- The validity of a certificate can be verified by whoever is knowledgeable about the evaluation apparatus of the
logic (deductive capabilities are unnecessary), independently of how it was obtained. The meaning of a successful verification is twofold:
we are ensured (1) that the formula is SAT, and (2) that the certificate encodes a model.
A few experimental results on the certification of satisfiable fomulas in the QBFLIB repository are reported below.
For each family/instance we report the time taken to solve the instance (Ts), to reconstruct a certificate/model (Tr),
and to verify the certificate against the formula (Tv). The size of the inference log (number of entries) and the size of the
representation for the model/certificate (number of internal nodes in the forest of BDDs) are given as well.
| SAT families (sKizzo v0.6.1, ozziKs v0.1, P4 2.6GHz 1GB) (see them all)|
| # || Family || #inst || avg|
| tot Ts|| tot Tr|| tot Tv|| avg|
- A certificate exemplifies a definite scenario in which QBF-encoded problems reveal their satisfiability.
For example, a SAT-answer suffices to know that at least one winning strategy exists in a QBF-encoded
two-player game, but it takes a certificate to exhibit an actual strategy.
A proof-of-concept example for such strategy-synthesis-as-QBF-model-extraction
approach is reported aside (click on the TicTacToe picture aside and give it a try!).
A cgi script queries through the C library libQBM
(soon available for download) a SAT-certificate providing evidence that the answer to the (QBF-encoded version of the)
following question is ''YES'':
Given the rules of TicTacToe, can the second (O) player always prevent the first player (X) from winning?