A Two-Watched Literal Scheme for First-Order Logic
Logic in Computer Science
2026-05-21 v1
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.
Cite
@article{arxiv.2605.21335,
title = {A Two-Watched Literal Scheme for First-Order Logic},
author = {Yasmine Briefs and Martin Bromberger and Tobias Gehl and Lorenz Leutgeb and Simon Schwarz and Christoph Weidenbach},
journal= {arXiv preprint arXiv:2605.21335},
year = {2026}
}