Vukmirović, P., Blanchette, J., & Heule, M. (2021). SAT-Inspired Eliminations for Superposition. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 231–240). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_32
Optimized SAT solvers not only preprocess the
clause set, they also transform it during solving as inprocessing.
Some preprocessing techniques have been generalized to firstorder
logic with equality. In this paper, we port inprocessing
techniques to work with superposition, a leading first-order proof
calculus, and we strengthen known preprocessing techniques.
Specifically, we look into elimination of hidden literals, variables
(predicates), and blocked clauses. Our evaluation using the
Zipperposition prover confirms that the new techniques usefully
supplement the existing superposition machinery.
CC BY 4.0
