
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 solverindependent 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).
 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
reconstructor (ozziKs).
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 subinstances, 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 #var  avg #clause  avg #alt   tot Ts  tot Tr  tot Tv  avg log  avg model  1  Adder2   5/8  2538  2599  3.1   434.8s  133.3s  0.1s  3898  13100  2  adder   8/8  2775  3743  3   2114.2s  3890.6s  2s  1312  63248  3  blocks   3/3  296  3030  2   0.4s  0.1s  0s  86  65  4  chain   12/12  1998  11174  2   1.4s  0.5s  0.3s  1450  19  5  comp   4/4  300  816  3   0.3s  0.1s  0s  167  29  6  counter   47/64  316  831  9.8   2421.5s  143.7s  0.3s  24856  63  7  k_d4_n   8/8  1056  3744  31.3   51s  430.6s  1.4s  6832  28429  8  k_grz_n   8/8  542  1987  16   203.4s  2.7s  0.1s  1154  1845  9  k_ph_n   7/8  787  10293  3.1   91.3s  1.8s  0.5s  1725  464  10  k_poly_n   8/8  701  1582  55.5   12.3s  20.9s  0.1s  2108  724 

