Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Spanning Matrices via Satisfiability Solving

Clemens Eisenhofer, Michael Rawson, Laura Kovács

TL;DR

The paper addresses proving first-order logic statements by encoding Bibel's connection method as SAT, arguing that a matrix-based representation yields stronger global refinements than traditional tableau approaches. It develops two encodings: $\\mathcal{E}_T$ for tableau-based proofs and a matrix-centric encoding $\\mathcal{E}_M$, then strengthens the approach with an unsat-core guided refinement $\\mathcal{E}_U$. The work establishes soundness, completeness, and termination for fixed resources, with a $\\Sigma_2^P$ complexity characterization, and demonstrates how iterative deepening and symmetry reductions can yield a practical decision procedure, including for the Bernays–Schönfinkel class and the effectively propositional fragment. It lays groundwork for integrating SAT-based proof search with global refinements, backtracking, and AVATAR-style splitting, with future work oriented toward implementation and empirical evaluation.

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önfinkel class.

Spanning Matrices via Satisfiability Solving

TL;DR

The paper addresses proving first-order logic statements by encoding Bibel's connection method as SAT, arguing that a matrix-based representation yields stronger global refinements than traditional tableau approaches. It develops two encodings: for tableau-based proofs and a matrix-centric encoding , then strengthens the approach with an unsat-core guided refinement . The work establishes soundness, completeness, and termination for fixed resources, with a complexity characterization, and demonstrates how iterative deepening and symmetry reductions can yield a practical decision procedure, including for the Bernays–Schönfinkel class and the effectively propositional fragment. It lays groundwork for integrating SAT-based proof search with global refinements, backtracking, and AVATAR-style splitting, with future work oriented toward implementation and empirical evaluation.

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önfinkel class.
Paper Structure (16 sections, 5 theorems, 12 equations, 3 figures)

This paper contains 16 sections, 5 theorems, 12 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Satisfiability Solving
  4. Connection Tableaux
  5. The Connection Method, Matrices, and Spanning Connections
  6. Encoding Connection Tableaux
  7. Connection tableau rules as SAT.
  8. Unification Constraints.
  9. SAT Encoding of Closed Connection Tableaux.
  10. Pathological Behaviour.
  11. Encoding Matrices
  12. Encoding Overview
  13. Fully Connected Matrices
  14. Spanning Sets of Connections
  15. Correctness and Complexity of Matrix Encodings
  16. ...and 1 more sections

Key Result

theorem thmcountertheorem

Suppose $M$ is minimal and has a spanning set of connections. Then $M$ is fully connected.

Figures (3)

  • Figure 1: Connection tableau rules, left-to-right: start, extension, and reduction. In start and extension, $L \vee \ldots \vee K$ is a freshly-renamed copy of a clause from the input problem. In extension and reduction, $L$ is connected to $L'$ using $\sigma$.
  • Figure 2: Matrix versus tableau proofs. Clauses are written vertically in matrices. Curved lines indicate connections. $\sigma$ is computed such that e.g. $\sigma(z^1) = f(y^1)$.
  • Figure 3: Unfinished matrix proof. An open path is shown in bold.

Theorems & Definitions (9)

  • theorem thmcountertheorem: Fully Connected Matrix
  • proof
  • theorem thmcountertheorem: Soundness
  • proof
  • theorem thmcountertheorem: Completeness
  • proof
  • theorem thmcountertheorem: Complexity Bound
  • proof
  • corollary thmcountercorollary: Termination