Verification of Proofs of Unsatisfiability for CNF formulas

As SAT-algorithms become more and more complex, there is little chance of writing a SAT-solver that is free of bugs. So it is of great importance to be able to verify the information returned by a SAT-solver. If the CNF formula to be tested is satisfiable, solution verification is trivial and can be easily done by the user. However, in the case of unsatisfiability, the user has to rely on the reputation of the SAT-solver. We describe an efficient procedure for checking the correctness of unsatisfiability proofs. As a by-product, the proposed procedure finds an unsatisfiable core of the initial CNF formula. The efficiency of the proposed procedure was tested on a representative set of large “real-life” CNF formulas from the formal verification domain