SAT-SOLVING-EXAMPREP/Preprocessing_Inprocessing.md

• 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)