7 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…
Lean on Vampire Proofs (Short Paper)
Jonas Bodingbauer, Márton Hajdu, Laura Kovács +2
Vampire proves theorems completely automatically in first- and higher-order logic extended with theories. Proof checking is increasingly demanded to consolidate user trust in Vampi…
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…
Synthesis Benchmarks for Automated Reasoning
Márton Hajdu, Petra Hozzová, Laura Kovács +3
Program synthesis is the task of constructing a program conforming to a given specification. We focus on deductive synthesis, and in particular on synthesis problems with specifica…
Positive Almost-Sure Termination of Polynomial Random Walks
Lorenz Winkler, Laura Kovács
The number of steps until termination of a probabilistic program is a random variable. Probabilistic program termination therefore requires qualitative analysis via almost-sure ter…
Partial Redundancy in Saturation
Márton Hajdu, Laura Kovács, Andrei Voronkov
Redundancy elimination is one of the crucial ingredients of efficient saturation-based proof search. We improve redundancy elimination by introducing a new notion of redundancy, ba…