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.

翻译：我们提出了一种新的一阶连接方法编码，将其转化为布尔可满足性问题。该编码摒弃了连接方法中树状表示的呈现方式，转而采用矩阵形式，因为我们证明在可满足性求解的背景下，树状演算存在若干缺陷。矩阵设置允许对基本连接演算进行多种全局改进。我们还证明，经过适当改进的演算是伯奈斯-舍恩芬克尔类的一个判定过程。