SPIDER: A Basic CSP Solver

This document provides a short description of a MAC-based solver written by the author for the Third International CSP Solver Competition (2008). 1 Features SPIDER ("SPider Is a Dull solvER") is a complete CSP solver written in C for solving problems with binary and non-binary extensional constraints, using standard binary-branching MAC (2-4). The solver is based on the CSP solver code from CPlan (1). It uses the revision-queue structure for propagating the effect of AC (5). The solver that ran in the competition has the following features. - variable ordering. The heuristic dom/wdeg (6) was used. - binary branching. After the second branch, the effect of the refutation is propagated. That is, when value a of variable X is tried and the search failed, a is removed from the domain of X and arc consistency is re-enforced. Interestingly, a binary-branching MAC with no propagation after the refu- tation branch can be just as good as the binary-branching MAC with propa- gation. It was found that for some benchmark instances, one version can be several times better than the other while the performance reverses on some other benchmarks. It was shown in (2,3) that binary-branching is strictly more powerful than d- way branching (d is the domain size). However, propagation is not essential to the proof: with or without propagation, binary-branching is still more powerful than d-way branching. More studies need to be done to see under what conditions is the propagation more effective. - value ordering. Values are statically ordered. Each value has an associated integer weight. The value with the largest weight will be picked first for instantiation. Before the search starts, the solver goes through each tuple in each extensional constraint and increases a value's weight by 1 if that value appears in the tuple and the constraint is of type "support", or decreases the weight by 1 if the constraint is of type "conflict".