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).
    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
    tot Ts tot Tr tot Tv avg