Constraint Learning for Non-confluent Proof Search

This paper introduces and iteratively refines a constraint learning approach for the classical first-order connection calculus that significantly reduces backtracking in non-confluent proof search while preserving completeness.

The Gist

Here is an explanation of the paper "Constraint Learning for Non-Confluent Proof Search," translated into simple language with creative analogies.

The Big Picture: Getting Lost in a Maze

Imagine you are trying to solve a massive, complex maze. Your goal is to find a path from the entrance to the exit (a "closed tableau," or a complete proof).

In some mazes, every time you hit a dead end, you just turn around and try the next door. This is easy. But in the specific type of maze this paper talks about (called non-confluent proof search), things are trickier.

Here's the problem: In this maze, the path you took earlier might have locked a door you need to open later.

• The Scenario: You choose to go left at the start. This seems fine. But 50 steps later, you realize you need a key you left behind at the start. Because you went left, you can't get that key.
• The Old Way (Backtracking): You have to walk all the way back to the start, un-choose "left," and try "right." Then you walk 50 steps again. If that fails, you go back to the start again. This is called backtracking. If the maze is huge, you might spend your whole life walking back and forth, re-doing the same 50 steps over and over.

The Solution: Learning from Your Mistakes

The authors, Michael Rawson, Clemens Eisenhofer, and Laura Kovács, decided to give the maze-walker a notebook.

Instead of just walking back and forth blindly, the walker uses a technique called Constraint Learning. Here is how it works in everyday terms:

1. The "Stuck" Moment

Imagine you are deep in the maze. You are at a dead end. You look around and realize, "I can't go forward because I chose 'Left' at the start, and that locked the door I need."

2. The Investigation (Reasoning)

Instead of just sighing and walking back, the walker asks: "Exactly which choices led to this dead end?"

• Was it just the "Left" choice?
• Or was it "Left" combined with "Taking the red backpack"?
• Or "Left" + "Red backpack" + "Wearing blue shoes"?

The paper describes a way to pinpoint the exact combination of choices that caused the problem.

3. Writing the Rule (The Constraint)

The walker writes a rule in the notebook:

"If I ever choose 'Left' AND wear 'Blue Shoes', I will get stuck. Never do that combination again."

This is a Constraint. It's a rule that says, "Don't go down this specific path."

4. The "Backjump"

Now, when the walker is exploring a new path and realizes, "Oh, I'm wearing blue shoes and I'm about to turn Left," they don't have to walk all the way back to the start. They can instantly say, "Nope, that's a forbidden combination," and jump straight to a different part of the maze.

This is called Backjumping. It's like teleporting out of a dead end instead of walking out of it.

Why This is a Big Deal

In the world of computer logic (specifically Connection Tableaux), computers have been getting stuck in these loops for decades.

• Old computers: Like a person who forgets they've been here before. They try the same bad path millions of times.
• New computers (with this paper): Like a smart explorer who keeps a map of "Do Not Enter" zones.

The paper introduces a specific language to write these "Do Not Enter" rules. They realized that just saying "Don't go Left" isn't enough. They needed to say "Don't go Left if the variable $x$ is set to $c$." It's a very precise way of saying, "Don't do this specific thing under these specific conditions."

The Results: A Faster Search

The authors built a prototype computer program called hopCoP to test this.

• They compared it to an older program called meanCoP (which uses a "cut" rule to stop backtracking, but sometimes misses the solution).
• The Result: hopCoP solved significantly more problems in the same amount of time.
• The Trade-off: The computer has to remember all these rules (the notebook gets heavy), but the time saved by not walking in circles is worth the extra memory.

Summary Analogy

Think of it like cooking a complex meal:

• Without Constraint Learning: You try to make a cake. You realize you forgot to buy eggs. You go to the store, buy eggs, come back, and start over. Then you realize you also forgot flour. You go to the store again. You keep repeating this cycle.
• With Constraint Learning: You try to make the cake, realize you need eggs and flour. You write a note on the fridge: "Recipe X requires Eggs AND Flour." Next time you start Recipe X, you check the fridge first. If you don't have both, you don't even start the mixing bowl. You save hours of cleaning up failed attempts.

The Takeaway

This paper teaches computers how to learn from their dead ends. By analyzing why a proof search got stuck and writing down a rule to prevent that specific mistake from happening again, computers can solve complex logic puzzles much faster, without getting lost in endless loops of backtracking.

Technical Summary

Here is a detailed technical summary of the paper "Constraint Learning for Non-Confluent Proof Search" by Rawson, Eisenhofer, and Kovács.

1. Problem Statement

Automated theorem proving (ATP) often relies on backtracking search when using non-confluent proof calculi, such as the connection tableau calculus.

