SAT-Inspired Eliminations for Superposition - Archive ouverte HAL Access content directly
Conference Papers Year :

SAT-Inspired Eliminations for Superposition

(1) , (2, 3) , (4)
1
2
3
4

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 firstorder logic with equality. In this paper, we port inprocessing techniques to work with superposition, and we strengthen preprocessing. 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.
Fichier principal
Vignette du fichier
satelimsup_paper.pdf (191.02 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03485200 , version 1 (17-12-2021)

Identifiers

Cite

Petar Vukmirović, Jasmin Blanchette, Marijn J H Heule. SAT-Inspired Eliminations for Superposition. FMCAD 2021 - 21st International Conference on Formal Methods in Computer-Aided Design, Oct 2021, New Haven, CT / virtual, United States. pp.231-240, ⟨10.5281/zenodo.4552499⟩. ⟨hal-03485200⟩
16 View
12 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More