A board game night with geeks
summary
Encodes Quarto as Boolean satisfiability using F#, rewrites rules into CNF and DIMACS, and feeds that to a SAT solver (runs on MiniSat) to produce an explicit board assignment proving a tie exists. The conversion, a small library and a parser are on GitHub; the solver returns a concrete counterexample in seconds versus ~90 hours brute force. Performance relies on unit resolution, watched literals and SAT heuristics, though CNF expansion can grow and simplifications help.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 0:42Cuarto
- 1:55Is this a possibility
- 2:34Route forces
- 4:01Automated reasoning
- 4:30Problem transformation
- 4:57Binary world
- 6:16Boolean logic
- 7:48Satisfy abilities
- 9:24The idea
- 10:17Defining variables
- 10:48All stones should be different
- 12:01For loop
- 13:37Unit Resolution
- 15:24Unit Resolution Example
- 36:43Science
- 37:45Properties
- 39:13Comments
related talks
34mLet’s Use An Automated Theorem Prover To Verify Video Games; I Swear This Is More Fun Than It Sounds
21mValidating SMT Solvers for Correctness and Performance via Grammar-based Enumeration
18mSMT2Test: From SMT Formulas to Effective Test Cases
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
26mCorralling the CNFs
34mSymbolic Execution for Randomized Programs
32mExplaining SAT Solving Using Causal Reasoning
14mSynthesizing Contracts Correct Modulo a Test Generator