59 lines
2.7 KiB
Markdown
59 lines
2.7 KiB
Markdown
# 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>)
|