Boosting Constrained Horn Solving by Unsat Core Learning
summary
Built a relational hyper‑graph neural network called R-HyGNN and a framework MUSHyperNet that predicts Minimal Unsatisfiable Subsets (MUSes) of Constrained Horn Clauses and reuses those predictions across verification runs, integrates with CEGAR and SymEx solvers via three prioritization strategies (score‑only, numeric combination, alternating queues), trains on CHC-COMP benchmarks, and yields concrete gains: 6.1% more problems solved and 13.3% faster average solving time while extracting MUS labels from solved UNSAT instances.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:24Constraint Horn clauses background
- 1:28Program verification example
- 3:13Minimal unsatisfiable subsets
- 3:35Framework and deep learning
- 6:05Training data from unsat cores
- 7:11Graph representation of clauses
- 9:44Graph neural network
- 10:52Predicted scores to guide solvers
- 11:56Scores with solver strategies
- 12:17Benchmark handling
- 13:41Experimental results
- 14:49Key takeaways
- 16:34Future directions
- 17:20Q&A
related talks
30mSemantics-Guided Synthesis
23mHigher-Order MSL Horn Constraints
38mConstrained Horn Clauses Satisfiability via Catamorphic Abstractions
18mAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
35mA Peek Inside SAT Solvers
21mScaling Abstraction Refinement for Program Analyses in Datalog Using Graph Neural(…)
10mSATisfying answers to difficult questions!
52mLearning as a Tool for Algorithm Design and Beyond-Worst-Case Analysis