- Most important heuristic, as it can steer the entire solver
## Types
- Static heuristics (pre-computed once)
	- Ex.: Natural Order
- Dynamic heuristics 
	- Ex.: Dynamic Largest Individual Sum (DLIS) (chose most common variable + phase)
	- Expensive, needs (full) scanning of (all) clauses
- Second order dynamic heuristics 
	- Ex.: VSIDS, ESIDS
	- Less expensive, good measurement 

# Look-ahead
- Instead of scanning static clause counts (DLIS) or scores (VSIDS), actually try each candidate variable
- For a candidate $x$: tentatively assign $x$ and separately $\overline x$, run full [propagation (BCP)](Solvers#Boolean Constraint Propagation (BCP)) for each, and measure the effect (# clauses reduced/simplified, # new units)
	- If one polarity's propagation conflicts -> failed literal -> the other polarity is forced (same primitive as [Variable instantiation](Preprocessing_Inprocessing#Variable instantiation)/[Vivification](Preprocessing_Inprocessing#Vivification / Distillation))
- Pick the variable (and often the polarity) that maximizes the combined look-ahead effect of both branches (e.g. product/sum of the two reduction counts, as in march/kcnfs)
- Very informative but expensive (full propagation per candidate, both polarities) -> basis of dedicated look-ahead solvers, rather than per-decision use inside CDCL

# Cut heuristic
- Find a variables that 'cuts' the CNF into parts without overlapping variables
- Solve parts separately (for all assignments of the cut)
- Divide & Conquer approach

# Horn Form
## Definition
- A clause is positive if it contains at least 1 positive literal, otherwise it's negative
- A Horn clause is a clause with at most one positive literal
- A CNF is in Horn Form if all clauses are Horn clauses
## Facts 
- If all clauses in a Horn Form CNF are positive there is a minimal satisfying assignment
	- This assignment can be found using BCP
- The minimal satisfying assignment of the positive part of a Horn Form CNF IFF it is SAT
	- I.e. if not it is UNSAT
## Usefulness/ Heuristic
- DP can transform a non Horn from CNF into one by **choosing variables** from clauses  with more than one positive literal (non horn clauses) and doing resolution on them. 
- [BCP](SAT_in_general#Special Case Unit Resolution) runs through a HORN CNF in polynomial time



# Variable State Independent Decaying Sum (VSIDS)
- Count occurrence of variables in conflict clauses
- Priority Queue is updated, and VSIDS is taken from it
- Decay/ re-score values after i conflicts (Chaff: $f = 1/2, i = 256$)
	- multiply all by some $f < 1$  
	- Emphasizes literals contributing to recent conflicts

#### Additional idea:
- Use VSIDS only as secondary heuristic, primarily try to satisfy must recently added clauses 
## Normalized VSIDS (NVSIDS)
- Keep the score between $[0, 1]$
- Pick $f = 0.95$ and calculate score like this:
	`new_score = old_score * f + in_conflict? (1 - f) : 0`
- You can defer the re-scoring to later, i.e. only update variables in conflict and then re-score all later on to save time
- Can also Bump resolved literals on conflict level, not just learned lits (good for heuristic?!)
## Exponential VSIDS (EVSIDS)
- Bump by exponential value $g^i = \frac{1}{f}^i$ 
	- `new_score = old_score + (1/f)^i`
- EVSIDS is just NVSIDS but without scaling 
$$\frac{f^{-n}}{1-f} \cdot \text{NVSIDS}$$
# Decision heuristic Summary table
- Old score: s
- decay $0 < f < 1$

| STRATEGY | Bumped              | not-bumped  |                                        |
| -------- | ------------------- | ----------- | -------------------------------------- |
| STATIC   | $s$                 | $s$         |                                        |
| INC      | $s + 1$             | $s$         |                                        |
| SUM      | $s + i$             | $s$         |                                        |
| VSIDS    | $s / 2 + 1$         | $s / 2$     | Only half every so often (every 256)   |
| NVSIDS   | $f \cdot s + (1-f)$ | $f \cdot s$ |                                        |
| EVSIDS   | $s + f^{-i}$        | $s$         |                                        |
| AVG      | $(s+i)/2$           | $s$         | average conflict-index decision scheme |
| VMTF     | $i$                 | $s$         | Variable Move to Front                 |
- Turns out AVG (moving average) and EVSIDS are very good
## Variable Move to Front
- Cheap to implement, aggressive