Spanning Matrices via Satisfiability Solving
<|reference_start|>Spanning Matrices via Satisfiability Solving: 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.<|reference_end|>
@article{eisenhofer2024spanning,
    title={Spanning Matrices via Satisfiability Solving},
    author={Clemens Eisenhofer, Michael Rawson, Laura Kov'acs},
    journal={arXiv preprint arXiv:2402.10610},
    year={2024},
    archivePrefix={arXiv},
    eprint={2402.10610},
    primaryClass={cs.LO}
}