Finding Connections via Satisfiability Solving

This paper introduces a novel SAT-based approach for connection calculi in first-order logic that encodes the proof search structure itself, presenting three distinct encodings with symmetry breaking and implementing them in the new solver upCoP to advance automated reasoning.

The Gist

Imagine you are trying to solve a massive, complex jigsaw puzzle. But instead of picture pieces, your pieces are logical statements (like "All cats are mammals" or "If it rains, the grass is wet"). Your goal is to arrange them to prove that a specific statement is true or false.

For decades, computer scientists have used two main ways to solve these puzzles:

1. The "Brute Force" Way: You keep adding new facts to your pile until you accidentally find the answer. It's like dumping the whole box of pieces on the table and hoping something fits.
2. The "Backtracking" Way: You try to build a specific path. If you hit a dead end, you go back, erase your last move, and try a different path. This is smarter, but computers often get stuck re-trying the same dead ends over and over again because they forget where they've already been.

The Big Idea: A "Smart" Puzzle Solver

This paper introduces a new method called UPCoP. The authors decided to combine the best of both worlds by using a SAT Solver (a super-fast computer program designed to solve logic puzzles) to manage the "Backtracking" method.

Think of a SAT solver as a hyper-organized project manager. It doesn't just guess; it remembers every single dead end it has ever encountered and writes a rule saying, "Never try this combination again."

The Three Main Tricks (The "Encodings")

The paper describes three different ways to translate the logic puzzle into a language the project manager (the SAT solver) understands.

1. The "Tree" Approach (Connection Tableaux)

Imagine building a tree where every branch is a guess.

• The Problem: If you have 100 branches, the tree gets huge very fast. The project manager gets overwhelmed by the sheer number of branches and forgets the big picture. It's like trying to navigate a forest by looking at every single leaf individually.
• The Result: This method works, but it's slow and clunky because the computer spends too much time managing the branches rather than solving the logic.

2. The "Matrix" Approach (The Grid)

Instead of a tree, imagine a grid or a spreadsheet.

• The Metaphor: Instead of building a tree, you lay out all your puzzle pieces in a big grid. You then draw lines connecting pieces that fit together (like connecting "Rain" to "Wet Grass").
• The Goal: You want to find a set of connections that covers the entire grid so there are no loose ends.
• Why it's better: This is much friendlier to the project manager. It turns the problem into a giant "Yes/No" checklist. The computer can quickly say, "Okay, if I connect Piece A to Piece B, I can't connect Piece A to Piece C." It's a much more efficient way to search.

3. The "Smart Growth" Approach (Iterative Deepening with Unsat Cores)

This is the paper's secret sauce.

• The Scenario: Imagine you are trying to build a bridge, but you don't know how many planks you need.
• The Mistake: You could try to build a bridge with 1,000 planks immediately. That's a waste of time if you only needed 5.
• The Solution: You start with a small pile of planks (say, 2). You ask the project manager: "Can we build a bridge with these?"
  • If the answer is NO, the manager doesn't just say "No." It gives you a receipt (called an Unsat Core). The receipt says, "You failed because you were missing a specific type of plank."
  • You look at the receipt, add just the missing planks, and try again.
• The Magic: This prevents the computer from wasting time on useless pieces. It grows the puzzle only as much as necessary, guided by the "receipts" of failure.

The "Symmetry" Problem (Avoiding Duplicates)

One of the biggest headaches in these puzzles is symmetry.

• The Metaphor: Imagine you have two identical red socks. If you try to solve a puzzle involving socks, the computer might try "Left sock on Left foot" and then "Right sock on Left foot." Since the socks are identical, these are the exact same solution. The computer wastes time solving the same puzzle twice.
• The Fix: The authors taught UPCoP to say, "If we have two identical pieces, we will always use the first one before the second one." This cuts out thousands of useless attempts instantly.

The Results: Does it Work?

The authors built a prototype solver called UPCoP and tested it against the world's best existing solvers (like meanCoP).

• The Outcome: While the old solvers are generally faster at solving easy problems, UPCoP solved 179 problems that the others couldn't solve at all.
• Why? Because UPCoP is better at finding the "hidden" solutions that require a very specific, non-obvious arrangement of pieces. It's like a detective who finds the one clue everyone else ignored.

In a Nutshell

This paper is about teaching a computer to solve logic puzzles by:

1. Turning the puzzle into a giant checklist (Matrix).
2. Using a "receipt of failure" to only add the necessary pieces (Iterative Deepening).
3. Ignoring duplicate attempts (Symmetry Breaking).

It's a shift from "guessing and checking" to "strategic planning," allowing computers to solve logic problems that were previously impossible.

Technical Summary

Here is a detailed technical summary of the paper "Finding Connections via Satisfiability Solving" by Eisenhofer, Rawson, and Kovács.

1. Problem Statement

Automated theorem proving (ATP) for First-Order Logic (FOL) typically relies on two distinct search strategies:

1. Ordering-based Saturation: Systems like Vampire or E deduce new facts to expand a search space.
2. Subgoal-Reduction: Systems like leanCoP or Setheo manipulate partial proofs and backtrack when dead-ends are reached.

The subgoal-reduction approach suffers from redundancy. Without global memory, provers may explore the same "useless" formulas repeatedly. While refinements exist, they often involve complex propositional structures (e.g., "if clauses C and D are present and substitution X is used, backtrack") that are difficult to reason about within standard ATP frameworks.

The paper addresses the challenge of integrating SAT/SMT solving capabilities (specifically learning, conflict analysis, and unsat cores) into connection calculi to manage global information and eliminate redundant search paths more effectively than traditional backtracking.

2. Methodology

