41 lines
2.0 KiB
Markdown
41 lines
2.0 KiB
Markdown
# What is SAT
|
|
- Satisfiability of a (CNF) formula
|
|
- Empty formula is SAT (Intersection of nothing)
|
|
- Empty Clause is UNSAT (union of nothing)
|
|
|
|
# Resolution
|
|
```
|
|
C u {l} D u {-l}
|
|
------------------------
|
|
C u D
|
|
```
|
|
## Special Case: Unit Resolution
|
|
```
|
|
C u {-l} {l}
|
|
------------------------
|
|
C
|
|
```
|
|
|
|
# Implication Graph
|
|
- Array/ Graph from literals/ variables to clauses/ reasons
|
|
- Maps a variable to the clause that lead to its assigning (only for [Unit Resolution](SAT_in_general#Special Case Unit Resolution))
|
|
- Logical end is the empty clause/ initial conflict clause $\kappa$
|
|
- (Normally hyprgraph with input nodes (reasons) and output node 'edge is the clause')
|
|
![[implication_graph.png]]
|
|
## (First) Unique Implication Point (UIP)
|
|
- A UIP is a node in the implication graphs lowest level which fully implies the conflict (together with all higher levels)
|
|
- The first UIP is typically what we want
|
|
- “pulls in” as few decision levels as possible
|
|
- Other strategies include last UIP, all UIP, where all decisions are used as a clause
|
|
- All UIP typically is a smaller clause but less useful
|
|
|
|
## Minimizing the learned clause
|
|
- Often the learned clause resulting from conflict analysis can be made smaller using self-subsumption
|
|
![[self_subsumption_learned_clause.png]]
|
|
- Here even h could then be removed, as e follows from Unit and d, i.e. we can construct a self subsumption only using an additional unit. But this is algorithmically more challenging)
|
|
## Shrinking
|
|
- Follow-up to [minimization](SAT_in_general#Minimizing the learned clause) (Sörensson & Biere, "Minimizing Learned Clauses")
|
|
- Minimization only reuses reasons already in the implication graph (self-subsumption)
|
|
- Shrinking instead assumes the negation of the (minimized) learned clause's literals and runs fresh unit propagation
|
|
- If a conflict is reached using only a subset of them, the rest were unnecessary -> drop them
|
|
- More expensive (does real propagation work), but can shrink clauses further than minimization alone |