A Curiously Effective Backtracking Strategy for Connection Tableaux
Michael Färber
TL;DR
This work tackles backtracking in connection-tableaux proof search, where completeness and efficiency hinge on how alternative proofs are explored after a literal is solved. It introduces less restricted backtracking via exclusive cuts, formalized as exclusive cuts on extension steps ($EX$) that preserve variants starting with a different root step, alongside reductions ($R$) and inclusive cuts ($EI$ and $REI$), producing the combined strategies $REI$ and $REX$. The author implements a Rust prover, meanCoP, with a tiny proof checker and WASM-targeted code, and demonstrates that $REX$ yields up to 19% more solved problems than the prior best strategy, outperforming leanCoP-REI and fleanCoP-REI on several first-order datasets. The results highlight the practical benefits of exclusive cuts for conjecture-directed search and motivate portfolio approaches that combine multiple backtracking strategies for further gains.
Abstract
Automated proof search with connection tableaux, such as implemented by Otten's leanCoP prover, depends on backtracking for completeness. Otten's restricted backtracking strategy loses completeness, yet for many problems, it significantly reduces the time required to find a proof. I introduce a new, less restricted backtracking strategy based on the notion of exclusive cuts. I implement the strategy in a new prover called meanCoP and show that it greatly improves upon the previous best strategy in leanCoP.