A Two-Watched Literal Scheme for First-Order Logic
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911702264578048 |
|---|---|
| author | Briefs, Yasmine Bromberger, Martin Gehl, Tobias Leutgeb, Lorenz Schwarz, Simon Weidenbach, Christoph |
| author_facet | Briefs, Yasmine Bromberger, Martin Gehl, Tobias Leutgeb, Lorenz Schwarz, Simon Weidenbach, Christoph |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_21335 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Two-Watched Literal Scheme for First-Order Logic Briefs, Yasmine Bromberger, Martin Gehl, Tobias Leutgeb, Lorenz Schwarz, Simon Weidenbach, Christoph Logic in Computer Science 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. |
| title | A Two-Watched Literal Scheme for First-Order Logic |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.21335 |