# A Two-Watched Literal Scheme for First-Order Logic

arXiv: https://arxiv.org/abs/2605.21335 · HTML: https://mlsanity.com/paper/2605.21335/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 May 2026.

## Built on by (most cited first, 1 of 1)

- [Extending SMT Solving with Non-Ground Clause Learning](https://mlsanity.com/paper/2609.11509/) (2026)

## Abstract (arXiv)

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.