The authors propose encoding the search for connection proofs (specifically connection tableaux and matrix proofs) directly as a Boolean Satisfiability (SAT) problem. Unlike traditional methods that ground FOL clauses into propositional logic to find a refutation, this method encodes the structure of the proof search itself.

The methodology evolves through three distinct encodings:

A. Encoding Connection Tableaux ($E_T$)

• Concept: Directly maps the construction of a connection tableau to SAT variables.
• Mechanism:
  • Variables $\langle L; U \rangle$ represent a literal $L$ being a leaf at path $U$.
  • Constraints enforce that every leaf must be extended (adding a new clause) or reduced (connecting to an ancestor).
  • Unification constraints ($\langle L \sim K \rangle$) ensure connected literals can be unified.
• Limitation: This approach suffers from "pathological behavior." The number of variables grows rapidly with path depth, and the SAT solver lacks sufficient propositional structure to learn effectively, leading to exhaustive enumeration similar to non-SAT methods but with higher overhead.

B. Encoding Matrix Proofs ($E_M$)

• Concept: Shifts from tree-based tableaux to matrix representations. A matrix proof is a set of clauses where every path through the matrix contains at least one connection (a "spanning set of connections").
• Mechanism:
  • Selectors ($S^k_C$): Boolean variables indicating if the $k$-th copy of clause $C$ is included in the matrix.
  • Fully Connected Constraint: Every literal in the selected matrix must connect to a literal in a different clause.
  • Spanning Constraint: If an "open path" (a path with no connections) is detected, the solver is forced to add a connection to close it.
• Advantage: This creates a combinatorial problem better suited for SAT solvers. It allows a single matrix proof to represent multiple tableau proofs, reducing redundancy.

C. Iterative Deepening via Unsat Core Refinement ($E_U$)

• Concept: Addresses the inefficiency of $E_M$ where the solver eagerly creates $d$ copies of every clause, even if fewer are needed.
• Mechanism:
  • Uses Abstraction-Refinement. Initially, only one copy of each clause is allowed.
  • If the solver finds the problem unsatisfiable, it returns an Unsat Core.
  • If the core indicates that a specific clause $C$ was needed in higher multiplicity (e.g., the assumption that "no more copies of $C$ are needed" caused the conflict), the multiplicity $\mu(C)$ is incremented.
  • This allows the solver to dynamically determine the necessary number of clause copies without guessing a global depth limit.

D. Symmetry Breaking and Redundancy Elimination

To further optimize the search, the authors introduce specific symmetry-breaking constraints:

1. Multiplicity Symmetry: Enforces an order on clause copies (e.g., copy $i$ can only be selected if copy $i-1$ is selected) to prevent the solver from trying interchangeable copies.
2. Instance Symmetry: Uses a total ordering on input clauses to prevent selecting a clause $D$ if a "smaller" clause $C$ could serve the same purpose (based on subsumption logic adapted for connection calculus).
3. Substitution Symmetry: Enforces an ordering on substitutions applied to variables in different copies of the same clause to avoid exploring symmetric substitution permutations.

3. Key Contributions

1. Novel Encodings: Introduced three SAT encodings ($E_T, E_M, E_U$) for connection calculi, proving their soundness and completeness.
2. Theoretical Analysis: Established that solving the matrix encoding $E_M$ falls within the complexity class $\Sigma^P_2$, matching the theoretical bound for checking satisfiability over rigid variables.
3. Iterative Deepening via Unsat Cores: Developed a method to use unsat cores to guide the multiplicity of clause copies, avoiding the "overkill" of generating unnecessary clause instances.
4. Symmetry Breaking: Proposed specialized symmetry-breaking techniques tailored to the structure of connection proofs (multiplicity, instance, and substitution symmetries).
5. Implementation (UPCoP): Implemented these techniques in a new prototype solver, UPCoP, which interfaces with CaDiCaL (SAT) and Z3 (SMT).

4. Experimental Results

The authors evaluated UPCoP on the TPTP 8.2.0 benchmark set (6,468 provable problems) against the state-of-the-art solver meanCoP.

• Performance: While UPCoP solved fewer total problems than meanCoP (1,272 vs. 1,972), it demonstrated unique capabilities.
• Unique Successes: UPCoP solved 179 problems that meanCoP could not solve.
• Reasons for Success:
  • Smaller Proofs: UPCoP often found matrix proofs that were structurally smaller than the tableau proofs required by meanCoP.
  • Clause Filtering: The unsat-core based approach successfully deduced that certain clauses were irrelevant to the proof, allowing the solver to ignore them and speed up the search.
• Solver Comparison: The SMT-based version (Z3) and SAT-based version (CaDiCaL) showed complementary strengths, with the hybrid encoding ($E_H$) performing particularly well on problems where most input clauses were used but only a few times.

5. Significance

This paper represents a significant shift in how automated theorem provers handle search space management.

• Paradigm Shift: Instead of using SAT solvers merely to check ground unsatisfiability (Herbrand refutation), the authors use them to manage the global state of the proof search, handling backtracking and redundancy elimination via learned constraints.
• Efficiency: By encoding the proof structure directly and using unsat cores for iterative deepening, the approach avoids the "combinatorial explosion" of generating unnecessary clause copies.
• Future Directions: The work highlights that while modern SAT solvers are powerful, their standard heuristics (like conflict learning) sometimes struggle with the specific symmetries of FOL proofs. The authors suggest that custom conflict learning engines (as explored in their follow-up work, hopCoP) may be necessary to fully unlock the potential of SAT-based connection proving.

In summary, the paper successfully demonstrates that SAT-based methods with symmetry breaking and unsat-core guided refinement offer a viable and powerful alternative to traditional backtracking in connection calculi, capable of solving problems that are intractable for current state-of-the-art subgoal-reduction provers.