march_eq

## developersMarijn HeuleHans van Maaren |
## overviewintroductionpre-processing partial lookahead additional features |

download now! |

- extensive equivalence reasoning within the pre-processor: Equivalence clauses are extracted and a minimum solution for this equivalence part of the formula is computed.
- optimised lookahead: Using special data-structures to reduce the number of cache misses, implication trees to reduce the number of unit propagations and a time-stamp structure to prevent backtracking costs, makes the lookahead phase is even ``fast'' on formulas with many clauses.
- combined lookahead evaluation: The heuristics in marcheq to evaluate the lookahead are fully optimised towards effectively solving benchmarks containing a considerable number of equivalence clauses.

- simplifying: Iterative propagation of all unary clauses and binary equivalences.
- equivalence reasoning: First all so called equivalence clauses
*l*1*l*2 ...*l*n (where the*l*i are literals, or their negations) are extracted from the CNF and placed in a separate data-structure called Conjunction of Equivalences (CoE). Second, the found CoE is solved using a polynomial algorithm. Unary clauses or binary equivalences found in the solution are iteratively propagated. If no conflict has occurred, a procedure is called to compute a solution of the CoE which total length of non-tautological equivalence clauses is minimal. Notice that at this point, march_eq takes another strategy than march. - two phase 3-Sat translator: In the first phase every pair of literals that occurs multiple times in clauses, is replaced by a single dummy variable and three clauses are added for each pair to make the dummy logically equivalent to the disjunction of the two literals involved. The second phase consists of a straight forward 3-Sat translation.
- addition of resolvents: Several resolvents of length two and three are added during this stage.
- full root lookahead: Although partial lookahead appears useful in the lower nodes of the DPLL search tree, performing a full lookahead in the root node practically always results in a speed-up.

The combined lookahead evaluation function (Diff in short) used
in march_eq combines the evaluation of the reduction of CNF-clauses and the
evaluation of the reduction of equivalence clauses. The reduction of the
CNF-clauses is measured by counting the newly created binary clauses in the
resulted formula after lookahead on a variable. The reduction of the CoE is
measured by summing up - in a weighted fashion - all reduced equivalence
clauses. A reduced equivalence clause of new length *n* is weighted using
*eqn* (equation (1)). The Diff is obtained by adding both
evaluations. The final branch decision is based on equation H, which is
calculated as in line 12 of Algorithm 1. In a node, variable *x* with the
highest H( *x* ) is selected as branch variable for its two child nodes.

(1) |

The partial behaviour of the lookahead is realised by only performing
lookahead on variables in set : At the beginning of each node, this
set is filled by pre-selection heuristics that are based on an approximation
function of the combined evaluation of the lookahead (Ace). The ranking of
variable *x* is calculated by multiplying Ace(*x*) and
Ace(*x*). The higher the ranking, the "better" the variable.
(*x*), used
to obtain Ace(*x*), refers to the set of all equivalence clauses (denoted
as ) in which *x* occurs, and
*occ*3( *x* ) refers to the number of
occurrences of literal *x* in ternary clauses.

(2) |

Because the computational costs of calculating the above pre-selection heuristics are relatively high, two variants of march_eq are submitted to the Sat 2004 competition: The first, march_eq_010 performs only lookahead on the "best" 10% of the variables, while the second, march_eq_100 performs a full lookahead which is expensive, but at least makes it possible to eliminate the pre-selection heuristics.

- Prohibit equivalent variables from both occurring in : Equivalent variables will have the same Diff, so only one of them is required in .
- Timestamps: A timestamp structure in the lookahead phase makes it possible to perform PartialLookahead without backtracking.
- Cache optimisations: Two alternative data-structures are used for storing the binary and ternary clauses. Both are designed to decrease the number of cache misses in the PartialLookahead procedure.
- Tree-based lookahead: Before the actual lookahead operations are performed, various implication trees are built of the binary clauses of which both literals occur in . These implications trees are used to decrease the number of unit propagations.
- Necessary assignments: If both
*x**y*and*x**y*are detected during the lookahead on*x*and*x*,*y*is assigned to true because it is a necessary assignment. - Binary equivalences: If both
*x**y*and*x**y*are detected during the lookahead on*x*and*x*, binary equivalence*x**y*is propagated in the CoE data-structure to reduce the length of some equivalence clauses. - Resolvents: Several binary resolvents are added during the solving phase. Those resolvents that are added have the property that they are easily detected during the lookahead phase and that they could increase the number of detected failed literals.
- Restructuring: Before calling procedure PartialLookahead, all satisfied ternary clauses of the prior node are removed from the active data-structure to speed-up the lookahead.