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 #varavg #clauseavg #alttot **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 11 mutex 7/7 8890 4173 1 94.6s 103.6s 0.3s 3326 41616 12 toilet_g 7/7 50 204 2 0s 0.1s 0s 49 30 13 tree 5/5 40 38 1 0s 0.1s 0s 21 58
- 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.
strategies, models, policies. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||