|
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).
- 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 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 #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 |
|
|