Boundary Points and Resolution

We use the notion of boundary points to study resolution proofs. Given a CNF formula F, a lit(x)-boundary point is a complete assignment falsifying only clauses of F having the same literal lit(x) of variable x. A lit(x)-boundary point mandates a resolution on variable x. Adding the resolvent of this resolution to F eliminates this boundary point. Any resolution proof has to eventually eliminate all boundary points of F. Hence one can study resolution proofs from the viewpoint of boundary point elimination. We use equivalence checking formulas to compare proofs of their unsatisfiability built by a conflict driven SAT-solver and very short proofs tailored to these formulas. We show experimentally that in contrast to proofs generated by this SAT-solver, almost every resolution of a specialized proof eliminates a boundary point. This implies that one may use the share of resolutions eliminating boundary points as a metric for proof quality.

• Type: Conference
• Year: 2009
• Where: SAT
• Authors: Eugene Goldberg
• Keywords: Boundary Points, Hardware, Resolution Proofs, SAT 2009, Variable X