Logic, Optimization, and Constraint Programming: A Fruitful Collaboration
summary
Asserts concrete equivalences and tools: conflict clauses are Benders cuts — SAT/SMT conflict learning is derivable from inference duality — and resolution corresponds to Gomory/Fourier‑Motzkin projections used for cutting planes. Shows Boole’s probability logic maps to an LP solved by column generation, and binary decision diagrams are used as relaxed state graphs that tighten domains and replace LP bounds in search. Demonstrates edge‑finding from network flows to CP and that cutting planes increase LP‑consistency, reducing search.
AI-written summary · about
chapters (29)
- 0:00Introduction
- 1:35Constraint Programming
- 3:15Everyones Theorem
- 4:08Logic Programming
- 5:46Chip
- 6:58Satisfiability
- 7:32Propositional Logic
- 9:37Example
- 12:29Decision Diagrams
- 12:58How did this work
- 15:25Analysis applied to a constraint program
- 17:49What is a decision diagram
- 20:46Boolean logics
- 21:12Probability logic
- 25:43Nonstandard logic
- 27:53Linear optimization
- 28:53Network flow theory
- 29:32Network flow example
- 30:35Scheduling example
- 32:08Edge finding literature
- 32:43Duality
- 36:30Business Decomposition
- 42:19Resolution
- 43:18Cutting Plane Theorem
- 44:40Consistency
- 47:45LP Consistency
- 49:58Research Areas
- 50:42The Future
- 54:16Relaxed Decision Diagrams
related talks
49mAn Introduction to Constraint Programming
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
30mA Novel EGs-Based Framework for Systematic Propositional-Formula Simplification
47mLogic Programming à la Carte
01h 34mFormal Logic Undressed
01h 02mTheory and Control
29mSynthesizing Axiomatizations using Logic Learning
58mInvited Talk: Solvers, unite! A simple unified semantics for reasoning with assurance(…)