1.3 KiB
1.3 KiB
SAT Solving Exam Prep
Notes for the SAT Solving oral exam (Fleury). Start with the summary, then drill into
individual topic files as needed; questions.md collects oral-exam-style questions
linking back into all of them.
Start here
- Fleury Summary of stuff.md — topic checklist for the exam, links out to every other file
- questions.md — oral-exam-style questions, organized by topic, linked back to the notes
Topic notes
- Encoding.md — CNF/DNF, NNF, Tseitin & Plaisted-Greenbaum transformations
- SAT_in_general.md — SAT/UNSAT, resolution, implication graph, UIP, clause minimization/shrinking
- Solvers.md — DP, DPLL, backjumping, CDCL, clause reduction, restarts, phase saving
- Implementation Details.md — watched literals, occurrence lists, trail, finding a UIP
- Decision Heuristics.md — VSIDS family, look-ahead, cut heuristic, Horn form
- Preprocessing_Inprocessing.md — BVE/BVA, subsumption, sweeping, symmetry breaking, autarkies, blocked clauses
- Scheduling.md — arithmetic/geometric/Luby restart schedules
- Proofs.md — RUP, RAT, redundancy