Persistent and Quasi-Persistent Lemmas in Propositional Model Elimination

Model elimination is a back-chaining strategy to search for and construct resolution refutations. Recent extensions to model elimination, implemented in Modoc, have made it a practical tool for satisfiability checking, particularly for problems with known goals. Many formulas can be refuted more succinctly by recording certain derived clauses, called lemmas. Lemmas can be used where a clause of the original formula would normally be required. However, recording too many lemmas overwhelms the proof search. Lemma management has a significant effect on the performance of Modoc. Earlier research studied pure persistent (global) strategies, and pure unit-lemma (local) strategies. This paper describes and evaluates a hybrid strategy to control the lifetime of lemmas, as well as a new technique for deriving certain lemmas efficiently, using a lazy strategy. Unit lemmas are recorded locally as in previous practice, but certain lemmas that are considered valuable are asserted globally. A range of functions for estimating value is studied experimentally. Criteria are reported that appear to be suitable for a wide range of application-derived formulas.