TU Delft Algorithmics
SAT @ Delft
Delft University of Technology MiniMarch ALG Group
EWI ALG SAT @ DelftMiniMarch
eng
 
 
 
 
 
 
 
 
 
 
 
developers
Siert Wieringa

Supervisors:
Hans van Maaren
Marijn Heule

MiniMarch is a modified version of MiniSat v2.0 Beta ([2]). The design goal was to make a version of MiniSat that is less sensitive to shuffling of the input formula. MiniMarch extends MiniSat with the following techniques:
  • 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.
Clauses are sorted, the first sorting criterion is the shortest size first. Amongst clauses of the same length the clauses with the highest weight wclause are ordered first.

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, 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.

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 iv the index of the clause in which v occurs for the first time in the sorted set of clauses.

Special thanks to INOXA internet for supporting this project by making a brand new server available for the purpose of testing MiniMarch.
[1] R.H. Kibria, Actin solver description submitted to SAT Race 2006
[2] MiniSat v2.0 Beta, Niklas Eén, Niklas Sörensson