... \title¹

We thank people who provided code, help, and discussion: Greg Badros, Alan Borning, Corin Anderson, Mike Ernst, Zack Ives, Subbarao Kambhampati, Henry Kautz, Jana Koehler, Tessa Lau, Denise Pinnel, Rachel Pottinger, Bart Selman, and the blind reviewers. This research was funded in part by Office of Naval Research Grant N00014-98-1-0147, by the ARCS foundation Barbara and Tom Cable fellowship, by National Science Foundation Grants IRI-9303461 and IIS-9872128, and by a National Science Foundation Graduate Fellowship.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... \title²

Appeared IJCAI-99. Copyright ©1999, International Joint Conference on Artificial Intelligence (www.ijcai.org). All rights reserved.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... encodings³

Encoding each value as a separate boolean variable is a simple but unwieldy solution; bitwise-encodings produce smaller formulae but ones which appear very hard to solve [Ernst et al.1997].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... variables⁴

While the assignment to the constraint variables is optimal according to CASSOWARY's objective function, it is not guaranteed to be the globally optimal assignment to the real variables by the same measure; a different assignment to the propositional variables might provide a better solution. So, the specific function used is not vital (we use CASSOWARY's default which minimizes the slack in inequalities).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... variables⁵

This restriction falls in line with the pure literal elimination rule if we consider the triggers themselves to be clauses. The trigger $\mbox{\it MaxLoad} \Rightarrow$ (load $\leq$ 30) from Figure 2 would then become the clause $\neg\mbox{\em MaxLoad}\ \vee$ (load $\leq$ 30), and MaxLoad could no longer be purely positive.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... entries⁶

All three sets of runs use minimal conflict sets, learning, and backjumping.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.