SAT-SOLVING-EXAMPREP/questions.md

Encoding

• What is CNF, what is DNF, and why is finding a satisfying assignment easy in DNF but hard in CNF (and vice versa for falsifying assignments)? CNF / DNF
• How would you encode "are two programs equivalent?" as a SAT instance, and what does a SAT result tell you? [Encoding Problems to boolean formula](Encoding#Encoding Problems to boolean formula)
• What is NNF? Why does the naive NNF -> CNF transformation (OR-distribution) blow up exponentially? [NNF](Encoding#NNF / Negation Normal Form)
• Walk through the Tseitin transformation on a small formula. Why does the resulting CNF only grow linearly, and why is splitting into binary operations sometimes not optimal (e.g. XOR)? [Tseitin](Encoding#Tseitin Transformation)
• What does Plaisted-Greenbaum change compared to plain Tseitin? Give a concrete positive-polarity and negative-polarity example and state which single implication direction suffices in each case. PG
• When does a subformula need the full biconditional even under PG?
• Translating a formula into NNF can itself blow up exponentially even before any CNF step — why does f \leftrightarrow g \mapsto (f\land g)\lor(\overline f\land \overline g) double the size, why does this compound when IFF/XOR are nested, and how does Tseitin sidestep it? [Negation Normal Form](lect02#Negation Normal Form)

Complexity

• SAT is in NP, UNSAT is in coNP — concretely, what's the certificate in each case, and who has an easy time (finder vs. checker)? Is NP = coNP? [P, NP and CO-NP](lect02#P, NP and CO-NP)
• In what sense is SAT the "NP king"? What does it actually buy you that every NP problem reduces to SAT? [P, NP and CO-NP](lect02#P, NP and CO-NP)

SAT Fundamentals

• Define SAT/UNSAT. Why is the empty formula SAT and the empty clause UNSAT? [What is SAT](SAT_in_general#What is SAT)
• State the resolution rule and derive unit resolution as its special case. Resolution
• Describe the Davis-Putnam procedure. Which operations preserve SAT, which preserve UNSAT, and why? [DP](Solvers#Davis Putnam Procedure (DP))
• How does DPLL differ from DP? Why is DPLL correct (Shannon expansion)? [DPLL](Solvers#Davis Putnam Logemann Loveland DPLL)
• (past oral exam question) Why does DP terminate? [Oral Exam](lect05#Oral Exam)
• (past oral exam question) Why doesn't DP's termination show that SAT is solvable in polynomial time — how many resolvents can eliminating one variable add, and how does that compound over all variables? [Oral Exam](lect05#Oral Exam)
• What is Horn form? Why can a satisfiability check on a positive Horn-form CNF be done in polynomial time via BCP alone? Horn Form

CDCL Core

• What does CDCL add on top of plain DPLL? CDCL
• What is backjumping, and how/why can it reduce the search space from exponential to quadratic in the number of "bad" decisions? Backjumping
• What is the implication graph and what does a (first) UIP represent in it? [Implication Graph](SAT_in_general#Implication Graph) / [UIP](SAT_in_general#(First) Unique Implication Point (UIP))
• Compare 1-UIP vs. all-UIP learning: which clause is typically smaller, and why is 1-UIP still usually preferred?
• Sketch the algorithm for finding the first UIP by walking the trail backwards. Finding an UIP
• What is self-subsumption-based minimization of a learned clause? [Minimizing](SAT_in_general#Minimizing the learned clause)
• How does shrinking differ from minimization — why can it remove literals that minimization cannot, and at what cost? Shrinking
• In what sense is conflict analysis confluent, and in what sense is it not?
• CDCL can undo assignments via backjumping and restarts — so why does it still terminate? What quantity only ever grows across conflicts? Termination
• After learning a conflict clause, to which decision level do you backjump, and in what sense is the learned clause a "shortcut" for the conflict you just derived through several decisions? Backjumping
• A UIP can be defined graph-theoretically as a dominator of the conflict node in the implication graph — what does that mean, and what would a dominator on a higher (non-last) decision level correspond to? Lecture 07
• What is a cut in the implication/conflict graph? How does it split the graph into a "reason side" and "conflict side", and how does the learned clause relate to the literals crossing the cut? [Cut in Conflict graphs](tutorial#Cut in Conflict graphs)

BCP / Implementation

• Compare the occurrence list, the head/tail scheme, and the two-watched-literal scheme: what does each need to update on assignment vs. on backtracking? Occurrence Stack / Head & Tail / Two Watch
• Why don't the two watched literals need any bookkeeping on backtrack, unlike a full occurrence/counting scheme?
• What is a blocking literal, and why is it needed given the watch invariant already guarantees the watched literals aren't false? Blocking Literal
• What's the special-case trick for binary clauses in the watch scheme, and why does it work only there? Trick for binary clauses
• Why is the trail useful for both propagation bookkeeping and UIP search? Control and Trail
• How do decision level, control stack, and trail relate operationally — what exactly does the control stack let you "undo", and what does the trail hold that the control stack doesn't? [Easy Sat Unit Prop Example](lect04#Easy Sat Unit Prop Example)

Restarts & Clause Management

• Why can restarts improve performance even though they discard the trail? What state survives a restart, and why is that specifically kept? Restarts
• Give the reset formulas for arithmetic, geometric, and Luby restart schedules. What tradeoff is each trying to balance? Scheduling
• Why does the Luby sequence look like 1,1,2,1,1,2,4,1,1,2,4,8,...?
• Name several heuristics for deciding which learned clauses to forget, and explain what LBD measures and why a low-LBD ("glue") clause is considered valuable. Reduction
• What does Glucose's restart trigger compare, and why does that indicate the solver is "stuck"?

Decision Heuristics

• Contrast static, dynamic, and second-order dynamic decision heuristics. Where does DLIS sit vs. VSIDS, and why? Types
• Walk through VSIDS scoring and periodic decay. How do NVSIDS and EVSIDS reformulate the same idea, and why is EVSIDS just unscaled NVSIDS? VSIDS
• What is phase saving, and why does re-using the saved phase after a restart help rather than hurt exploration? [Phase saving](Solvers#Phase saving)
• Explain look-ahead based variable selection. Why is it too expensive to run on every CDCL decision, and where else in your notes does the same "assign, propagate, check for conflict" primitive show up? Look-ahead
• What is the cut heuristic, and how is it a divide & conquer approach to solving? Cut heuristic

Preprocessing / Inprocessing

• What's the difference between preprocessing and inprocessing, and why run simplification again after every restart instead of once up front?
• Explain Bounded Variable Elimination — why must the clause count not increase for it to apply? [BVE](Preprocessing_Inprocessing#Bounded Variable Elimination (BVE))
• Explain Bounded Variable Addition as BVE's reverse, with an example. When is it worth applying? [BVA](Preprocessing_Inprocessing#Bounded Variable Addition (BVA))
• Distinguish forward and backward subsumption. Subsumption
• What does sweeping do, and why does it preserve the exact model set where subsumption/BVE only preserve (un)satisfiability? Sweeping
• What is variable instantiation (failed-literal probing), and how does vivification generalize the same "assign, propagate, check" idea to whole clauses instead of single literals? [Variable instantiation](Preprocessing_Inprocessing#Variable instantiation) / [Vivification](Preprocessing_Inprocessing#Vivification / Distillation)
• What is a pure literal, and why is fixing it always safe? [Pure Literal](Preprocessing_Inprocessing#Pure Literal)
• What is symmetry breaking? Give a symmetry-breaking predicate for the "exactly one of $x_1,x_2$" constraint and explain what it removes. [Symmetry Breaking](Preprocessing_Inprocessing#Symmetry Breaking)
• Define autarky. What is a conditional autarky, and how does it relate to globally blocked clauses? Autarky
• Sketch how you'd compute a (conditional) autarky via fixpoint search. [Computing autarkies](Preprocessing_Inprocessing#Computing (conditional) autarkies)
• What is a blocked clause, and why is it always safe to remove one (proof idea via resolvent tautology)? [Blocked Clauses](Preprocessing_Inprocessing#Blocked Clauses)
• How does the set-blocked-clause generalization extend the single blocked-literal condition? Set Blocked Clauses
• What does Stalmark's method operate on, and how does that differ from Tseitin/CNF-based reasoning? [Stalmarks Method](Preprocessing_Inprocessing#Stalmarks Method)
• Sort BVE, BCE, Subsumption, Sweeping, Pure literals, and Symmetry breaking into "same models" / "every model after works" / "changes models" — justify each placement.

Proofs

• Why do UNSAT results need proofs, and what's the basic idea (deriving the empty clause)? Proofs
• What is RUP, and why is checking an RUP proof cheap? RUP
• What is RAT, and in what sense is it strictly more general than RUP? RAT
• How does RAT let you represent blocked-clause removal in a proof? RAT
• What does it mean for a clause to be (semantically) redundant, and how does Propagation Redundancy (PR) generalize RAT? Redundancy

Big Picture

• Trace one SAT instance end to end: how might you encode it (Tseitin/PG), which inprocessing techniques could simplify it, how would CDCL solve it, and what would an UNSAT proof for it look like?
• Compare the three "Watch scheme" implementations for the same underlying goal — what does each optimize for (memory, cache locality, backtrack cost)?
• Both look-ahead decision making and failed-literal probing (variable instantiation) share a mechanism — what is it, and why is one used as a decision heuristic and the other as preprocessing?