ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
summary
ADCL presents a calculus that learns n-parameterized accelerated clauses (transitive closures of recursive CHCs) and implements it in the tool LoAT, using four rules: step, accelerate, backtrack, block. It proves unsatisfiability (not yet satisfiability) by replacing long unfoldings with single learned clauses, turning proofs that would need hundreds of millions of resolution steps into tiny proofs; empirical comparison shows LoAT competitive with Z3 BMC and Spacer and solves benchmarks other tools cannot.
AI-written summary · about
chapters (10)
- 0:00ADCL and CHCs
- 2:27Acceleration in CHC analysis
- 4:34Acceleration benefits example
- 7:01Traditional vs accelerated proofs
- 8:25ADCL calculus formalization
- 12:17ADCL proof construction
- 16:11ADCL unsatisfiability proofs
- 17:58Experimental results and tools
- 20:05ADCL limitations and future
- 21:29Q&A
related talks
38mConstrained Horn Clauses Satisfiability via Catamorphic Abstractions
18mAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
01h 02mTheory and Control
30mSemantics-Guided Synthesis
23mHigher-Order MSL Horn Constraints
21mBoosting Constrained Horn Solving by Unsat Core Learning
01h 05mThe Power of Extended Resolution: A Practitioner's Perspective