Mining Propositional Simplification Proofs for Small Validating Clauses

The problem of obtaining small conflict clauses in SMT systems has received a great deal of attention recently. We report work in progress to find small subsets of the current partial assignment that imply the goal formula when it has been propositionally simplified to a boolean value. The approach used is algebraic proof mining. Proofs from a propositional reasoner that the goal is equivalent to a boolean value (in the current assignment) are viewed as first-order terms. An equational theory between proofs is then defined, which is sound with respect to the quasi-order “proves a more general set theorems.” The theory is completed to obtain a convergent rewrite system that puts proofs into a canonical form. While our canonical form does not use the smallest subset of the current assignment, it does drop many unnecessary parts of the proof. The paper concludes with discussion of the complexity of the problem and effectiveness of the approach.