3 citations · 7 across the 6 of their papers we have counts for
6 papers
Generalizing CDCL with Graph Backtracking
Robin Coutelier, Thomas Hader, Laura Kovács
We present graph backtracking, a novel, fine-grained backtracking scheme for CDCL-based SAT solving, parametrized by a user-defined weight function. For conflict repair, we challen…
The Vampire Diary
Filip Bártek, Ahmed Bhayat, Robin Coutelier +10
During the past decade of continuous development, the theorem prover Vampire has become an automated solver for the combined theories of commonly-used data structures. Vampire now…
Term Ordering Diagrams
Márton Hajdu, Robin Coutelier, Laura Kovács +1
The superposition calculus for reasoning in first-order logic with equality relies on simplification orderings on terms. Modern saturation provers use the Knuth-Bendix order (KBO)…
Lazy Reimplication in Chronological Backtracking
Robin Coutelier, Mathias Fleury, Laura Kovács
Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is…
SAT Solving for Variants of First-Order Subsumption
Robin Coutelier, Jakob Rath, Michael Rawson +2
Automated reasoners, such as SAT/SMT solvers and first-order provers, are becoming the backbones of rigorous systems engineering, being used for example in applications of system v…
SAT-Based Subsumption Resolution
Robin Coutelier, Laura Kovács, Michael Rawson +1
Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new SAT-based reasoning technique for sub…