Explaining SAT Solving Using Causal Reasoning
summary
CausalSAT runs solvers on UNSAT benchmarks, logs clause features and uses DRAT-trim to count clause utility (uses in the proof over the next 10,000 conflicts), learns a causal graph with structure learning, then answers causal queries. Results: ATE for LBD 1→2 = -0.26 so low‑LBD clauses have higher utility; CATE shows high‑LBD clauses drop rapidly while low‑LBD do not; small clauses win even when LBD is fixed; propagation has greatest impact and Maple/Luby effects are quantified.
AI-written summary · about
chapters (9)
- 0:00Intro
- 1:17Do we really understand?
- 3:59Causality in SAT Solver
- 5:20Approach Overview
- 6:53Data Generation
- 9:23Structure Learning
- 10:43Query Formulation
- 19:09Query Answering
- 22:17Future Work
related talks
10mSATisfying answers to difficult questions!
44mAutomated Scientific Discovery Using Insights from Problem Structure
20mFunction synthesis for maximizing model counting
52mLearning as a Tool for Algorithm Design and Beyond-Worst-Case Analysis
01h 01mThe Mathematics of Causal Inference, with Reflections on Machine Learning and the Logic of Science
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
33mLearning Abstract Causal Structure From Causal Interventions In Children And Artificial Agents
29m🧠🧹 Causality - Mental Hygiene for Data Science