Use a Rust SAT Solver to play better pickleball!
summary
Shows practical use of SAT/SMT tools: imports Rust SCIP crate (and mentions Z3) and models players as a two‑dimensional binary array plus a continuous deviation variable, then minimizes group skill variance. Produces balanced teams for 99 players into 33 groups with 31 groups identical and two slightly lower. Solves up to 108 players quickly, 111 takes over a day, 120 times out after a week. Code and data are available on GitHub and the model is optimization not pure SAT.
AI-written summary · about
chapters (13)
- 0:00SAT solvers and pickleball scheduling
- 1:16Peter Poole and Cook-Levin theorem
- 6:14Constraint satisfaction and SAT
- 8:23NP-complete and NP-hard
- 12:36Papers We Love meetup
- 18:13Practical SAT solvers
- 24:17Rust SCIP crate
- 32:04Real-world scheduling CSPs
- 35:58LeetCode with SAT solvers
- 41:16Pickleball tournament scheduling
- 45:28Rust pickleball solver
- 50:46Solver testing and results
- 54:17Q&A
related talks
37mSAT for Rustaceans
35mA Peek Inside SAT Solvers
34mSolving Problems Declaratively
15mSatune: Synthesizing Efficient SAT Encoders
28mScimitar: Functional Programs as Optimization Problems
18mScalable Floating-Point Satisfiability via Staged Optimization
22mSatisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
52mLearning Rust the wrong way.