http://www.cse.ucsc.edu/~avg/ProofChecker/README-sat-2009.txt Track organizer: Allen Van Gelder, avg where? at cs.ucsc.edu In the verified-unsat track of the 2009 Sat Solver Competition, solvers produce some verification output and are only tested on unsatisfiable benchmarks. Because of the experimental nature of this track, there are no prizes and no official ranking system. See http://www.cse.ucsc.edu/~avg/ProofChecker/cert-poster-sat07.pdf for the poster shown at SAT 2007 for that year's track. We expect 2009 to be conducted similarly. There are several accepted proof formats, each with precise specifications. These formats are designed to be neutral to the solver's methodology as far as possible (in contrast to several "trace" formats proposed in the literature that are specific to the grasp/chaff style). All formats may be found at http://www.cse.ucsc.edu/~avg/ProofChecker/ , but we expect the most popular to be the RUP format, so that is described briefly in this page. The purpose of the RUP proof format is to allow a solver to "retro-fit" some verification output without too much trouble, and to allow for some possibility of derivation rules other than resolution. The short story is that solvers in the vein of grasp, chaff, berkmin, minisat, and picosat can simply output their conflict clauses (the final one being the empty clause). Also, we believe that look-ahead solvers will be able to output a RUP proof without great difficulty. Notice that it is not necessary to actually use all the clauses you output, but if the redundancy is too great, you might hit filesize limits or time limits. Practical experience is needed to see what can be achieved. The proof should be on a separate file and should consist of one 256-byte header (255 bytes plus the newline), followed by derived clauses in the usual DIMACS format. Please visit the above URL for additional details and software to check your verification output during development. The rest of this page goes into details in case there are solvers that use a different approach, or readers just want to see some examples. The idea is based on E.Goldberg, Y.Novikov. Verification of proofs of unsatisfiability for CNF formulas. Design, Automation and Test in Europe. March 2003, pp. 886--891. http://eigold.tripod.com/papers.html. The method of deriving the derived clause is not important. It might be by resolution or some other means. It is only necessary that the soundness of the derived clauses can be verified by a procedure that we call REVERSE UNIT-PROPAGATION (RUP for short). In the discussion, clauses are delimited by square brackets. Suppose that F is the input formula and D_1, ..., D_r are the derived clauses that have been output, with D_r = [] (the empty clause). The sequence D_1, ..., D_r is an RUP refutation of F if and only if: For each i from 1 through r, steps 1--3 below derive []: 1. Negate D_i = [L_{ij}] producing one or more unit clauses, [-L_{ij}]. For example, the negation of [x, y, z] is [-x], [-y], [-z]. (When i = r, there are no unit clauses produced.) 2. Add these unit clauses [-L_{ij}] and D_1 through D_{i-1} to F. (When i = r, there are no unit clauses to add.) 3. Perform unit-clause propagation. EXAMPLES Say the input file F has these clauses: c example p cnf 4 4 1 -4 -3 0 1 4 0 -1 0 -4 3 0 EXAMPLE 1 The RUP proof might be these integers (newlines are for readability): 4 3 0 0 This proof contains two derived clauses, [4 3] and []. Negating [4 3] gives [-4] and [-3], which are added to F. Then unit-clause propagation derives []. Next, add [4 3] (the first derived clause) to F, and again unit-clause propagation derives []. So the proof is verified as sound, although we have no idea why the program output [4 3] as a derived clause. EXAMPLE 2 Another correct RUP proof for F is: 0 This is because the formula itself can be refuted by unit-clause propagation. EXAMPLE 3 Another correct RUP proof for F is: 1 -3 0 1 3 0 -3 0 3 0 0 This is the sequence of resolvents in a resolution proof, but no structure is given, so that fact might not be obvious.