Using Resolution Proofs to Analyse CDCL Solvers

AbstractWe investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3–4):117–134, 2007) and Nalon et al. (in: Automated reasoning with analytic Tableaux and related methods—24th international conference, (TABLEAUX’15), pp 185–200, 2015), which form the basis of modal theorem proving (Nalon et al., in: Proceedings of the twenty-sixth international joint conference on artificial intelligence (IJCAI’17), pp 4919–4923, 2017). We complement these calculi by a new tighter variant and show that proofs can be efficiently translated between all these variants, meaning that the calculi are equivalent from a proof complexity perspective. We then develop the first lower bound technique for modal resolution using Prover–Delayer games, which can be used to establish “genuine” modal lower bounds for size of dag-like modal resolution proofs. We illustrate the technique by devising a new modal pigeonhole principle, which we demonstrate to require exponential-size proofs in modal resolution. Finally, we compare modal resolution to the modal Frege systems of Hrubeš (Ann Pure Appl Log 157(2–3):194–205, 2009) and obtain a “genuinely” modal separation.

Download Full-text

Two Techniques for Minimizing Resolution Proofs

Theory and Applications of Satisfiability Testing – SAT 2010 - Lecture Notes in Computer Science ◽

10.1007/978-3-642-14186-7_26 ◽

2010 ◽

pp. 306-312 ◽

Cited By ~ 11

Author(s):

Scott Cotton

Keyword(s):

Resolution Proofs

Download Full-text

Lifting propositional proof compression algorithms to first-order logic

Journal of Logic and Computation ◽

10.1093/logcom/exaa065 ◽

2020 ◽

Author(s):

Jan Gorzny ◽

Ezequiel Postan ◽

Bruno Woltzenlogel Paleo

Keyword(s):

Propositional Logic ◽

Empirical Evaluation ◽

Order Logic ◽

Automated Deduction ◽

First Order Logic ◽

Compression Algorithms ◽

International Conference ◽

First Order ◽

Theorem Provers ◽

Resolution Proofs

Abstract Proofs are a key feature of modern propositional and first-order theorem provers. Proofs generated by such tools serve as explanations for unsatisfiability of statements. However, these explanations are complicated by proofs which are not necessarily as concise as possible. There are a wide variety of compression techniques for propositional resolution proofs but fewer compression techniques for first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. The first approach lifted from propositional logic delays resolution with unit clauses, which are clauses that have a single literal. The second approach is partial regularization, which removes an inference $\eta $ when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from $\eta $ to the root of the proof. This paper describes the generalization of the algorithms LowerUnits and RecyclePivotsWithIntersection (Fontaine et al.. Compression of propositional resolution proofs via partial regularization. In Automated Deduction—CADE-23—23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31–August 5, 2011, p. 237--251. Springer, 2011) from propositional logic to first-order logic. The generalized algorithms compresses resolution proofs containing resolution and factoring inferences with unification. An empirical evaluation of these approaches is included.

Download Full-text

Tree resolution proofs of the weak pigeon-hole principle

Proceedings 16th Annual IEEE Conference on Computational Complexity ◽

10.1109/ccc.2001.933873 ◽

2002 ◽

Cited By ~ 1

Author(s):

S. Dantchev ◽

S. Riis

Keyword(s):

Pigeon Hole Principle ◽

Resolution Proofs ◽

Tree Resolution

Download Full-text

A feasibly constructive lower bound for resolution proofs

Information Processing Letters ◽

10.1016/0020-0190(90)90141-j ◽

1990 ◽

Vol 34 (2) ◽

pp. 81-85 ◽

Cited By ~ 6

Author(s):

Stephen Cook ◽

Toniann Pitassi

Keyword(s):

Lower Bound ◽

Resolution Proofs

Download Full-text

Polynomial-size Frege and resolution proofs of st-connectivity and Hex tautologies

Theoretical Computer Science ◽

10.1016/j.tcs.2006.03.011 ◽

2006 ◽

Vol 357 (1-3) ◽

pp. 35-52 ◽

Cited By ~ 5

Author(s):

Samuel R. Buss

Keyword(s):

Polynomial Size ◽

Resolution Proofs

Download Full-text

Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC

Formal Methods in Computer Aided Design (FMCAD'07) ◽

10.1109/famcad.2007.16 ◽

2007 ◽

Cited By ~ 12

Author(s):

Jocelyn Simmonds ◽

Jessica Davies ◽

Arie Gurfinkel ◽

Marsha Chechik

Keyword(s):

Speed Up ◽

Resolution Proofs

Download Full-text

Post Mortem Analysis of SAT Solver Proofs

10.29007/gpp8 ◽

2018 ◽

Cited By ~ 1

Author(s):

Laurent Simon

Keyword(s):

Complex Systems ◽

Learning Algorithms ◽

Point Of View ◽

Post Mortem ◽

Learning Mechanism ◽

Clause Learning ◽

Sat Solver ◽

Resolution Proofs ◽

Final Proof

Conflict-Driven Clause Learning algorithms are well known from an engineerpoint of view. Thanks to Minisat, their designs are well understood, and mostof their implementations follow the same ideas, with essentially the samecomponents. Same heuristics, fast restarts, same learning mechanism.However, their efficiency has an important drawback: they are more and morelike complex systems and harder and harder to handle. Unfortunately, only afew works are focusing on understanding them rather than improving them. Inmost of the cases, their studies are often based on a generate and testpattern: An idea is added to an existing solver and if it improves itsefficiency the idea is published and kept. In this paper, we analyse``post-mortem'' the proofs given by one typical CDCL solver,Glucose. The originality of our approach is that we only consider it as aresolution proofs builder, and then we analyze some of the proofcharacteristics on a set of selected unsatisfiable instances, by shuffling each ofthem 200 times. We particularly focus on trying to characterize useless anduseful clauses in the proof as well as proofs shapes. We also show thatdespite their incredible efficiency, roughly 90% of the time spent in aCDCL is useless for producing the final proof.

Download Full-text