|
1.0figs/learn-ex2.eps
|
LPSAT inherits methods for learning and backjumping from
RELSAT [Bayardo and Schrag1997]. LPSAT's depth-first search of the
propositional search space creates a partial assignment to the boolean
variables. When the search fails, it is because the partial assignment
is inconsistent with the LCNF problem. LPSAT identifies an
inconsistent subset of the truth assignments in the partial
assignment, a conflict set, and uses this subset to learn in two
ways. First, since making the truth assignments represented in the
conflict set leads inevitably to failure, LPSAT can learn a clause
disallowing those particular assignments. For example, in the problem from
Figure 2 the constraints triggered by setting
MinFuel, MaxFuel, MaxLoad, and AllLoaded to true
are inconsistent, and MinFuel, MaxFuel, and
AllLoaded form a conflict set. So, LPSAT can learn the clause
.
Second, because continuing the search is
futile until at least one of the variables in the conflict set has its
truth assignment changed, LPSAT can backjump in its search to the
deepest branch points at which a conflict set variable received its
assignment, ignoring any deeper branch points.
Figure 4 shows a search tree in which MinFuel,
MaxFuel, MaxLoad, and AllLoaded have all been set to
true. Using the conflict set containing MinFuel, MaxFuel,
and AllLoaded, LPSAT can backjump past the branchpoint for
MaxLoad to the branchpoint for MinFuel, the deepest member
of the conflict set which is a branchpoint.
However, while LPSAT inherits methods to use conflict sets from RELSAT, LPSAT must produce those conflict sets for both propositional and constraint failures while RELSAT produces them only for propositional failures. Thus, given a propositional failure LPSAT uses RELSAT's conflict set discovery mechanism unchanged, learning a set based on two of the clauses which led to the contradiction [Bayardo and Schrag1997]. For a constraint conflict, however, LPSAT identifies an inconsistent subset of the active constraints, and the propositional triggers for these constraint compose the conflict set. We examine two methods for identifying these inconsistent subsets.
In our first method, called global conflict set discovery, LPSAT includes the entire set of active constraints in the conflict set. This mechanism is simple but often suboptimal since a smaller conflict set would provide greater pruning action. Indeed, preliminary experiments showed that -- while global conflict set discovery did increase solver speed over a solver with no learning or backjumping facility -- the conflict sets were on average twice as large as those found for logical conflicts.
In our second method, called minimal conflict set discovery, LPSAT identifies a (potentially) much smaller set of constraints which are responsible for the conflict. Specifically, our technique identifies an inconsistent conflict set of which every proper subset is consistent.
|
1.0figs/cons7.eps
|
Figure 5 illustrates the constraints from the example in Figure 2. The constraints MaxLoad, MaxFuel, and MinFuel and the implicit constraints that fuel and load be non-negative are all consistent; however, with the introduction of the dashed constraint marked AllLoaded the constraint set becomes inconsistent. Informally, LPSAT finds a minimal conflict set by identifying only those constraints which are, together, in greatest conflict with the new constraint. We now discuss how LPSAT discovers the conflicting constraints in this figure and which set it discovers.
When LPSAT adds the AllLoaded constraint to CASSOWARY's constraint set, CASSOWARY initially adds a ``slack'' version of the constraint which allows error and is thus trivially consistent with the current constraint set. This error is then minimized by the same routine used to minimize the overall objective function [Badros and Borning1998]. In Figure 5, we show the minimization as a move from the initial solution at the upper left corner point to the solution at the upper right corner point of the shaded region. The error in the solution is the horizontal distance from the solution point to the new constraint AllLoaded. Since no further progress within the shaded region can be made toward AllLoaded, the error has been minimized; however, since the error is non-zero, the strict constraint is inconsistent.
At this point, LPSAT uses ``marker variables'' (which CASSOWARY adds to each original constraint) to establish the conflict set. A marker variable is a variable that was added by exactly one of the original constraints and thus identifies the constraint in any derived equations. LPSAT examines the derived equation that gives the error for the new constraint, and notes that each constraint with a marker variable in this equation contributes to keeping the error non-zero. Thus, all the constraints identified by this equation, plus the new constraint itself, compose a conflict set.
In Figure 5 the MinFuel and MaxFuel constraints restrain the solution point from coming closer to the AllLoaded line. If the entire active constraint set were any two of those three constraints, the intersection of the two constraints' lines would be a valid solution; however, there is no valid solution with all three constraints.
Note that another conflict set (AllLoaded plus MaxLoad) exists with even smaller cardinality than the one we find. In general, there may be many minimal conflict sets, and our conflict discovery technique will discover only one of these, with no guarantee of discovering the global minimum. Some of these sets may prove to have better pruning action, but we know of no way to find the best minimal conflict set efficiently. However, the minimal conflict set is at least as good as (and usually better than) any of its supersets.
A brief proof that our technique will return a minimal conflict set appears in the LPSAT technical report [Wolfman and Weld1999].
indicates an inconsistent constraint set. The bold
variables are members of the conflict set.