Boundary Points and Resolution Export

@incollection{gsat09, abstract = {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 variablex. 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.}, author = {Goldberg, Eugene}, citeulike-article-id = {6074605}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-02777-2_16}, citeulike-linkout-1 = {http://www.springerlink.com/content/e32w6846273323g6}, doi = {10.1007/978-3-642-02777-2_16}, journal = {Theory and Applications of Satisfiability Testing - SAT 2009}, keywords = {cdcl, proof-complexity, resolution}, pages = {147--160}, posted-at = {2009-11-05 14:36:34}, priority = {2}, title = {Boundary Points and Resolution}, url = {http://dx.doi.org/10.1007/978-3-642-02777-2_16}, year = {2009} }

TY - CHAP ID - gsat09 L3 - citeulike-article-id:6074605 N2 - 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 variablex. 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. JF - Theory and Applications of Satisfiability Testing - SAT 2009 EP - 160 TI - Boundary Points and Resolution SP - 147 KW - cdcl KW - proof-complexity KW - resolution AU - Goldberg, Eugene PY - 2009/// UR - http://dx.doi.org/10.1007/978-3-642-02777-2_16 ER -