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, wliteral. For balanced variables this same value d(v) is determined as a first estimate to the best branching direction. It might be undefined if wliteral(v) = wliteral(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 propQ1 and propQ2 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.