On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers

摘要

SAT solvers are nowadays used in many applications where the UNSAT result has a special meaning that is at time critical. SAT instances sometimes exhibit symmetries which can be exploited to produce short proofs that would have been exponential for resolution alone. However, current unsatisfiability proof formats do not support symmetrical learning on which dynamic symmetry handling is based. We present in this paper a new proof format called DSRUP (Delete Symmetry Reverse Unit Propagation) which is an extension of DRUP (Delete Reverse Unit Propagation) and that is devised to certify UNSAT claims of SAT solvers implementing symmetrical learning. We first show that the problem of verifying symmetries of a CNF formula is Turing NP-hard. This led us to the definition of a new type of symmetry called RUP-symmetry, a class of symmetries more general than syntactic symmetries that can be efficiently checked. The DSRUP proof format is formally described and a verification algorithm is provided to validate DSRUP certificates. Finally, we provide experimental results obtained with the state-of-the-art dynamic symmetry-handling-based SAT solvers on unsatisfiable symmetric benchmarks drawn from SAT competitions, using an implementation of the DSRUP checking algorithm.