SAT-SOLVING-EXAMPREP/Fleury Summary of stuff.md

Encoding

• Formula -> CNF / DNF
  • Circuit vs Formula
• [Tseitin](Encoding#Tseitin Transformation)
  • Complexities
  • Benefits
• Proofs

Solving

• CNF
  • [What is SAT / UNSAT](SAT_in_general#What is SAT)
  • Explain meaning for a encoded Circuit ([Encoding Problems to boolean formula](Encoding#Encoding Problems to boolean formula))
• Techniques
  • [DP](Solvers#Davis Putnam Procedure (DP))
  • Resolution
  • [DPLL](Solvers#Davis Putnam Logemann Loveland DPLL)
  • Complexities in Space & Time

CDCL

• [Propagation "BCP"](Solvers#Boolean Constraint Propagation (BCP))
  • Watch list
  • [Blocking lit](Implementation Details#Blocking Literal)
  • Example question: Confluence of conflicts
    • Answer: Confluent on conflict, not which specific one though
• Conflict analysis
• [Implication Graph](SAT_in_general#Implication Graph)
• [1-UIP, ALL UIP](SAT_in_general#(First) Unique Implication Point (UIP))
  • Example question: what is smaller? benefits? (see [(First) Unique Implication Point (UIP)](SAT_in_general#(First) Unique Implication Point (UIP)))
• [minimization](SAT_in_general#Minimizing the learned clause)
• shrinking
• Complexities of CDCL
  • What is the cost of missing propagations?
• Restarts (schemes: Scheduling)
• Forgetting clauses
• Decision Heuristics
• [Phase (Saving)](Solvers#Phase saving)

Inprocessing

• Scheduling

"Same models"

• Subsumption
• Sweeping
• [Vivification](Preprocessing_Inprocessing#Vivification / Distillation)

"Every Model after Works" M_1 \rightarrow M_2

• [Symmetry breaking](Preprocessing_Inprocessing#Symmetry Breaking)
• [Pure literals](Preprocessing_Inprocessing#Pure Literal)
• BCA (see [Blocked Clauses / Blocked literal](Preprocessing_Inprocessing#Blocked Clauses / Blocked literal))

"Change Models"

• [bounded Variable Elimination](Preprocessing_Inprocessing#Bounded Variable Elimination (BVE))
• Blocked Clause Elimination (see [Blocked Clauses / Blocked literal](Preprocessing_Inprocessing#Blocked Clauses / Blocked literal))
• Plaisted-Greenbaum
• Autarkies

Local Search?

• Not specified by Fleury, but lecture was held by Fleury
  • weird

Im weak on

• Glucose
• Look ahead