A suite comprised of QuBE-CERT and CHECKER. QuBE-CERT is an extension of QuBE 3.1, a solver leveraging Conflict/Solution AND-OR search as its main algorithm. During the search QuBE constructs two different sets: (i) A, a set of clauses, and (ii) B a set of terms. The elements of A and B are the reasons computed during the search phase. Moreover, to each reason QuBE associates the set of clauses/terms that generated it while backtracking. In normal operations, QuBE does not record such intermediate steps, and QuBE-CERT adds to QuBE the instrumentation required to store them in A and B together with the corresponding reasons. QuBE-CERT also keeps track of the last empty clause (term) derived by QuBE, closing the proof of the truth value of the formula. Starting from the output of QuBE-CERT, and if the input formula was false, CHECKER checks that each clause in A has been correctly generated starting from the empty clause. On the other hand, if the input formula was true, CHECKER checks that each term in B has been correctly generated. In essence, the set of elements in A are a clause- resolution proof, while the set of elements in B are a term-resolution proof with model generation.
Please cite this paper when referencing ChEQ:
Massimo Narizzano, Claudia Peschiera, Luca Pulina, Armando Tacchella:
Evaluating and certifying QBFs: A comparison of state-of-the-art tools. AI Commun. 22(4): 191-210 (2009)