Utilizing Structure in Combinatorial Solving and Reasoning
summary
Shows that decomposition-guided reductions give tight treewidth bounds for answer set programming: upper bounds encode provability along a tree decomposition with a k to k log k blow-up (log k bits per bag to order atoms), and matching ETH-based lower bounds via reductions from disjoint paths and QBF. Implements a hybrid solver nestHDB that uses #SAT as a sub-solver, handles treewidths ≈200, and empirically improves counting and projected counting performance.
AI-written summary · about
chapters (11)
- 0:00Introduction to treewidth
- 2:34FPT results and tree depth
- 5:02Decomposition-guided reduction
- 9:36ASP and graph representations
- 14:11Defining provability on trees
- 17:30Cyclic dependencies and bounds
- 20:16Lower bounds via disjoint paths
- 23:10Generalizing with QBF
- 27:27Reduction logic and examples
- 32:22Nested dynamic programming
- 35:38Conclusion and Q&A
related talks
01h 16mIn Search of the Hard Instances
48mBeyond SAT - Proofs for QBF, and more
27mRooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separatio...
24mA New Conjecture on Hardness of Low-Degree 2-CSP’s with...
59mThe Proof Complexity of Integer Programming
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
40mRelational Reasoning in Object-based Programs
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...