A Covering Problem for Hypercubes

A Covering Problem for Hypercubes

J ¤org Hoffmann

Max-Planck-Institut f¤ur Informatik Saarbr¤ucken, Germany hoffmann@mpi-sb.mpg.de

Abstract

We introduce a new NP-complete problem asking if a �query� hypercube is (not) covered by a set of other �evidence� hypercubes. This comes down to a form of constraint reasoning asking for the satis�ability of a CNF formula where the logical atoms are inequalities over single variables, with possibly in�nite variable domains. We empirically investigate the location of the phase transition regions in two random distributions of problem instances. We introduce a solution method that iteratively constructs a representation of the non-covered part of the query cube. In particular, the method is not based on backtracking. Our experiments show that the method is, in a signi�cant range of instances, superior to the backtracking method that results from translation to SAT, and application of a stateof-the-art DP-based SAT solver.

This paper is an extended abstract. More details can be found in the long version of the paper [Hoffmann and Kupferschmid, 2005].

We introduce a new NP-complete problem asking if there is a point in a given n-dimensional �query� hypercube that is not covered by � contained in the union of � a set of other ndimensional �evidence� hypercubes. An n-dimensional hypercube is a cross product of n intervals. Intervals in our context are de�ned as statements of the form l < [≤] x < [≤] u where �x� is a variable, �l� and �u� are members of x's domain, and �<� is a total order de�ned over this domain. 1

De�nition 1 Let QCOVER denote the following problem: Given an n-dimensional hypercube Q, and a set E of ndimensional hypercubes, is there a point in Q that is not contained in ⋃E∈E E?

Covering problems of this kind arise, e.g., in the context of regression planning with numeric state variables [Koehler, 1998]. More generally, QCOVER is a form of constraint reasoning asking for the satis�ability of a CNF formula where the logical atoms are inequalities over single variables, with possibly in�nite variable domains. The correspondence is the

1 By square parentheses �symb1 [symb2]� we denote alternative possibilities, i.e. that symb2 can be substituted for symb1.

Sebastian Kupferschmid

Universit¤at Freiburg, Institut f¤ur Informatik Freiburg, Germany kupfersc@informatik.uni-freiburg.de

following. A QCOVER instance is a constraint problem with n variables xd . The query hypercube speci�es a region inside which the solution must lie, the evidence cubes specify regions inside which the solution must not lie. A hypercube corresponds to a conjunction of inequalities of the form c < [≤,>,≥] xd . So the complement of a hypercube (of an evidence hypercube) corresponds to a disjunction of such inequalities, and the overall problem is a conjunction of disjunctive constraints. Vice versa, any conjunction of such disjunctive constraints can be expressed as hypercubes (if a disjunctive constraint does not mention a variable xd , then the interval in dimension d is the whole variable domain).

Proposition 1 QCOVER is NP-complete.

We empirically explore two random distributions of QCOVER instances. The �rst one, which we call Random QCOVER, chooses the end points for all intervals uniformly from a set of m possible values. The second one, which we call Random 3-QCOVER, is similar to the �xed clause-length model for generating random 3SAT instances [Mitchell et al., 1992]. It always selects the query cube to be the cross-product of the (whole) variable domains, and, in the evidence cubes, assigns the whole variable domains to all but 3 randomly chosen dimensions. For both distributions, we investigate the location of the phase transition regions. As it turns out, Random 3-QCOVER shows a typical phase transition behaviour while RandomQCOVER shows no such behaviour, see Figure 1.

By 50% point, we denote the number k of evidence cubes at which our random instances have (empirically) equal probability of being satis�able or unsatis�able. The 50% point depends on n and m. We use instances from the 50% points to evaluate different solution methods.

Today, in most cases the empirically most ef�cient solution methods for satis�ability problems are backtracking methods. Such methods are depth-�rst searches that split, in each search node, the search space along the possible values of a variable. A polynomial propagation of constraints is used to determine con�icts early on in the search tree, and analysis of con�icts is used to prune unnecessary branches. Methods of this kind have proved successful for solving constraint satisfaction problems. In particular, the modern descendants of the Davis Putnam procedure still constitute the state-ofthe-art in determining the solvability of propositional CNF formulas. In our work, we have implemented a backtracking method for QCOVER by plugging a straightforward translation to SAT into Chaff [Moskewicz et al., 2001]. 2 To contrast this method, we have also developed an algorithm, named cube elimination, that, instead of backtracking over possible variable values, iteratively constructs a representation of the non-covered part of the query cube. See Figure 2.

procedure cube elimination(Q, E) Q := {Q} for all E ∈ E do Q′ := ∅ for all Q′ ∈ Q do Q′ :=Q′ ∪ minimal cover(Q′ \ E) endfor Q := Q′ if Q = ∅ then answer �unsatis�able�, return ∅ endif endfor answer �satis�able�, return Q

The algorithm maintains a set Q of hypercubes that initially contains only the query cube itself. Then iteratively all evidence cubes E are �eliminated� by subtracting them from all cubes Q in Q. The result Q \ E of such a subtraction is not necessarily a hypercube; we represent it as a set of hypercubes, computed by the minimal cover procedure. The latter is a simple for-loop over all dimensions, returning a set of hypercubes that covers exactly Q \ E, and that is minimal in the sense that there is no smaller set of hypercubes covering exactly Q \ E (the worst-case size of the set is 2n).

In SAT, where all variables are boolean and have only two possible values, cube elimination comes down to transforming the CNF into a DNF. This seems a hopeless approach, but, for our Random QCOVER distribution, our experiments show that cube elimination is often superior to the backtracking method implemented by Chaff. Figure 3 shows our results for the Random QCOVER distribution, in terms of (nr. of search decisions made by Chaff) divided by (total nr. of cubes generated by cube elimination). Clearly, cube elimination becomes superior as the value of m increases. This is particularly true in the unsatis�able instances where the cube elimination search space is, in the largest instances, around 5 orders of magnitude smaller than that of backtracking. It should be noted that cube elimination produces a representation of all satisfying assignments in the satis�able cases.

2 The translation implements the multiple-valued variable for each dimension by a set of boolean variables a that cover (only) the relevant case distinctions in that dimension. Binary exclusion clauses of the form ¬a ∨ ¬a′ ensure that, by unit propagation, only one variable a can be set to 1 at a time.

In the Random 3-QCOVER distribution, we found backtracking to be generally superior to cube elimination. For lack of space, we ommit the details. In spirit, cube elimination is somewhat similar to the �bucket elimination� framework de�ned by Rina Dechter [1999]. The cube elimination algorithm is easiest to understand, and was originally motivated by, viewing the satis�ability problem we consider as a geometrical problem. This opens up the question if geometrical interpretations of other satis�ability problems can lead to interesting new methods for these problems.