On-the-Fly Lazy Clause Simplification Based on Binary Resolvents

This paper describes techniques for simplifying a propositional clausal formula during the search process of the satisfiability checking of the formula. Generally, simplification technique has a trade-off between the checking cost and the effect of it. If the simplification technique is executed during search, then the cost can be problematic. We propose some on-the-fly simplification techniques whose computational cost is negligibly small. Hence, these techniques are executed frequently throughout the process of a CDCL solver, that is, unit propagation, conflict analysis, removal of satisfied clauses, etc. The proposed simplification techniques are based on binary resolvents, which are derived from unit propagation process, and consist of various probing techniques, self-subsuming resolution and on-demand addition of binary resolvents. The experimental results show that these simplification techniques can improve the performance of CDCL solvers.