A Two-Watched Literal Scheme for First-Order Logic

TL;DR

This paper extends the two-watched literal scheme from propositional to first-order logic, providing an efficient algorithm for clause propagation and conflict detection with formal proofs and practical implementation.

Contribution

It introduces a lifted two-watched literal scheme for first-order logic, including a formal algorithm, proof of correctness, and an implementation demonstrating improved performance.

Findings

Outperforms standard dynamic programming in detecting propagatable literals.

Provides a sound and complete algorithm for first-order clause propagation.

Implementation shows efficiency gains, especially with long clauses.

Abstract

The two-watched literal scheme, a core component of efficient CDCL (Conflict-Driven Clause Learning) implementations for propositional logic, is extended to first-order logic. Given a set of first-order clauses and a set of ground literals, our lifted two-watched literal scheme efficiently detects all propagating and false clauses with respect to the ground literals. We present the algorithm as a system of rules and prove its soundness and completeness. Additionally, we provide an implementation of the two-watched literal scheme, which outperforms a standard dynamic programming approach for detecting propagatable literals and conflicts, especially when dealing with long clauses.