Light-Weight Integration of SAT Solving into First-Order Reasoners – First Experiments
We describe a light-weight integration of the propositional SAT solver PicoSAT and the saturation-based superposition prover E. The proof search is driven by the saturation prover. Periodically, the saturation is interrupted, and all first-order clauses are grounded. The resulting ground problem is converted to a propositional format and handed to the SAT solver. If the SAT solver reports unsatisfiability, the proof is extracted and reported on the first-order level. First experiments demonstrate the viability of the approach and suggest future extensions. They also yield interesting information about the structure of the search space.
2018 ◽
Keyword(s):
2018 ◽
Keyword(s):
2020 ◽
Vol 34
(02)
◽
pp. 1644-1651
Keyword(s):
2018 ◽
Keyword(s):
Keyword(s):