- Preprocessing is very good at optimizing the CNF
- Its mostly polynomial (not too costly)
- But running it until completion can be too much
- Inprocessing runs preprocesors after each restart
- benefits of preprocessing, less overhead timewise
# Bounded Variable Elimination (BVE)
- Use resolution to remove a variable
- Works only if number of clauses is not increasing  (bounded)
- Best and most important preprocessing 

# Bounded Variable Addition (BVA)
- Conversely reverse the resolution rule to add a variable
- Only if you can decrease the number of variables
- $(a\lor d), (b\lor d), (c\lor d)$ and $(a\lor e), (b\lor e), (c\lor e)$  
- >> $(a\lor x), (b\lor x), (c\lor x)$ and $(\overline x \lor d), (\overline x \lor e)$ 

# Subsumption
- Smaller clause subsumes longer clause (backward subsumption)
- Longer clause is subsumed by smaller clause (forwards subsumption)

# Sweeping
- Find literals/nodes that are functionally equivalent (e.g. candidates via random simulation, confirmed with a SAT call)
- Merge equivalent literals: substitute one for the other everywhere, removing the redundant variable
- Preserves the exact model set (true logical equivalence), unlike Subsumption/BVE which only preserve (un)satisfiability
- Example: $(\overline x \lor y) \land (\overline y \lor x) \land (x \lor a) \land (\overline y \lor b)$
	- Simulation shows $x,y$ always agree; SAT call confirms $\overline{x \leftrightarrow y}$ is UNSAT $\Rightarrow x \leftrightarrow y$
	- Substitute $y := x$ everywhere: $(x \lor a) \land (\overline x \lor b)$ (the defining clauses for $y$ drop out)

# Variable instantiation
```
for l in lits:
	for c in clauses:
		assume l and -l' for all other l' in c
	if all c lead to conflict assign -l
```

# Pure Literal
- Find variables which only occur in one phase.
- Assign variable to that phase & remove all subsumed clauses

# Symmetry Breaking
- Find symmetries: permutations of variables/literals that leave the CNF invariant (e.g. via automorphisms of the clause-variable incidence graph)
- Add symmetry-breaking predicates (SBPs) that pick one canonical representative per symmetric orbit (e.g. lexicographic-leader constraints)
- Cuts away redundant, symmetric parts of the search space without losing satisfiability
- "Every model after works": a model of the constrained (canonical) formula is still a model of the original
- Example: $(x_1 \lor x_2) \land (\overline{x_1} \lor \overline{x_2})$ ("exactly one of $x_1,x_2$") is symmetric under swapping $x_1 \leftrightarrow x_2$
	- Two models exist: $x_1{=}1,x_2{=}0$ and $x_1{=}0,x_2{=}1$ (mirror images)
	- Add SBP $(\overline{x_1} \lor x_2)$ (forces $x_1 \le x_2$) to keep only the canonical $x_1{=}0,x_2{=}1$, cutting the mirrored branch from the search

# Stalmarks Method
- Method on triplets (such as results from the Tseitin transformation)
- Can transform (in)equalities
- BCP over (in)equalities, Structural Rules, Test Rule

# Autarky
- Partial assignments $\sigma$ maybe satisfes subset of a CNF 
- If all clauses touched by $\sigma$ are satisfied
	- $\sigma$ is an an autarky
	- These clauses may be removed
### Conditional autarky
- an coditinal autarky is an assignment $\alpha = \gamma \cup \beta$ 
- First F is simplified $F|_\gamma$ and then $\beta$ is an autarky of $F|_\gamma$
- Relation to (globally) blocked clauses 
	- Let $\gamma = \overline{C \setminus L}, \beta = L$  
	- We have $\gamma \cup \beta \text{ is autarky} \iff L \text{ globally blocked } C$
### Computing (conditional) autarkies
- Trivial base case: pure literals are already autarkies (touched clauses are all satisfied)
- Fixpoint search: tentatively assign a literal, satisfy the clauses it touches, then keep adding literals whose touched clauses are already satisfied, until no touched clause is falsified (else backtrack the guess)
- For conditional autarkies: fix $\gamma$ first (simplify $F|_\gamma$), then run the same fixpoint search for $\beta$ on $F|_\gamma$
# Blocked Clauses
- If we have a blocked clause $C$ containing a literal $l$ 
- and all resolvents of $C$ are tautological (trivially true) we can remove C
- (Trivial proof by contradiction)
## Set Blocked Clauses
- Extension to generalize the blocked literal to a Set $L$
	- Similar idea Set blocked Clause $C$, and all Clauses $D$ which contain a $l \in \overline L$ 
$$
	(C \setminus L) \cup \overline L \cup D\; \text{tautological}
$$ 
# Vivification / Distillation
- Try to set literals in clauses to false and find out which other literals are implied
- Maybe even the clause is implied
```
for c in clauses:
	for i in len (c):
		lit = c[i]
		assign (-lit)
		propagate ()
		if eval(c) == True:
			// Implies itself somehow
			mark_clause_for_removal (c)
		for other in c[i+1..]:
			if is_assigned (other):
				mark_lit_for_removal (other)
```