Automated Scientific Discovery Using Insights from Problem Structure
summary
Shows how a plain SAT solver plus unit propagation and clause learning finds a machine proof of the Erdős discrepancy case (the 1161 bound and a 1160 witness) and produces a checkable 13 GB proof trace, and how adding streamliners—extra constraints discovered incrementally from small instances—reveals regular patterns that lead to a constructive algorithm for spatially balanced Latin squares (structure appears around size 14 and enables orders far larger than brute force like 35×35).
AI-written summary · about
chapters (8)
- 0:00Start
- 4:58Discoveries in Discrete Math
- 19:18The Spatially-balanced Latin square (SBLS) problem
- 25:59Outline --- Discovering Problem Structure
- 26:11Proposed Framework: Overview of Streamlined Combinatorial Search
- 29:24Overview of Streamlined Search
- 30:55Proposed Framework: Formal Description and Overview
- 42:32Summary, cont.
related talks
10mSATisfying answers to difficult questions!
30mUnfamiliar Terrain
40mAdvances in Deep Learning for Mathematical Theorem Proving
32mExplaining SAT Solving Using Causal Reasoning
34mSolving Problems Declaratively
16mJust-in-Time Learning for Bottom-Up Enumerative Synthesis
52mKeynote: Tools for Verified Scala
47mBig Ideas in Program Synthesis