# Encoding
- Formula -> [CNF](Encoding#CNF (Conjunctive Normal Form)) / [DNF](Encoding#DNF (Disjunctive Normal Form))
	- Circuit vs Formula
- [Tseitin](Encoding#Tseitin Transformation)
	- Complexities
	- Benefits
- [Proofs](Proofs)
# Solving
- [CNF](Encoding#CNF (Conjunctive Normal Form))
	- [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](SAT_in_general#Resolution)
	- [DPLL](Solvers#Davis Putnam Logemann Loveland DPLL)
	- Complexities in Space & Time
# [CDCL](Solvers#CDCL)
- [Propagation "BCP"](Solvers#Boolean Constraint Propagation (BCP))
	- [Watch list](<Implementation Details#(Two) Watch scheme>)
	- [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](SAT_in_general#Shrinking)
- Complexities of CDCL
	- What is the cost of missing propagations?
- [Restarts](Solvers#Restarts) (schemes: [Scheduling](Scheduling))
- [Forgetting clauses](Solvers#Reduction)
- [Decision Heuristics](<Decision Heuristics>)
- [Phase (Saving)](Solvers#Phase saving)
# [Inprocessing](Preprocessing_Inprocessing)
- [Scheduling](Scheduling)
## "Same models"
- [Subsumption](Preprocessing_Inprocessing#Subsumption)
- [Sweeping](Preprocessing_Inprocessing#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](Encoding#Plaisted–Greenbaum (PG))
- [Autarkies](Preprocessing_Inprocessing#Autarky)


# Local Search?
- Not specified by Fleury, but lecture was held by Fleury
	- weird

# Im weak on 
- [Glucose](Solvers#Reduction)
- [Look ahead](<Decision Heuristics#Look-ahead>)