Replacing partial order with contiguity
Feasible since the length of the encoding is fixed!
- Eliminates the O(k3) clauses to specify the transitivity of partial order relation
- Fewer causal link variables needed
- A causal link can exist from step i to j only if j=i+q, qɬ
- Fewer clobbering possibilities, thus fewer threat resolution clauses
- 83.33% reduction in the number of clauses in the asymptotic case!