@inproceedings{593885b34f564c70ac7bc9e90a040e25,
title = "SAT-Inspired Eliminations for Superposition",
abstract = "Optimized SAT solvers not only preprocess the clause set, they also transform it during solving as inprocessing. Some preprocessing techniques have been generalized to first-order 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.",
author = "P. Vukmirovic and J. Blanchette and M.J.H. Heule",
year = "2021",
month = oct,
doi = "10.34727/2021/isbn.978-3-85448-046-4_32",
language = "English",
series = "Conference Series: Formal Methods in Computer-Aided Design",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "231--240",
editor = "Ruzica Piskac and Whalen, {Michael W.} and Hunt, {Warren A.} and Georg Weissenbacher",
booktitle = "Proceedings of the 21st Formal Methods in Computer-Aided Design - FMCAD 2021",
address = "United States",
note = "21st International Conference on Formal Methods in Computer-Aided Design, FMCAD 2021 ; Conference date: 18-10-2021 Through 22-10-2021",
}