95 lines
4.7 KiB
Markdown
95 lines
4.7 KiB
Markdown
- 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)
|
|
``` |