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

  1. 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).
    certification
    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.


  2. 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|
    1Adder25/8253825993.1434.8s133.3s0.1s389813100
    2adder8/82775374332114.2s3890.6s2s131263248
    3blocks3/3296303020.4s0.1s0s8665
    4chain12/1219981117421.4s0.5s0.3s145019
    5comp4/430081630.3s0.1s0s16729
    6counter47/643168319.82421.5s143.7s0.3s2485663
    7k_d4_n8/81056374431.351s430.6s1.4s683228429
    8k_grz_n8/8542198716203.4s2.7s0.1s11541845
    9k_ph_n7/8787102933.191.3s1.8s0.5s1725464
    10k_poly_n8/8701158255.512.3s20.9s0.1s2108724
    11mutex7/788904173194.6s103.6s0.3s332641616
    12toilet_g7/75020420s0.1s0s4930
    13tree5/5403810s0.1s0s2158



  3. 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?
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.



back