• The Core Issue: In non-confluent systems, the order in which proof steps (inferences) are chosen matters. A choice that seems valid at one stage may bind variables in a global substitution in a way that prevents closing other branches later. This leads to "stuck" tableaux where no further inferences are possible, forcing the solver to backtrack.
• Pathological Backtracking: While some backtracking is necessary, these systems often suffer from excess backtracking. Solvers may repeatedly explore the same dead ends because they fail to recognize that a specific combination of previous choices caused the failure.
• Limitations of Existing Solutions: Previous attempts to reduce backtracking, such as the "Prolog cut" used in the leanCoP system or various heuristics in meanCoP, are incomplete. They prune the search space effectively but risk missing valid proofs.

2. Methodology

The authors propose adapting Constraint Learning (specifically Conflict-Driven Clause Learning, or CDCL, from the SAT/SMT community) to the connection tableau calculus. The goal is to learn constraints that explain why a tableau is stuck, thereby preventing the solver from revisiting similar dead ends while maintaining completeness.

A. Constraint Language

The authors define a language to represent the "reason" a tableau is stuck.

• Initial Definition (Simplified): Constraints are sets of atoms representing specific inference steps:
  • $SC$: Starting the tableau with clause $C$.
  • $R^q_p$: A reduction from position $p$ to ancestor $q$.
  • $E^i_C/p$: Extending position $p$ using the $i$-th literal of clause $C$.
• Refined Definition: To make constraints more general and efficient, the language is decomposed into:
  • Literal Placement: $L@p$ (Literal $L$ is at position $p$).
  • Variable Bindings: $x \mapsto t$ (Variable $x$ is bound to term $t$).
  • No-Connection Atoms: $p \not\sim q$ (Positions $p$ and $q$ can never be connected, regardless of substitution).
  • Disequations: $s \neq t$ (To handle regularity and tautology elimination).

B. The Search Algorithm (Algorithm 1)

The search proceeds iteratively with a trail of decisions (atoms):

1. Select: Choose an open branch in the tableau.
2. Attempt Inference: Try to apply a rule (reduction or extension).
3. Conflict Detection:
   • If an inference is impossible due to the calculus rules, the system computes a reason (a minimal set of previous steps causing the blockage).
   • If an inference is impossible because it violates a learned constraint, the constraint itself acts as the reason.
4. Learning: When all inferences for a branch fail, the system constructs a constraint clause representing the union of reasons for failure.
5. Backjumping: The solver backtracks (undoes decisions) until the learned constraint is no longer violated, effectively skipping large portions of the search space that would lead to the same dead end.

C. Completeness and Termination

The paper proves that for a fixed depth limit (iterative deepening), the algorithm terminates. Because constraints are never forgotten within a depth limit and the number of possible tableaux is finite, the solver will eventually either find a closed tableau or learn the empty constraint (proving unsatisfiability at that depth).

3. Key Contributions

1. First Application of Constraint Learning to Connection Tableaux: The paper successfully adapts CDCL techniques to a non-confluent, first-order tableau calculus without sacrificing completeness.
2. Refined Constraint Language: The development of a specific constraint language (including "no-connection" atoms and variable bindings) that generalizes dead-end explanations beyond specific tableau derivations.
3. Prototype Implementation (hopCoP): A new theorem prover built to test these concepts, implemented in an imperative style but inspired by the lean methodology.
4. Empirical Validation: A rigorous comparison against meanCoP (a state-of-the-art connection prover with incomplete backtracking restrictions) and !meanCoP (a variant with cuts).

4. Experimental Results

The authors evaluated hopCoP against meanCoP and !meanCoP on several benchmark sets (TPTP FOF/CNF, MPTP, Miz40) with a 10-second time limit.

• Search Space Reduction: On the PUZ005-1 problem, hopCoP required significantly fewer extension steps at deeper iterative deepening levels compared to meanCoP (e.g., at depth 7, meanCoP tried ~6.4 million steps, while hopCoP tried ~48k).
• Solved Problems: Despite the overhead of maintaining learned constraints, hopCoP solved more problems than both meanCoP and !meanCoP across most benchmarks:
  • M2k: hopCoP (1,050) > !meanCoP (878) > meanCoP (795).
  • Miz40: hopCoP (13,040) > !meanCoP (9,748) > meanCoP (7,592).
  • TPTP: hopCoP (4,026) > meanCoP (3,578) > !meanCoP (3,283).
• Overhead vs. Gain: The results demonstrate that the reduction in backtracking steps outweighs the computational overhead of managing learned constraints.

5. Significance

• Completeness vs. Performance: The work bridges a critical gap in ATP. It shows that one can achieve the performance benefits of "pruning" the search space (usually associated with incomplete methods like cuts) while retaining the theoretical guarantee of completeness.
• Applicability: While focused on connection tableaux, the authors argue this approach is applicable to other non-confluent tableau calculi (e.g., intuitionistic or modal logics).
• Future Directions: The paper highlights potential intersections with Machine Learning (using learned heuristics to guide constraint learning) and suggests that future implementations could leverage exception handling mechanisms for more efficient backjumping.

In summary, this paper presents a robust method for reducing pathological backtracking in automated theorem proving by learning constraints that explain dead ends, resulting in a complete prover that outperforms existing incomplete state-of-the-art systems on standard benchmarks.