# 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