Spanning Matrices via Satisfiability Solving
Logic in Computer Science
2024-02-19 v1
Abstract
We propose a new encoding of the first-order connection method as a Boolean satisfiability problem. The encoding eschews tree-like presentations of the connection method in favour of matrices, as we show that tree-like calculi have a number of drawbacks in the context of satisfiability solving. The matrix setting permits numerous global refinements of the basic connection calculus. We also show that a suitably-refined calculus is a decision procedure for the Bernays-Sch\"onfinkel class.
Cite
@article{arxiv.2402.10610,
title = {Spanning Matrices via Satisfiability Solving},
author = {Clemens Eisenhofer and Michael Rawson and Laura Kovács},
journal= {arXiv preprint arXiv:2402.10610},
year = {2024}
}