• Clause sorting By sorting the clauses we not only hope to find conflict clauses imposing strong constraints faster but also facilitate resistance against the shuffling of clauses in the input formula.
• Symmetric simplifier The simplifying pre-processor introduced in MiniSat 2.0 is rather sensitive to the swapping of signs in the input formula. Our modifications make it symmetric.
• Branching heuristics MiniMarch combines dynamic lookahead branching heuristics for balanced variables with static occurrence based heuristics for unbalanced variables.
• Activity initialization The activities are initialized, to make the initial variable decisions taken less sensitive to variable index shuffling.

The simplifier in MiniSat 2.0 attempts to eliminate variables from the formula. In an attempt to eliminate variable v the solver does a merge on all pairs of clauses with literal v occurring in one and literal v in the other. The result of a merge is the clause that consists of all literals in both clauses minus v and v.

The simplifier used to call merge on the clauses from the list using the scheme described in algorithm 1.

To make the simplifier unaffected by shuffling we have modified this scheme. We require the subset of clauses in which v occurs to be sorted. The new scheme is now based on choosing pairs of clauses that are best in the ordering first.

MiniMarch combines dynamic lookahead branching heuristics for balanced variables with static occurrence based heuristics for unbalanced variables. The balance of a variable is defined as:

A variable is regarded as balanced if it's balance is smaller then the balance of the whole formula which is defined by:

For unbalanced variables (bal(v) > balance) the branching direction d(v) is determined as the direction of the literal with the lowest literal weight, w_literal. For balanced variables this same value d(v) is determined as a first estimate to the best branching direction. It might be undefined if w_literal(v) = w_literal(v).

Whenever the activity based branching heuristic used by MiniSat picks a balanced variable the lookahead procedure described in algorithm 3 is invoked.

The literal l that the lookahead procedure starts with is the opposite of the literal determined by d(v). This is because lookahead will have to propagate both literals and decide on the best. If the literal propagated second has the highest chance of being the best the chance of having to revert to the literal propagated first goes down. If d(v) has not yet been defined it will be defined as the literal with the highest number of clause watches or if that is equal the negation of the literal of v that occurred first in the sorted set of clauses.

The variables propQ₁ and propQ₂ return a measurement indicating the "quality of the propagation". They can be either a natural number or conflict. If no conflict was found the value is defined as:

Where IUP(v) is the set of all variables of which the value became fixed as a result of iterative unit propagation resulting of the propagation of v (including v itself). The value of m(r) is the sum of the distances the watch pointers moved to the next undefined variable in a clause that was watching r.

The MiniMarch solver uses activity initialization, a technique that was proposed before in [1]. The actual value of the initial activity in MiniMarch differs from the one proposed in that earlier work, we use:

With i_v the index of the clause in which v occurs for the first time in the sorted set of clauses.