MAX-PLANCK-INSTITUT FÜR

INFORMATIK

Linear 0-1 Inequalities and Extended Clauses

Peter Barth

MPI–I–94–216 April 1994

[figure: I N F O R M A T I K]

Im Stadtwald D 66123 Saarbrücken

Germany Author’s Address

Peter Barth Max-Planck-Institut für Informatik Im Stadtwald 66123 Saarbrücken, Germany Email: Peter.Barth@mpi-sb.mpg.de

Publication Notes

An earlier version of this paper has appeared as [Bar93].

Acknowledgements

The author is grateful to Alexander Bockmayr for his valuable comments and fruitful discussions. The work was supported by the German Ministry for Research and Technology (BMFT) (contract ITS 9103), the ESPRIT Basic Research Project ACCLAIM (contract EP 7195) and the ESPRIT Working Group CCL (contract EP 6028).

Abstract

Extended clauses are the basic formulas of the 0-1 constraint solver for the constraint logic programming language CLP(PB). We present a method for transforming an arbitrary linear 0-1 inequality into a set of extended clauses, such that the solution space remains invariant. After applying well-known linearization techniques on non-linear 0-1 constraints followed by the presented transformation method, we are able to handle arbitrary 0-1 constraints in CLP(PB).

The transformation method presented relies on cutting planes techniques known from 0-1 integer programming. We develop specialized redundancy criteria and so produce the minimal number of extended clauses needed for preserving equivalence. The method is enhanced by using a compact representation of linear 0-1 inequalities and extended clauses. Unit resolution for classical clauses is generalized to pseudo-Boolean unit resolution for arbitrary linear 0-1 inequalities. We extend the transformation method to constrained transformation when the inequality to be transformed is part of a larger set of linear 0-1 inequalities. Furthermore the method can be used to obtain all strongest extended cover inequalities of a knapsack inequality.

Keywords

constraint logic programming, pseudo-Boolean constraints, 0-1 integer programming, extended clauses, extended cover inequalities.

CONTENTS 1

Contents

1 Introduction 2 2 Preliminaries 4 3 Generating Valid Extended Clauses 8

3.1 The Strongest Extended Clause . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.2 Strict Reductions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

4 Identifying Redundant Extended Clauses 12 5 Implementation 18 6 Symmetries 21 7 Detection of Fixed Literals 24 8 Constrained Simplification 29

8.1 Coefficient Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 8.2 Constrained Strict Reductions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 8.3 Constrained Transformation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

9 Applications 40 9.1 Generalized Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 9.2 0-1 Integer Programming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

9.2.1 Extended Clauses and Extended Cover Inequalities . . . . . . . . . . . . . . . 43 9.2.2 Restrictions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 9.2.3 Computational Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

10 Conclusion 48

1 Introduction

0-1 constraint satisfaction problems have been investigated for a long time. Instantiating the computational domain X in the CLP(X) scheme of Jaffar and Lassez [JL87] with 0-1 or pseudo-Boolean constraints was first introduced by Bockmayr [Boc93]. The resulting language CLP(PB) aims to be a logic programming environment suitable for various applications where 0-1 problems naturally arise, which is the case for many AI-applications [BB93] and operations research.

In the context of constraint logic programming there are several special requirements for the constraint solver. Ideally, a constraint solver should detect inconsistency of a set of constraints, or, if the constraint set is inconsistent, provide a solved form, that is a description of all solutions of the constraint set. Van Hentenryck [VH89] introduces constraints over finite domains. The finite domain constraint solver is based on local consistency techniques and is successfully applied to a large variety of combinatorial problems. The main disadvantage of this approach is that, in order to achieve good computational behavior, constraint solving is relaxed such that

• global consistency of the constraint set is not assured and

• there is no solved form.

Obviously, 0-1 constraint satisfaction problems can be easily expressed as finite domain problems by restricting the domain of each domain variable to {0, 1}. Solving 0-1 problems and classical Boolean problems with this approach can be quite efficient [CD93]. Our goal is to provide a complete constraint solver for 0-1 constraints that computes a solved form of the accumulated constraints and provides an easy check of logical entailment and therefore satisfiability. Especially for concurrent constraint programming languages [SR90], deciding logical entailment of constraints is essential.

Granot et al. [GH71] showed how to express 0-1 constraints as an equivalent set of classical clauses. 0-1 constraints can then be solved with resolution based methods [Rob65] in an incremental way [Jac92]. The solved form then is a set of prime implicants, which fits exactly into our requirements. Early attempts of transforming arbitrary pseudo-Boolean constraints into an equivalent set of clauses failed mainly because of the large number of generated clauses [GH71, GG80]. Recently [Hoo92] has presented a deductive system “Generalized Resolution” working with extended clauses, an extension of classical clauses. Semantically, a classical Boolean clause states that at least one of its literals has to be true. So a classical Boolean clause

L_{1} ∨ … ∨ L_{n}

can be expressed as linear 0-1 inequality

L_{1} + ⋯ + L_{n} ≥ 1 ,

where a negated literal \overline{X_{i}} corresponds to (1−X_{i}) and the truth values false and true correspond to 0 and 1 respectively. Extended clauses generalize classical clauses by allowing other values than 1 on the right-hand side. An extended clause is of the form

L_{1} + ⋯ + L_{n} ≥ d ,

expressing that at least d of the n literals in the extended clause have to be 1. Hooker [Hoo92] shows that there exists an equivalent notion of prime implicants for a set of extended clauses, and the deductive system “Generalized Resolution” generates such a set of prime extended clauses. We propose to use extended clauses as basic constraints in our complete constraint solver, because

• there is a deductive system computing a solved form where satisfiability and logical entailment are easily decidable,

• the solved form describes all possible solutions and is explanative because of the natural d out of n interpretation,

• extended clauses are more expressive than classical clauses and provide a much more compact representation of information while preserving computational manageability.

For the latter point note that the equivalent representation of the extended clause L_{1} +⋯+L_{n} ≥ d using classical clauses without introducing new variables is

⋀_{I⊆{1,...,n}:|I|=n−d+1}(∨_{i∈I}L_{i}) ,

a conjunction of \binom{n}{n−d+1} clauses. Especially the more compact representation enables us to represent 0-1 constraints as an equivalent set of extended clauses, because the number of extended clauses needed is typically much smaller than the number of equivalent classical clauses. Applying standard linearization techniques to nonlinear constraints [BM84], we can transform arbitrary 0-1 constraints into a set of linear 0-1 inequalities. These linear 0-1 inequalities must then be transformed into an equivalent set of extended clauses in order to be processed by the constraint solver. In this paper we present a transformation method producing efficiently the minimal number of extended clauses that are equivalent to a given linear 0-1 inequality. We adopt cutting plane techniques, known from 0-1 integer programming, for generating valid extended clauses. Specialized redundancy criteria ensure that the minimal number of needed extended clauses is generated. Note that the number of needed extended clauses may be exponential w.r.t. the number of variables in the inequality. We introduce a compact representation of linear 0-1 inequalities and extended clauses and incorporate the technique into the transformation method. A linear 0-1 inequality is typically part of a set of linear 0-1 inequalities, and we show how to use this information in order to reduce the number of generated extended clauses. In this context we also present simplification methods and generalize the unit resolution procedure of classical clauses to linear 0-1 inequalities.

Beside the use of the presented method for the constraint solver of CLP(PB), we also relate extended cover inequalities [NW88] to the produced set of extended clauses. We show that the method generates the set of all strongest, non redundant extended cover inequalities, which can be used in a preprocessing phase of a 0-1 integer programming solver. Another application is the implementation of one of the basic deduction rules of “Generalized Resolution” that allows to apply several resolution steps at once.

The paper is organized as follows. In Sect. 2 we give basic definitions and introduce extended clauses and the pseudo-Boolean normal form of linear 0-1 inequalities. We discuss the generation of valid extended clauses from a pseudo-Boolean inequality in Sect. 3, and prove the equivalence of the set of generated extended clauses and the pseudo-Boolean inequality. Strong redundancy criteria, that allow an efficient redundancy test, are presented in Sect. 4. With help of the redundancy criteria only the minimal number of extended clauses is generated. We sketch an implementation of the transformation method in Sect. 5. An important improvement is the use of symmetries along with the compact form of pseudo-Boolean inequalities and extended clauses, introduced in Sect. 6. In Sect. 7 we generalize unit resolution for classical clauses to pseudo-Boolean unit resolution. Unit relaxation of a set of pseudo-Boolean inequalities is defined and we obtain a simple incomplete unsatisfiability check that is used to detect some of the fixed literals of a set of pseudo-Boolean inequalities. In Sect. 8 the transformation procedure is generalized to the case where the pseudo-Boolean inequality is part of a larger set of pseudo-Boolean inequalities. We present in this context also simplification routines for strengthening a pseudo-Boolean inequality and splitting a pseudo-Boolean inequality into a set of equivalent but simpler pseudo-Boolean inequalities. Two applications of the transformation routine, namely the implementation of one of the basic deduction rules of ”Generalized Resolution” and traditional 0-1 integer programming, are described in Sect. 9. We show how to apply the presented techniques in a preprocessing phase of 0-1 integer programming problems and give some encouraging computational results followed by the conclusion in Sect. 10.

2 Preliminaries

We use the following conventions and abbreviations [Hoo92]. Let B = {X_{1}, X_{2}, …, X_{n}} be a finite set of Boolean variables and the domain of the X_{i} be {0, 1}. A literal L_{j} is either a Boolean variable X_{i} (a positive literal), or the negation of a variable \overline{X_{i}} (a negative literal). Let L be the set of all literals. The negation of a negative literal \overline{\overline{X_{i}}} is always simplified to X_{i}. We denote by Var(X_{i}) = Var(\overline{X_{i}}) = X_{i} the variable of a literal. An assignment is a mapping α from B to {0, 1}. An assignment can also be seen as a 0-1 vector of dimension n. We extend α to a mapping from L to \{0, 1\} by defining α(\overline{X_{i}}) := 1 − α(X_{i}). A set of literals L = \{L_{1}, …, L_{n}\} can also be seen as a sum of literals L_{1} + ⋯ + L_{n}. We extend α to a mapping from 2^{L} to IN by defining α(L) := α(L_{1}) + ⋯ + α(L_{n}), that is the number of literals that are mapped to 1. A product c_{i}L_{i} is a pair of an integer coefficient c_{i} and a literal L_{i}. A set of products cL = {c_{1}L_{1}, …, c_{n}L_{n}} can also be seen as sum of products c_{1}L_{1} + ⋯ + c_{n}L_{n}. We extend α to a mapping from 2^{ZZ×L} to ZZ by defining α(cL) := c_{1}α(L_{1}) + ⋯ + c_{n}α(L_{n}), that is the sum over the coefficients whose literals are mapped to 1. For a set of products cL we denote by s(c) := c_{1} + ⋯ + c_{n} the sum over the integer coefficients of cL.

An extended clause is of the form

L_{1} + ⋯ + L_{n} ≥ d

where 0 ≤ d ≤ n + 1 and Var(L_{i}) ≠ Var(L_{j}) for all 1 ≤ i, j ≤ n. An assignment α satisfies an extended clause L ≥ d if at least d of its n literals are mapped to 1, that is if α(L) ≥ d. If d ≥ n + 1 then there is no assignment satisfying L ≥ d and we abbreviate L ≥ d by □. If d = 0 then every assignment is a satisfying assignment of L ≥ d. We say then that L ≥ d is a tautology and abbreviate it by ⊤. We denote by deg(L ≥ d) = d the degree of an extended clause L ≥ d. Note that classical clauses are extended clauses with degree 1.

A linear pseudo-Boolean (or 0-1 ) inequality is of the form

c_{1}L_{1} + ⋯ + c_{n}L_{n} ≥ d

where the c_{i} and d are integer numbers. An assignment α satisfies a linear pseudo-Boolean inequality cL ≥ d if α(cL) ≥ d. If there is no assignment satisfying cL ≥ d we abbreviate cL ≥ d by □. If every assignment satisfies cL ≥ d, then cL ≥ d is a tautology and we abbreviate it by ⊤. As for extended clauses, we like to have only one occurrence of a variable in a linear pseudo-Boolean inequality, and we want to be able to immediately detect whether cL ≥ d is □, or whether it is a tautology.

Definition 2.1 A linear pseudo-Boolean inequality cL ≥ d is in (pseudo-Boolean) normal form if

d ≥ c_{1} ≥ ⋯ ≥ c_{n} ≥ 1 and Var(L_{i}) ≠ Var(L_{j}) for all 1 ≤ i < j ≤ n .

We assume that d ≥ 1 since otherwise the linear pseudo-Boolean inequality in normal form is a tautology, that is, it is valid for every assignment α and therefore need not be considered.

Proposition 2.2 [HR68] For each non tautologous linear 0-1 inequality there is a linear pseudo-Boolean inequality in normal form admitting the same set of satisfying assignments.

PROOF: We begin with an arbitrary linear pseudo-Boolean inequality

e_{1}L′_{1} + ⋯ + e_{m}L′_{m} ≥ d′ ,  (1)

and construct in the following a linear pseudo-Boolean inequality in normal from. We first apply several arithmetic equivalence transformations. We rewrite (1) such that literals containing the same variable are grouped together and obtain

a_{1}X_{1} + b_{1}\overline{X_{1}} + ⋯ + a_{n}X_{n} + b_{n}\overline{X_{n}} ≥ d′ ,

where the X_{i} are pairwise different. For each i such that a_{i} = b_{i} we can simplify a_{i}X_{i} + b_{i}\overline{X_{i}} to the constant a_{i} and move the constant a_{i} to the right-hand side. So let us assume that a_{i} ≠ b_{i} for all 1 ≤ i ≤ n. We next replace a_{i}X_{i} + b_{i}\overline{X_{i}} by c′_{i}L_{i} + c′′_{i} for all 1 ≤ i ≤ n according to

c′_{i}L_{i} + c′′_{i} := \{ \begin{matrix}(a_{i} − b_{i})X_{i} + b_{i} & if & a_{i} > b_{i} \\ (b_{i} − a_{i})\overline{X_{i}} + a_{i} & if & b_{i} > a_{i} . \end{matrix}

Note that the c′_{i} are all positive. Bringing the constants c′′_{i} to the right-hand side gives us the new right-hand side d = d′ − ∑_{i=1}^{n} c′′_{i}. After re-indexing according to the ordering restriction we have brought the linear 0-1 inequality into the form

c′_{1}L_{1} + ⋯ + c′_{n}L_{n} ≥ d .  (2)

where c′_{1} ≥ ⋯ ≥ c′_{n} ≥ 1 and Var(L_{i}) ≠ Var(L_{j}) for all 1 ≤ i < j ≤ n. Note that d ≥ 1, since otherwise (1) is a tautology. So far we have only applied arithmetic equivalence transformations, hence an assignment α satisfies (1) if and only if α satisfies (3). When constructing the pseudo-Boolean normal form of a linear pseudo-Boolean inequality we can detect at this point whether we have a tautology or not.

Suppose that c′_{i} > d for some i, then every assignment α where α(L_{i}) = 1 maps the left-hand side of (2) to an integer greater than d and satisfies (2). For all assignments α where α(L_{i}) = 0 the value of the left-hand side is independent of c_{i}. Hence we can safely replace each c′_{i} by d if c′_{i} > d. This step is also called coefficient reduction [CJP83]. Formally we define

c_{i} := \{ \begin{matrix}c′_{i} & if & c′_{i} ≤ d \\ d & if & c′_{i} > d \end{matrix}

for all 1 ≤ i ≤ n, and thereby obtain the pseudo-Boolean normal form

c_{1}L_{1} + ⋯ + c_{n}L_{n} ≥ d  (3)

of (1), where d ≥ c_{1} ≥ ⋯ ≥ c_{n} ≥ 1. Obviously an assignment α satisfies (1) if and only if α satisfies (2) if and only if α satisfies (3). ⊓ ⊔

Note that a linear pseudo-Boolean inequality in normal form cL ≥ d is satisfiable if and only if s(c) ≥ d, because c_{i} > 0 for all 1 ≤ i ≤ n. Hence cL ≥ d is unsatisfiable if and only if s(c) < d, and we can easily decide whether cL ≥ d is □.

Example 2.3 Let us transform the linear 0-1 inequality

− 6 · X_{1} + −5 · X_{6} + 4 · X_{3} + 3 · X_{6} + 3 · X_{4} + 3 · X_{3} + 2 · X_{1} + 2 · \overline{X_{3}} + 2 · X_{5} + −2 · \overline{X_{6}} + 1 · X_{2} ≥ 7 (4)

into pseudo-Boolean normal form using Prop. 2.2. We first regroup the products and obtain

4 · X_{3} + 3 · X_{3} + 2 · \overline{X_{3}} + −6 · X_{1} + 2 · X_{1} + 3 · X_{4} + 2 · X_{5} + 1 · X_{2} + −5 · X_{6} + 3 · X_{6} + −2 · \overline{X_{6}} ≥ 7

which simplifies to

7·X_{3} +2·\overline{X_{3}} +−4·X_{1} +0·\overline{X_{1}} +3·X_{4} +0·\overline{X_{4}} +2·X_{5} +0·\overline{X_{5}} +1·X_{2} +0·\overline{X_{2}} +−2·X_{6} +−2·\overline{X_{6}} ≥ 7 .

Because a_{6} = −b_{6} = −2 we simplify −2 · X_{6} + −2 · \overline{X_{6}} to −2 and derive

7 · X_{3} + 2 · \overline{X_{3}} + −4 · X_{1} + 0 · \overline{X_{1}} + 3 · X_{4} + 0 · \overline{X_{4}} + 2 · X_{5} + 0 · \overline{X_{5}} + 1 · X_{2} + 0 · \overline{X_{2}} ≥ 7 + 2 = 9 .

We next replace the a_{i}X_{i} + b_{i}\overline{X_{i}} by c′_{i}L_{i} + c′′_{i} according to Prop. 2.2 and obtain

5 · X_{3} + 2 + 4 · \overline{X_{1}} + −4 + 3 · X_{4} + 0 + 2 · X_{5} + 0 + 1 · X_{2} + 0 ≥ 9 .

By bringing the constants to the right-hand side we have

5 · X_{3} + 4 · \overline{X_{1}} + 3 · X_{4} + 2 · X_{5} + 1 · X_{2} ≥ 9 − 2 + 4 = 11 .

After re-indexing we obtain the pseudo-Boolean normal form

5 · L_{1} + 4 · L_{2} + 3 · L_{3} + 2 · L_{4} + 1 · L_{5} ≥ 11  (5)

of (4), where L_{1} = X_{3}, L_{2} = \overline{X_{1}}, L_{3} = X_{4}, L_{4} = X_{5}, and L_{5} = X_{2}.

Assumption 2.4 From now on we assume that all linear 0-1 inequalities are in pseudo-Boolean normal form.

Note that an extended clause is a linear pseudo-Boolean inequality cL ≥ d where all the c_{i} are 1.

Let us say that the extension Ext(I) of a linear pseudo-Boolean inequality I is the set of assignments α satisfying I. The extension Ext(S) of a set of linear pseudo-Boolean inequalities S is the intersection of the extensions of the linear pseudo-Boolean inequalities in S. A set of linear pseudo-Boolean inequalities S is satisfiable if Ext(S) is nonempty. A set of linear pseudo-Boolean inequalities S (strictly) dominates a set of pseudo-Boolean inequality S′ if Ext(S) is a (proper) subset of Ext(S′). We also write S ⊧ S′ if S dominates S′. We abbreviate {I} ⊧ S′ by I ⊧ S′ and S ⊧ {I} by S ⊧ I. Two sets of linear pseudo-Boolean inequalities S, S′ are equivalent if Ext(S) = Ext(S′). If a set of linear pseudo-Boolean inequalities S dominates a linear pseudo-Boolean inequality I, we say I is valid w.r.t. S.

Let us say that a linear pseudo-Boolean inequality cL ≥ d reduces to c′L ≥ d′ (the reduction) if 0 ≤ c′_{i} ≤ c_{i} for all 1 ≤ i ≤ n and d′ = d − (s(c) − s(c′)). We require that d′ ≥ 1 and so forbid reduction to tautologies. Because α(cL) − d ≤ α(c′L) − d′ for all assignments α, a linear pseudo-Boolean inequality dominates all its reductions. We denote by Red(cL ≥ d) the set of all reductions of a linear pseudo-Boolean inequality cL ≥ d. We say a linear pseudo-Boolean inequality cL ≥ d strictly reduces to c′L′ ≥ d′ if c′L′ ≥ d′ is a reduction and either c′_{i} = c_{i} or c′_{i} = 0 for all 1 ≤ i ≤ n. We say we have eliminated the literal L_{i} if c′_{i} = 0. We denote by SRed(cL ≥ d) the set of all strict reductions of a linear pseudo-Boolean inequality cL ≥ d. A reduction of an extended clause L ≥ d is L \ L′ ≥ d − |L′| where L′ ⊆ L.

Deciding domination between linear pseudo-Boolean inequalities is an NP-complete problem^{1}. We show next that extended clauses are a generalization of classical clauses, where one of the main properties, namely domination, remains easily decidable.

Lemma 2.5 L ≥ d dominates L′ ≥ d′ iff

|L \ L′| ≤ d − d′ .  (6)

PROOF:

“⇐”: We eliminate all literals from L that are not in L′ and obtain L ∩ L′ ≥ d − |L \ L′|, that is a reduction of L ≥ d. Since |L \ L′| ≤ d − d′, we have 0 ≤ d′ ≤ d − |L \ L′| ≤ d and therefore L ≥ d also dominates L ∩ L′ ≥ d′. Since L ∩ L′ ⊆ L′, we know that L ≥ d dominates L′ ≥ d′.

“⇒”: We assume that |L \ L′| > d − d′ and show that in this case L ≥ d does not dominate L′ ≥ d′ by constructing an assignment α satisfying L ≥ d, but not L′ ≥ d′. We choose α ∈ Ext(L ≥ d) such that α(L) = d and α(L_{i}) = 0 for all L_{i} ∈ L′ \ L. Then we know that α(L′) = d − |L \ L′|. Since |L \ L′| > d − d′, we have d − |L \ L′| < d′ and therefore α(L′) < d′. But then α is not in the extension of L′ ≥ d′, that is L ≥ d does not dominate L′ ≥ d′. ⊓ ⊔

When deciding domination between two classical clauses L ≥ 1 and L′ ≥ 1, condition (6) reduces to |L \ L′| ≤ 0, which is equivalent to L ⊆ L′; the usual condition for deciding domination (or implication) between classical clauses.

1 Note that a linear pseudo-Boolean inequality cL ≥ d dominates another linear pseudo-Boolean inequality c′L′ ≥ d′ iff the maximum of c′L′ subject to cL ≥ d is greater than d′. So deciding domination between two linear pseudo-Boolean inequalities involves solving a knapsack problem [NW88].

We say a set of extended clauses S is in normal form if no extended clause in S dominates another extended clause in S. Obviously every set of extended clauses S can be easily brought into normal form by deleting all extended clauses that are dominated by other extended clauses in S.

Assumption 2.6 From now on we assume that all sets of extended clauses are in normal form.

3 Generating Valid Extended Clauses

We show how to generate a set of extended clauses equivalent to a linear pseudo-Boolean inequality. We define the strongest extended clause of a linear pseudo-Boolean inequality, and relate it to cutting plane inequalities known from 0-1 integer programming [NW88]. The equivalence of the set of all strongest extended clauses of all strict reductions of a linear pseudo-Boolean inequality and the linear^{2} pseudo-Boolean inequality itself, is the key theorem of this section.

3.1 The Strongest Extended Clause

Linear combination and integer rounding are well known techniques of 0-1 integer programming for deriving valid inequalities [NW88]. We adopt these techniques in order to generate valid extended clauses.

Let us divide a pseudo-Boolean inequality in normal form

c_{1}L_{1} + ⋯ + c_{n}L_{n} ≥ d  (7)

by a positive integer k and round the fractional coefficients of the left-hand side yielding

⌈c_{1}/k⌉L_{1} + ⋯ + ⌈c_{n}/k⌉L_{n} ≥ d/k ,

where ⌈a⌉ = min({b ∈ IN : b ≥ a}). Because rounding only increases the left-hand side, we have generated a valid inequality w.r.t. (7). Since the coefficients ⌈c_{i}/k⌉ are integer, the left-hand side is integer for all assignments. Therefore, the right-hand side d/k can be replaced by the largest integer less than or equal to d/k, that is ⌈d/k⌉. We obtain the valid pseudo-Boolean inequalities

⌈c_{1}/k⌉L_{1} + ⋯ + ⌈c_{n}/k⌉L_{n} ≥ ⌈d/k⌉ ,

dominated by (7), for all positive integers k. These pseudo-Boolean inequalities are a subclass of the so called cutting plane inequalities [NW88], obtained from a linear combination of the pseudo-Boolean inequality and the valid bounds L_{i} ≥ 0 and −L_{i} ≥ −1 for the literals L_{i} followed by integer rounding of the coefficients and the right-hand side. We obtain the valid extended clause

L_{1} + ⋯ + L_{n} ≥ ⌈d/c_{1}⌉ ,  (8)

dominated by (7), if we set k = c_{1} since then the ⌈c_{i}/k⌉ are all 1. The extended clause (8) derived from a pseudo-Boolean inequality cL ≥ d is denoted by CP(cL ≥ d), and we know that cL ≥ d dominates CP(cL ≥ d).

2Since we do not consider nonlinear pseudo-Boolean inequalities throughout the paper we may omit the word “linear” in the following.

Example 3.1 Let cL ≥ d be

5 · L_{1} + 4 · L_{2} + 3 · L_{3} + 2 · L_{4} + 1 · L_{5} ≥ 11 ;

then CP(cL ≥ d) is

L_{1} + L_{2} + L_{3} + L_{4} + L_{5} ≥ 3 .

For a set of pseudo-Boolean inequalities S we denote by CP(S) the set of extended clauses CP(cL ≥ d) for all cL ≥ d in S. The cutting plane operation CP generates a valid extended clause L ≥ d′ dominated by a pseudo-Boolean inequality cL ≥ d. We are now interested in the greatest integer β such that L ≥ β is dominated by cL ≥ d.

Proposition 3.2 A pseudo-Boolean inequality cL ≥ d dominates the extended clause

L ≥ β ,  (9)

where β is the smallest β such that ∑_{i=1}^{β} c_{i} ≥ d, determined by the condition

∑_{i=1}^{β−1} c_{i} < d ≤ ∑_{i=1}^{β} c_{i} .  (10)

The extended clauses L ≥ β + l are not dominated by cL ≥ d for all l ≥ 1. Hence (9) is the strongest extended clause w.r.t. cL ≥ d with left-hand side L.

PROOF:

[a] We show first that cL ≥ d dominates L ≥ β. Because cL ≥ d is in pseudo-Boolean normal form, we know that c_{1} ≥ ⋯ ≥ c_{n}. Thus for all 1 ≤ k ≤ n we have ∑_{i=1}^{k} c_{i} ≥ ∑_{i∈K} c_{i} for all K ⊆ {1, …, n} and |K| = k. Let k be β − 1. Since ∑_{i=1}^{β−1} c_{i} < d we know that ∑_{i∈K} c_{i} < d for all K ⊆ {1, …, n} and |K| = β − 1. Consequently for all satisfying assignments α ∈ Ext(cL ≥ d) we have α(L) > β − 1 and therefore α(L) ≥ β.

[b] We next show that cL ≥ d does not dominate L ≥ β + l for all l ≥ 1. Let α be an assignment such that α(L_{1}) = … = α(L_{β}) = 1 and α(L_{β+1}) = … = α(L_{n}) = 0. Then α ∈ Ext(cL ≥ d) because ∑_{i=1}^{β} c_{i} ≥ d, but α ∉ Ext(L ≥ β + l) for all l ≥ 1 because α(L) = β. ⊓ ⊔

For a pseudo-Boolean inequality cL ≥ d we denote by SCP(cL ≥ d) the strongest extended clause L ≥ β of Prop. 3.2. For a set of pseudo-Boolean inequalities S we denote by SCP(S) the set of all extended clauses SCP(cL ≥ d) with cL ≥ d in S. From Proposition 3.2 we know that the degree of SCP(cL ≥ d) is greater than or equal to the degree of CP(cL ≥ d); therefore SCP(cL ≥ d) dominates CP(cL ≥ d). Note that SCP(cL ≥ d) is also a cutting plane inequality, i.e. it can be obtained as a linear combination from cL ≥ d and the bounds L_{1} ≥ 0 and −L_{1} ≥ −1, followed by integer rounding. It is not necessary to construct the strongest extended clause using linear combination and integer rounding, because Prop. 3.2 guarantees that SCP(cL ≥ d) is already the strongest extended clause.

Example 3.3 Let cL ≥ d again be

5 · L_{1} + 4 · L_{2} + 3 · L_{3} + 2 · L_{4} + 1 · L_{5} ≥ 11

as in Example 3.1, then

CP(cL ≥ d) = SCP(cL ≥ d) = L_{1} + L_{2} + L_{3} + L_{4} + L_{5} ≥ 3 .

If cL ≥ d is

5 · L_{1} + 4 · L_{2} + 3 · L_{3} + 2 · L_{4} + 1 · L_{5} ≥ 10

then

CP(cL ≥ d) = L_{1} + L_{2} + L_{3} + L_{4} + L_{5} ≥ 2

and

SCP(cL ≥ d) = L_{1} + L_{2} + L_{3} + L_{4} + L_{5} ≥ 3 .

Note that SCP(cL ≥ d) strictly dominates CP(cL ≥ d).

3.2 Strict Reductions

We know that all reductions of a pseudo-Boolean inequality cL ≥ d are valid w.r.t. cL ≥ d. Hence for all strict reductions c′L′ ≥ d′ of cL ≥ d we know that SCP(c′L′ ≥ d′) is a valid extended clause w.r.t. cL ≥ d.

Example 3.4 A strict reduction of

5 · L_{1} + 4 · L_{2} + 3 · L_{3} + 2 · L_{4} + 1 · L_{5} ≥ 11

is

5 · L_{1} + 4 · L_{2} + 3 · L_{3} + 2 · L_{4} ≥ 10

obtained by eliminating L_{5}. Its strongest extended clause is

L_{1} + L_{2} + L_{3} + L_{4} ≥ 3 .

We now show that SCP(SRed(cL ≥ d)), the set of strongest extended clauses derived from all strict reductions of a pseudo-Boolean inequality cL ≥ d, is equivalent to cL ≥ d. For that we first show that a set of pseudo-Boolean inequalities dominates the set of all strongest extended clauses derived from the pseudo-Boolean inequalities in that set.

Lemma 3.5 Let S be a set of pseudo-Boolean inequalities, then

Ext(S) ⊆ Ext(SCP(S)) .

PROOF: The strongest extended clause of a pseudo-Boolean inequality cL ≥ d is valid w.r.t. cL ≥ d. Therefore we have Ext(cL ≥ d) ⊆ Ext(SCP(cL ≥ d)). Because the intersection of sets T_{i} is a subset of the intersection of sets T′_{i} if T_{i} ⊆ T′_{i}, the lemma is established. ⊓ ⊔ Theorem 3.6 Let cL ≥ d be an arbitrary linear pseudo-Boolean inequality; then

Ext(cL ≥ d) = Ext(SCP(SRed(cL ≥ d))) .  (11)

PROOF:

[a] Ext(cL ≥ d) ⊆ Ext(SCP(SRed(cL ≥ d))) : For all strict reductions c′L′ ≥ d′ of cL ≥ d we know that Ext(cL ≥ d) ⊆ Ext(c′L′ ≥ d′) because cL ≥ d dominates c′L′ ≥ d′. Hence

Ext(cL ≥ d) ⊆ ⋂_{c′L′≥d′∈SRed(cL≥d)} Ext(c′L′ ≥ d′) = Ext(SRed(cL ≥ d)) .

By Lemma 3.5 we have Ext(SRed(cL ≥ d)) ⊆ Ext(SCP(SRed(cL ≥ d))).

[b] Ext(SCP(SRed(cL ≥ d))) ⊆ Ext(cL ≥ d) : We show that if α ∉ Ext(cL ≥ d), then α ∉ Ext(SCP(SRed(cL ≥ d))) from which the theorem follows. Suppose that α ∉ Ext(cL ≥ d). We show that in this case there is a strict reduction of cL ≥ d such that α is not a satisfying assignment of this reduction, and therefore α ∉ Ext(SCP(SRed(cL ≥ d))). Since α ∉ Ext(cL ≥ d), we know that α(cL) = d′ < d. Let Y be the set of literals L_{i} where α(L_{i}) = 1 and Z = L \ Y, then ∑_{i:L_{i}∈Y} c_{i} = d′ < d. Let c′L′ ≥ d′ be ∑_{i:L_{i}∈Z} c_{i}L_{i} ≥ d−d′. Because d′ < d, we know that d−d′ ≥ 1, and therefore c′L′ ≥ d′ is a strict reduction of cL ≥ d, obtained by eliminating the literals that are mapped to zero by α. Let SCP(c′L′ ≥ d′) be L′ ≥ β. We know that β ≥ 1 because d − d′ ≥ 1. Because α(L′) = 0, we derive that α ∉ Ext(SCP(c′L′ ≥ d′)), and therefore α ∉ Ext(SCP(SRed(cL ≥ d))), which proves the theorem. ⊓ ⊔

Theorem 3.6 gives a simple procedure for transforming a linear pseudo-Boolean inequality into an equivalent set of extended clauses. Unfortunately a very large number of extended clauses may be produced. Obviously we preserve equivalence if we consider only extended clauses that are not dominated by others.

Example 3.7 The set of all strongest extended clauses of all strict reductions of

5 · L_{1} + 4 · L_{2} + 3 · L_{3} + 2 · L_{4} + 1 · L_{5} ≥ 11  (12)

is

\begin{matrix}L_{1} + L_{2} + L_{3} + L_{4} + L_{5} ≥ 3 & L_{1} + L_{2} + L_{3} + L_{4} ≥ 3 & L_{1} + L_{2} + L_{3} + L_{5} ≥ 2 \\ L_{1} + L_{2} + L_{4} + L_{5} ≥ 2 & L_{1} + L_{3} + L_{4} + L_{5} ≥ 2 & L_{2} + L_{3} + L_{4} + L_{5} ≥ 2 \\ L_{1} + L_{2} + L_{3} ≥ 2 & L_{1} + L_{2} + L_{4} ≥ 2 & L_{1} + L_{2} + L_{5} ≥ 2 \\ L_{1} + L_{3} + L_{4} ≥ 2 & L_{1} + L_{3} + L_{5} ≥ 1 & L_{1} + L_{4} + L_{5} ≥ 1 \\ L_{2} + L_{3} + L_{4} ≥ 2 & L_{2} + L_{3} + L_{5} ≥ 1 & L_{2} + L_{4} + L_{5} ≥ 1 \\ L_{3} + L_{4} + L_{5} ≥ 1 & L_{1} + L_{2} ≥ 1 & L_{1} + L_{3} ≥ 1 \\ L_{1} + L_{4} ≥ 1 & L_{1} + L_{5} ≥ 1 & L_{2} + L_{3} ≥ 1 \\ L_{2} + L_{4} ≥ 1 & L_{2} + L_{5} ≥ 1 & L_{3} + L_{4} ≥ 1 L_{1} ≥ 1 . \end{matrix}

Note that there are 25 strict reductions and therefore 25 extended clauses. If we delete all extended clauses that are dominated by others, we obtain

L_{1} + L_{2} + L_{3} + L_{4} ≥ 3  L_{1} + L_{2} + L_{5} ≥ 2  L_{1} ≥ 1 .

The set of these 3 extended clauses is equivalent to (12).

An interesting property is that the normal form of SCP(SRed(cL ≥ d)) is prime.

Definition 3.8 A set of extended clauses S is called prime if for all extended clauses L ≥ d that are dominated by S there is an extended clause in S dominating L ≥ d.

Proposition 3.9 For all extended clauses L′ ≥ d′ dominated by SCP(SRed(cL ≥ d)) there exists an extended clause in SCP(SRed(cL ≥ d)) dominating L′ ≥ d′.

PROOF: Suppose that L′ ≥ d′ is dominated by SCP(SRed(cL ≥ d)). Because Ext(cL ≥ d) = Ext(SCP(SRed(I))), we know that cL ≥ d dominates L′ ≥ d′. Obviously cL ≥ d dominates L′ ≥ d′ only if it dominates L′′ ≥ d′ where L′′ = L′ ∩ L. We consider the strict reduction c′′L′′ ≥ d′′ of cL ≥ d and its corresponding strongest extended clause L′′ ≥ β. From Prop. 3.2 we know that β ≥ d′, and therefore L′′ ≥ β in SCP(SRed(cL ≥ d)) dominates L′ ≥ d′. ⊓ ⊔

Hence, for a single pseudo-Boolean inequality cL ≥ d the normal form of SCP(SRed(cL ≥ d)) is already the solved form that should be extracted by our constraint solver.

The challenge is to find the normal form of SCP(SRed(cL ≥ d)) without completely constructing the dominated and therefore redundant extended clauses, and to minimize the number of domination checks. In the following we describe strong redundancy criteria identifying extended clauses that are dominated by other extended clauses.

4 Identifying Redundant Extended Clauses

The normal form of SCP(SRed(cL ≥ d)), that is all non redundant extended clauses in SCP(SRed(cL ≥ d)), is the set of extended clauses, equivalent to cL ≥ d, that we want to build. A naive way is to completely generate SCP(SRed(cL ≥ d)), and then delete the redundant extended clauses. Typically many of the generated extended clauses are redundant. We develop strong redundancy criteria that minimize the number of domination checks needed for deciding whether an extended clause is redundant, i.e. is dominated by another extended clause. We show how to decide redundancy of an extended clause in SCP(SRed(cL ≥ d)) by checking domination against two other extended clauses. For this purpose we first arrange the elements of SCP(SRed(cL ≥ d)) as a directed acyclic graph.

Let T = T (cL ≥ d) be a finite acyclic graph with root node where the nodes are labeled with the strict reductions of cL ≥ d. The root of T is labeled by cL ≥ d. The direct subgraphs of T are the graphs T (c′L′ ≥ d′) for all strict reductions c′L′ ≥ d′ of cL ≥ d, where exactly one literal has been eliminated. We denote by T (T, j) the direct subgraph of T with the label ∑_{1≤i≠j≤n} c_{i}L_{i} ≥ d − c_{j}, provided that d − c_{j} ≥ 1. We abbreviate T (T (… (T (T, j_{1}), j_{2}), …), j_{k}) by T ({j_{1}, …, j_{k}}). We say j_{1} … j_{k} is a path to the graph T ({j_{1}, …, j_{k}}). Note that every permutation of j_{1} … j_{k} is a path to T ({j_{1}, …, j_{k}}), and that every element of SRed(cL ≥ d) is the label of exactly one node in T (cL ≥ d). We denote by T_{j} the strongest extended clause of the root label of T (T, j). The strongest extended clause of the root label of T ({j_{1}, …, j_{k}}) is referenced by T_{{j_{1},...,j_{k}}}. Note that the extended clause T_{{j_{1},...,j_{k}}} has n − k literals, therefore the length of the path determines the number of literals of the label. A part of the graph view of SCP(SRed(cL ≥ d)) is shown in

\begin{matrix}c_{1}L_{1} … c_{n}L_{n} ≥ d \\ L_{1} … L_{n} ≥ β_{∅} \end{matrix} ; \begin{matrix}c_{2}L_{2} … c_{n}L_{n} ≥ d − c_{1} \\ L_{2} … L_{n} ≥ β_{\{1\}} \end{matrix}  \begin{matrix}c_{1}L_{1} … ≥ d − c_{n−2} \\ L_{1} … L_{n−3}L_{n−1}L_{n} ≥ β_{\{n−2\}} \end{matrix}  \begin{matrix}c_{1}L_{1} … c_{n−1}L_{n−1} ≥ d − c_{n} \\ L_{1} … L_{n−1} ≥ β_{\{n\}} \end{matrix} ; \begin{matrix}c_{1}L_{1} … c_{n−3}L_{n−3}c_{n−1}L_{n−1} ≥ d − c_{n−2} − c_{n−1} \\ L_{1} … L_{n−3}L_{n−1} ≥ β_{\{n−2,n\}} \end{matrix}  \begin{matrix}c_{1}L_{1} … c_{n−2}L_{n−2} ≥ d − c_{n} \\ L_{1} … L_{n−2} ≥ β_{\{n−1,n\}} \end{matrix} L_{1} L_{n−2} L_{n} L_{n} L_{n−2} L_{n−1}

Figure 1: Part of a graph view of SCP(SRed(cL ≥ d))

Fig. 1. For each node we show the strict reduction and its corresponding strongest extended clause. Additionally the arcs are labeled by the literal L_{i} that we eliminated from father node to son node.

In the following we denote by J_{k} := {j_{1}, …, j_{k}} ⊂ {1, …, n} a set of indices such that T (J_{k}) is a valid strict reduction of cL ≥ d. We denote by \overline{J_{k}} := \{j′_{1}, …, j′_{n−k}\} the set of indices of the remaining literals in T (J_{k}), that is \overline{J_{k}} ∪ J_{k} = \{1, …, n\} and \overline{J_{k}} ∩ J_{k} = ∅. We then have

T (J_{k}) = ∑_{i=1}^{n−k} c_{j′_{i}}L_{j′_{i}} ≥ d − ∑_{i=1}^{k} c_{j_{i}} .

We abbreviate ∑_{i=1}^{n−k} c_{j′_{i}}L_{j′_{i}} by c(J_{k})L(J_{k}) and ∑_{i=1}^{n−k} L_{j′_{i}} by L(J_{k}). We first investigate the degrees of the strongest extended clauses along a path.

Lemma 4.1 For all J_{k} and J_{k+1} = J_{k} ∪ {j_{k+1}} we have

deg(T_{J_{k}}) ≥ deg(T_{J_{k+1}}) ≥ deg(T_{J_{k}}) − 1 .

PROOF: Let T_{J_{k}} be L_{j_{k+1}} + L(J_{k+1}) ≥ β and T_{J_{k+1}} be L(J_{k+1}) ≥ β′. We need to show that

β ≥ β′ ≥ β − 1.
[a] β ≥ β′ :

We know that L(J_{k+1}) ≥ β′ dominates L_{j_{k+1}} + L(J_{k+1}) ≥ β′. Since L_{j_{k+1}} + L(J_{k+1}) ≥ β is a strongest extended clause, we have β ≥ β′.

[b] β′ ≥ β − 1 : We know that L_{j_{k+1}} + L(J_{k+1}) ≥ β dominates its reduction L(J_{k+1}) ≥ β − 1. Because L(J_{k+1}) ≥ β′ is a strongest extended clause, we have β′ ≥ β − 1. ⊓ ⊔

Therefore the degree of the strongest extended clauses along a path from the root at each step either decreases by 1 or stays equal. We conclude that the following condition holds for all J_{l} ⊂ J_{k}.

|J_{k}| − |J_{l}| ≥ deg(T_{J_{l}}) − deg(T_{J_{k}})  (13)

Lemma 4.2 Let T (J_{k}) be c_{j_{k+1}}L_{j_{k+1}} + ∑_{i=1}^{n−(k+1)} c_{j′_{i}}L_{j′_{i}} ≥ d′ + c_{j_{k+1}}. W.l.o.g. assume that c_{j′_{p}} ≥ c_{j′_{q}} for all 1 ≤ p < q ≤ n − (k + 1). Let deg(T_{J_{k}}) be β and deg(T_{J_{k+1}}) be β′. If c_{j_{k+1}} ≥ c_{j′_{β′}} then β′ + 1 = β.

PROOF: The strict reduction T (J_{k+1}) of T (J_{k}) is ∑_{i=1}^{n−(k+1)} c_{j′_{i}}L_{j′_{i}} ≥ d′. From (10) in Prop. 3.2 we know that

∑_{i=1}^{β′−1} c_{j′_{i}} < d′ ≤ ∑_{i=1}^{β′} c_{j′_{i}} .

By adding c_{j_{k+1}} to the left inequality, we derive

c_{j_{k+1}} + ∑_{i=1}^{β′−1} c_{j′_{i}} < d′ + c_{j_{k+1}} .  (14)

According to Prop. 3.2, β is the smallest number of the largest coefficients such that the sum of the largest coefficients is greater than the right-hand side d′ + c_{j_{k+1}}. From c_{j_{k+1}} ≥ c_{j′_{β′}} and (14) we know that c_{j_{k+1}} is one of the coefficients of this sum, and therefore β > β′. By Lemma 4.1 we have β ≤ β′ + 1, and therefore β′ + 1 = β. ⊓ ⊔

Example 4.3 Let the strict reduction T (J_{k+1}) be

6 · L_{1} + 5 · L_{2} + 4 · L_{3} + 3 · L_{4} ≥ 12 .

Its strongest extended clause is

L_{1} + L_{2} + L_{3} + L_{4} ≥ 3

with degree 3, because 6 + 5 < 12 ≤ 6 + 5 + 4. Let c_{i}L_{i} be the product that has been eliminated, that is the label of the father node is

c_{i} · L_{i} + 6 · L_{1} + 5 · L_{2} + 4 · L_{3} + 3 · L_{4} ≥ 12 + c_{i}

and its strongest extended clause is

L_{i} + L_{1} + L_{2} + L_{3} + L_{4} ≥ β.

By Lemma 4.2 we know that if c_{i} ≥ 4 then β = 4. Suppose that c_{i} = 4; then condition (10) becomes 6 + 5 + 4 < 16 ≤ 6 + 5 + 4 + 4 and as expected the degree β is 4. Note that if c_{i} = 3 then β is still 4, that is the converse in Lemma 4.2 does not necessarily hold.

We now give a complete redundancy criterion for SCP(cL ≥ d) = T_{∅}, which is also a sufficient redundancy criterion for all strongest extended clauses.

Lemma 4.4 T_{∅} is redundant if and only if deg(T_{∅}) = deg(T_{{n}}).

PROOF: Let T_{∅} be L ≥ β, let L′ be L \ {L_{n}} and let T_{{n}} be L′ ≥ β′. Note that c_{n} ≤ c_{i} for all 1 ≤ i ≤ n.

⇐: Since β = β′, we know that L′ ≥ β dominates L ≥ β because L′ ⊂ L. Hence L ≥ β is redundant.

R

B  C

A

Figure 2: Redundancy caused by an extended clause in the subgraph

⇒: Suppose that L ≥ β is redundant. Then there exists L′′ ≥ β′′ in SCP(SRed(cL ≥ d)) that dominates L ≥ β, and thus β′′ ≥ β. Since L′′ ≥ β′′ is a strongest extended clause of a strict reduction of cL ≥ d, we have by Lemma 4.1 that β ≥ β′′ and therefore β = β′′. Because the degree of the strongest extended clauses along a path always decreases by 1 or stays equal, see (13), and since L′′ ⊂ L, we know that all strongest extended clauses along the path from the root to the node with strongest extended clause L′′ ≥ β have the degree β. Especially for a direct son of the root we have a strongest extended clause L \ {L_{j}} ≥ β dominating L ≥ β. From Lemma 4.2 we know that the coefficient c_{j} of the eliminated literal L_{j} is smaller than c_{β−1}, because otherwise β′′ + 1 = β. From c_{j} < c_{β−1} we derive j ≥ β − 1, since cL ≥ d is in pseudo-Boolean normal form and therefore ∑_{i=1}^{β−1} c_{i} < d − c_{j}. Because c_{j} ≥ c_{n}, we have d − c_{j} ≤ d − c_{n} and therefore ∑_{i=1}^{β−1} c_{i} < d − c_{n}. But then β′ ≥ β, and because β′ is the degree of a strongest extended clause on a path from the root, we have β′ ≤ β and therefore β′ = β. ⊓ ⊔

Proposition 4.5 If T_{J_{k}} is dominated by T_{J_{l}} and J_{l} ⊃ J_{k}, then T_{J_{k+1}} := T_{J_{k}∪{j_{k+1}}} dominates T_{J_{k}}, where c_{j_{k+1}} ≤ c_{i} for all i ∈ \overline{J_{k}}.

PROOF: The proposition follows immediately from Lemma 4.4 if we view T (J_{k}) as an independent graph. ⊓ ⊔

With Prop. 4.5 we can decide whether T_{J_{k}} is dominated by an extended clause in a subgraph of the graph with root label T (J_{k}) by checking domination against one specific extended clause. In Fig. 2 Lemma 4.4 is illustrated. The graph corresponds to a part of the graph view of SCP(SRed(cL ≥ d)). Assume that the sons of each node are ordered such that the coefficient of the eliminated literal of a son node is greater than or equal to all the coefficients of the eliminated literals of its right neighbors. Now Lemma 4.4 says that there is an extended clause A under the extended clause R dominating R if and only if C dominates R. In the proof of Lemma 4.4 we show that if there is an A dominating R, then B is dominating R, from which we show that C is dominating R. The key idea is to show that the strongest extended clauses A,B, and C all have the same degree.

We now give a similar criterion for extended clauses lying on a path to T (J_{k}), and, as in Prop. 4.5, identify a single specific extended clause that needs to be considered.

Lemma 4.6 For J_{l} ⊂ J_{k} the extended clause T_{J_{k}} is dominated by T_{J_{l}} if and only if

|J_{k}| − |J_{l}| ≤ deg(T_{J_{l}}) − deg(T_{J_{k}}) .

PROOF: Because |{1, …, n}\J_{l}|−|{1, …, n}\J_{k}| = |J_{k}|−|J_{l}| the lemma follows immediately from Lemma 2.5. ⊓ ⊔

Lemma 4.7 If T_{J_{k+1}} is dominated by T_{J_{l}} where J_{l} ⊂ J_{k+1}, then T_{J_{k+1}\{j_{i}}} dominates T_{J_{k+1}} for all j_{i} ∈ J_{k+1} \ J_{l}.

PROOF: From (13) we have |J_{k+1}| − |J_{l}| ≥ deg(T_{J_{l}}) − deg(T_{J_{k+1}}) and from Lemma 4.6 we have |J_{k+1}| − |J_{l}| ≤ deg(T_{J_{l}}) − deg(T_{J_{k+1}}), therefore we know that |J_{k+1}| − |J_{l}| = deg(T_{J_{l}}) − deg(T_{J_{k+1}}). Since in this case the degree of all extended clauses on a path from T_{J_{l}} to T_{J_{k+1}} decreases always by one, we have that the degree of all direct fathers, T_{J_{k+1}\{j_{i}}} for all j_{i} ∈ J_{k+1} \ J_{l}, is the degree of T_{J_{k+1}} plus one. ⊓ ⊔

We identify similar to Proposition 4.5 a single specific extended clause that needs to be tested for application of Lemma 4.6.

Proposition 4.8 If T_{J_{k+1}} is dominated by T_{J_{l}} where J_{l} ⊂ J_{k+1}, then there exists J_{k+1} \ {j_{max}} such that T_{J_{k+1}} \ {j_{max}} dominates T_{J_{k+1}} and c_{j_{max}} ≥ c_{j_{i}} for all 1 ≤ i ≤ k + 1.

PROOF: Let us consider a specific path H_{k+1} := h_{1} … h_{k+1} from the root to T (J_{k+1}) where c_{h_{1}} ≤ ⋯ ≤ c_{h_{k+1}} = c_{j_{max}} and h_{k+1} = j_{max}, i.e. always the smallest coefficient becomes eliminated next. For all direct fathers of T (J_{k+1}) the coefficient of the literal that becomes eliminated is therefore less than or equal to c_{h_{k+1}}. Because of Lemma 4.7 we have a strict reduction

R := ∑_{i∈\overline{J_{k+1}}} c_{i}L_{i} + c_{x}L_{x} ≥ d + c_{x} − ∑_{i∈J_{k+1}} c_{i} ,

where x ∈ J_{l} and deg(SCP(R)) = β + 1. Using our fixed path H_{k+1}, we know that there is another strict reduction

H := ∑_{i∈\overline{J_{k+1}}} c_{i}L_{i} + c_{j_{max}}L_{j_{max}} ≥ d + c_{j_{max}} − ∑_{i∈J_{k+1}} c_{i} .

We now show that deg(SCP(R)) = deg(SCP(H)) = β + 1. Suppose that c_{j_{max}} ≥ c_{j′_{β}}. As in Lemma 4.2 we then derive that deg(SCP(H)) > β, hence deg(SCP(H)) = β + 1. Now suppose that c_{j_{max}} < c_{j′_{β}}. Since c_{j_{max}} ≥ c_{x}, we have c_{x} < c_{j′_{β}}. Because deg(SCP(R)) = β + 1, we have

∑_{1≤i≤β} c_{j′_{i}} < d + c_{x} − ∑_{i∈J_{k+1}} c_{i} .

With c_{j_{max}} ≥ c_{x} we get

∑_{1≤i≤β} c_{j′_{i}} < d + c_{j_{max}} − ∑_{i∈J_{k+1}} c_{i} ,

which also implies deg(SCP(H)) > β and therefore deg(SCP(H)) = β + 1. Let J_{k+1} \ {j_{max}} be {h_{1}, …, h_{k}}, then the proposition follows. ⊓ ⊔

I

A

B  C

R

Figure 3: Redundancy caused by an extended clause above in the graph

Consider the illustration of Prop. 4.8 in Fig. 3. Prop. 4.8 says that there is an A dominating R if and only if C dominates R. In the graph we assume that the fathers of each node are ordered such that the coefficient of the eliminated literal to come from a father node to a son node is greater than or equal to all the coefficients of the eliminated literals of its left neighbors. In the proof of Prop. 4.8 we show first that if A dominates R, then there is a B dominating R, and that all degrees along a path from R to A decrease by one. The double line corresponds to the specific path H_{k+1}, and we show that C, lying on this path, has the same degree as B and therefore dominates R.

We combine now Prop. 4.5 and Prop. 4.8 to a complete redundancy criterion.

Theorem 4.9 The strongest extended clause T_{J_{k+1}} is redundant if and only if

[a] T_{J_{k+2}} dominates T_{J_{k+1}} where c_{j_{k+2}} ≤ c_{i} for all i ∈ \overline{J_{k+1}}, or

[b] T_{J_{k+1}\{j_{max}}} dominates T_{J_{k+1}} where c_{j_{max}} ≥ c_{i} for all i ∈ J_{k+1}.

PROOF:

⇐: [a] from Prop. 4.5 and [b] from Prop. 4.8.

⇒: Suppose that neither [a] nor [b] is satisfied for T_{J_{k+1}}, but T_{J_{k+1}} is redundant. Then there is a strongest extended clause L′′ ≥ β that dominates T_{J_{k+1}} := L′ ≥ β′ and L′′ ≠ L′. From Prop. 4.8 we have L′′ ⊅ L′ and from Prop. 4.5 we have L′′ ⊄ L′. Therefore there is at least one literal in L′′ that is not in L′. Following the proof of Lemma 2.5 a valid reduction of L′′ ≥ β is L′′ ∩ L′ ≥ β − |L′′ \ L′|, which also dominates L′ ≥ β′. The strongest extended clause containing exactly the literals in L′′ ∩ L′ therefore dominates L ≥ β′ and hence T_{J_{k+1}}. Because L′′ ∩ L′ ⊂ L′′ (L′′ \ L′ ≠ ∅) Prop. 4.5 applies and therefore condition [a]. ⊓ ⊔

For illustrating statement [b] of Theorem 4.9 we look again at Fig. 2. We have shown that if there is an X dominating R and X is not on a path also including R then we will find and A in the subgraph under X such that Prop. 4.5 applies.

By Theorem 4.9 we can decide redundancy of a strongest extended clause by investigating exactly 2 other strongest extended clauses. We end this section with an example.

Example 4.10 Let us transform the pseudo-Boolean inequality

5 · L_{1} + 4 · L_{2} + 3 · L_{3} + 2 · L_{4} + 1 · L_{5} ≥ 11 .

Its strongest extended clause is

L_{1} + L_{2} + L_{3} + L_{4} + L_{5} ≥ 3 .

Let us compute the strict reductions T ({i}) and their corresponding strongest extended clauses T_{{i}}.

\begin{matrix}i & T (\{i\}) & T_{\{i\}} \\ 1 & 4 · L_{2} + 3 · L_{3} + 2 · L_{4} + 1 · L_{5} ≥ 6 & L_{2} + L_{3} + L_{4} + L_{5} ≥ 2 \\ 2 & 5 · L_{1} + 3 · L_{3} + 2 · L_{4} + 1 · L_{5} ≥ 7 & L_{1} + L_{3} + L_{4} + L_{5} ≥ 2 \\ 3 & 5 · L_{1} + 4 · L_{2} + 2 · L_{4} + 1 · L_{5} ≥ 8 & L_{1} + L_{2} + L_{4} + L_{5} ≥ 2 \\ 4 & 5 · L_{1} + 4 · L_{2} + 3 · L_{3} + 1 · L_{5} ≥ 9 & L_{1} + L_{2} + L_{3} + L_{5} ≥ 2 \\ 5 & 5 · L_{1} + 4 · L_{2} + 3 · L_{3} + 2 · L_{4} ≥ 10 & L_{1} + L_{2} + L_{3} + L_{4} ≥ 3 \end{matrix}

We see that T_{{5}} dominates T_{∅} (Theorem 4.9[a] ⇐) and that T_{{1}}, T_{{2}}, T_{{3}}, T_{{4}} are dominated by T_{∅} (Theorem 4.9[b] ⇐). We calculate T_{{4,5}} = L_{1} + L_{2} + L_{3} ≥ 2 and conclude that T_{{5}} is not redundant(Theorem 4.9; completeness). Proceeding further we arrive at the set of non redundant extended clauses as in Example 3.7.

5 Implementation

We sketch an implementation of the transformation algorithm using the strong redundancy criteria presented in Sect. 4.

Theorem 4.9 is a complete redundancy criterion for a strongest extended clause that reduces the number of needed domination checks to 2. We denote by β′ = deg(T_{J_{k+2}}) the degree of the strongest extended clause of the specific father of T (J_{k+1}) and with β′′ = deg(T_{J_{k}\{j_{max}}}) the degree of the strongest extended clause of the specific son of T (J_{k+1}). The degree of the extended clause for which we want to check redundancy is denoted by β = deg(T_{J_{k+1}}). From Theorem 4.9 we see immediately that T_{J_{k+1}} is redundant iff

β′ − 1 = β  or  β = β′′ .

Hence, for deciding redundancy of a strongest extended clause only the degrees of two strongest extended clauses (the specific father and the specific son) are needed.

We describe an algorithm that computes from a given linear pseudo-Boolean inequality cL ≥ d in normal form a set of equivalent non redundant extended clauses. We assume that ∑_{i=1}^{n} c_{i} ≥ d, since otherwise cL ≥ d is unsatisfiable. We also assume that ∑_{i=2}^{n} c_{i} ≥ d, since otherwise α(L_{1}) = 1 for all α ∈ Ext(cL ≥ d), and we can consider the simpler problem of transforming

∑_{i=2}^{n} c_{i}L_{i} ≥ d − c_{1} .

In the following we assume that cL ≥ d is satisfiable, in pseudo-Boolean normal form and that for every literal L_{i} ∈ L there are assignments α_{1}, α_{2} ∈ Ext(cL ≥ d) such that α_{1}(L_{i}) = 1 − α_{2}(L_{i}). Note that for all generated strongest extended clauses L′ ≥ β we have |L′| > β.

In the program fragments we use the following nonstandard notation. Given a pseudo-Boolean term cL we select the last (resp. first) coefficient/literal pair c_{l}L_{l} and the remaining term c′L′ by cL = c′L′ + c_{l}L_{l} (resp. cL = c_{l}L_{l} + c′L′). We give first the procedure get beta calculating the degree β of the strongest extended clause of its argument, a strict reduction, and β′′, the degree of the strongest extended clause of the strict reduction, where we have eliminated the literal with the smallest coefficient. The right-hand side β′′ then is the degree of the strongest extended clause of the specific son node as in Prop. 4.8.

      get beta(cL ≥ d)

i, β, sum, prevsum := 1, 0, 0, 0

while sum < d

cL = c_{l}L_{l} + c′L′
prevsum := sum
sum, β, cL := sum + c_{l}, β + 1, c′L′

endwhile

while cL = c_{l}L_{l} + c′L′

cL := c′L′

endwhile

(* c_{l} is the smallest coefficient *)

β′′ := if prevsum ≥ d − c_{l} then β − 1 else β endif return (β, β′′)

      end get beta

We obtain β by summing up the coefficients according to (9), and count the number of added coefficients until we reach the right-hand side. Since the specific son is the one where the literal with the smallest coefficient has been eliminated, this coefficient can not be part of the sum. Note that ∑_{i=2}^{n} c_{i} ≥ d. Therefore the degree of the specific son is one smaller if and only if the actual sum minus the last added coefficient, that is the previous sum, is already greater than or equal to the right-hand side d − c_{l} of the specific son. We see that the overhead for calculating β′′ is not high. In the actual implementation we store the value of the smallest coefficient for each strict reduction and so avoid searching for it.

For an efficient implementation we must not generate the whole graph. Instead we implicitly visit the nodes, that is the strict reductions, in a specific order such that for each strict reduction the redundancy test becomes trivial. We assure that each strict reduction T (J_{k+1}) is visited only once through the path H_{k+1} (see Proof of Prop. 4.8). This is achieved by splitting the pseudo-Boolean term (the left-hand side of the pseudo-Boolean inequality) into two parts, one containing the literals that must be eliminated and one part containing the literals that need not be eliminated. We eliminate literals having a smaller coefficient first and then forbid further reduction on these literals by moving them from the first part to the second part. We thus make sure that the strict reductions are visited only through the specific path. We give a recursive procedure transform generating each possible strict reduction only once and adding its strongest extended clause to the output set if and only it is not redundant. The procedure transform has as parameters a pseudo-Boolean inequality, which is split into the two parts and the right-hand side, and the right-hand side β′ of the strongest extended clause of the father in the path H_{k+1}.

transform(cL, ĉL̂, d, β′)

S := ∅

(β, β′′) = get beta(cL + ĉL̂ ≥ d)

if β′ − 1 ≠ β ∧ β′′ ≠ β then (* not redundant *)

S := S ∪ {L + L̂ ≥ β} (* add the non redundant clause to the output set *) endif (* As long as cL contains elements and there are valid strict reductions *) while c′L′ + c_{l}L_{l} = cL ∧ d − c_{l} ≥ 1 (* eliminate c_{l}L_{l} *)

S := S ∪ transform(c′L′, ĉL̂, d − c_{l}, β)

ĉL̂ := ĉL̂ + c_{l}L_{l} (* forbid further reduction on L_{l} *)

cL := c′L′

endwhile return S

      end transform

Note that in the while-loop we select first the product with the smallest coefficient and then forbid further reduction on it by moving the product to the second part. The set of all non redundant strongest extended clauses equivalent to the pseudo-Boolean inequality cL ≥ d then is transform(cL, ∅, d, 0). We finish this section with some examples.

Example 5.1 The examples are taken from [NW88].

[a] [NW88, page 266] Let cL ≥ d be

79 · X_{1} + 53 · X_{2} + 53 · X_{3} + 45 · X_{4} + 45 · X_{5} ≤ 178 .

The pseudo-Boolean normal form of cL ≥ d is

79 · \overline{X_{1}} + 53 · \overline{X_{2}} + 53 · \overline{X_{3}} + 45 · \overline{X_{4}} + 45 · \overline{X_{5}} ≥ 97 .

The equivalent set of extended clauses is

\begin{aligned}\{\overline{X_{1}} + \overline{X_{2}} + \overline{X_{3}} + \overline{X_{4}} + \overline{X_{5}} & ≥ & 2, \\ \overline{X_{1}} + \overline{X_{2}} + \overline{X_{3}} & ≥ & 1\} . \end{aligned}

[b] [NW88, page 460] Let cL ≥ d be

774 · X_{1} + 76 · X_{2} + 22 · X_{3} + 42 · X_{4} + 21 · X_{5} + 760 · X_{6} + 818 · X_{7} + 62 · X_{8} + 785 · X_{9} ≤ 1500 .

The transformation procedure generates the single extended clause

\overline{X_{1}} + \overline{X_{6}} + \overline{X_{7}} + \overline{X_{9}} ≥ 3

which is equivalent to cL ≥ d.

[c] [NW88, page465] Let cL ≥ d be

300 · X_{3} + 300 · X_{4} + 285 · X_{5} + 285 · X_{6} + 265 · X_{8} + 265 · X_{9} + 230 · X_{12}+ 230 · X_{13} + 190 · X_{14} + 200 · X_{22} + 400 · X_{23} + 200 · X_{24} + 400 · X_{25}+

200 · X_{26} + 400 · X_{27} + 200 · X_{28} + 400 · X_{29} + 200 · X_{30} + 400 · X_{31}  ≤ 2700

which is a linear 0-1 inequality from the constraint set of a 0-1 integer programming problem. Transforming cL ≥ d generates 4282 non redundant strongest extended clauses. They have been calculated with a PROLOG-implementation of the algorithm in 4.8 seconds cpu-time on a SPARC-10/31. All 15 inequalities of the problem produce together 8710 extended clauses where 749 extended clauses are dominated by extended clauses generated from another inequality such that 7961 extended clauses remain. Note that the number of non redundant classical clauses that are equivalent to cL ≥ d, as needed in [GH71], is 117520.

Example 5.1[c] demonstrates the advantage of extended clauses versus classical clauses. Because of the large number of classical clauses needed to represent a pseudo-Boolean inequality, clausal satisfiability methods can not be applied to typical 0-1 integer programming problems [GG80]. The reformulation of a pseudo-Boolean inequality as a set of extended clauses is more likely to be applicable on general 0-1 problems because of its compact representation. In the next section we give an even more compact representation of pseudo-Boolean inequalities and extended clauses that allows to speed up the computation, and brings even larger problems into the scope of this symbolic method.

6 Symmetries

We introduce the concept of symmetries for a set of literals w.r.t. to a pseudo-Boolean inequality and then define the compact set representation of pseudo-Boolean inequalities and extended clauses. The more compact formulation helps to avoid redundant computation in the transformation method.

Let us transform the pseudo-Boolean inequality

5 · A + 5 · B + 4 · C + 3 · D + 3 · E + 3 · F ≥ 12 .  (15)

Three strict reductions of (15) are for example

5 · A + 5 · B + 4 · C + 3 · E + 3 · F ≥ 9  (16)
5 · A + 5 · B + 4 · C + 3 · D + 3 · F ≥ 9  (17)
5 · A + 5 · B + 4 · C + 3 · D + 3 · E ≥ 9  (18)

obtained by eliminating D for (16), E for (17) and F for (18). Note that these three strict reductions are identical except for the names of the last two literals. Therefore these three extended clauses yield exactly the same set of non redundant extended clauses except for the names of the literals. We say that D, E and F are symmetric in (15). In the following we describe how to avoid redundant computations occurring while eliminating symmetric literals. For that we first define a compact representation of a set of pseudo-Boolean inequalities.

Definition 6.1 For all 1 ≤ i < j ≤ m let S_{i} and S_{j} be sets of literals such that Var(L_{l}) ≠ Var(L_{k}) for all L_{l} ∈ S_{i} and L_{k} ∈ S_{j}. We say that

∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d ,  (19)

where d ≥ c_{1} > ⋯ > c_{m} ≥ 1 and 1 ≤ k_{i} ≤ |S_{i}| for all 1 ≤ i ≤ m, is a compact pseudo-Boolean inequality set of a set of pseudo-Boolean inequalities. The compact pseudo-Boolean inequality set (19) represents the set of all pseudo-Boolean inequalities

\{cL ≥ d | \begin{matrix}|L| = ∑_{i=1}^{m} k_{i} and \\ for all c_{l}L_{l} ∈ cL there is an S_{i} such that L_{l} ∈ S_{i} and c_{l} = c_{i} and \\ |S_{i} ∩ L| = k_{i} for all 1 ≤ i ≤ m . \end{matrix} \}  (20)

In other words, all pseudo-Boolean inequalities where from each set of literals S_{i} exactly k_{i} occur in the pseudo-Boolean inequality with coefficient c_{i}. We say we expand a compact pseudo-Boolean inequality set if we replace ∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d by (20) and define expand(∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d) := (20). For a set S of compact pseudo-Boolean inequality sets we define expand(S) := ⋃_{I∈S} expand(I).

Example 6.2 We can represent the single pseudo-Boolean inequality (15) by the compact pseudo-Boolean inequality set

5 · {A, B}^{2} + 4 · {C}^{1} + 3 · {D, E, F }^{3} ≥ 12 .

The three strict reductions (16), (17) and (18) can be represented by

5 · {A, B}^{2} + 4 · {C}^{1} + 3 · {D, E, F }^{2} ≥ 9 .

Note that every pseudo-Boolean inequality can be represented as compact pseudo-Boolean inequality set where k_{i} = |S_{i}|.

The compact pseudo-Boolean inequality set representation is the key to exploit the symmetry property of literals in a pseudo-Boolean inequality. The possible strict reductions that lead to an identical search can now be represented by a single compact pseudo-Boolean inequality set. We define similar to Def. 6.1 a compact set representation for extended clauses.

Definition 6.3 For all 1 ≤ i < j ≤ m let S_{i} and S_{j} be sets of literals such that Var(L_{l}) ≠ Var(L_{k}) for all L_{l} ∈ S_{i} and L_{k} ∈ S_{j}. We say that

∑_{i=1}^{m} S_{i}^{k_{i}} ≥ β ,  (21)

where 1 ≤ k_{i} ≤ |S_{i}| for all 1 ≤ i ≤ m, is a compact extended clause set of a set of extended clauses. The compact extended clause set (21) represents the set of all extended clauses

\{L ≥ β | \begin{matrix}|L| = ∑_{i=1}^{m} k_{i} and \\ |S_{i} ∩ L| = k_{i} for all 1 ≤ i ≤ m . \end{matrix} \}  (22)

We say we expand a compact extended clause set if we replace ∑_{i=1}^{m} S_{i}^{k_{i}} ≥ β by the set of extended clauses (22) and define expand(∑_{i=1}^{m} S_{i}^{k_{i}} ≥ β) := (22). For a set S of compact extended clause sets we define expand(S) := ⋃_{I∈S} expand(I).

We generalize now the generation of strongest extended clauses of Prop. 3.2. For a compact pseudo-Boolean inequality set ∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d the corresponding strongest compact extended clause set is

∑_{i=1}^{m} S_{i}^{k_{i}} ≥ β  (23)

where

∑_{i=1}^{β−1} c_{i} · k_{i} < d ≤ ∑_{i=1}^{β} c_{i} · k_{i} .  (24)

Note that (24) corresponds to (9) but takes into account the compact set representation. We denote by SCP′(∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d) := ∑_{i=1}^{m} S_{i}^{k_{i}} ≥ β the strongest compact extended clause set of a compact pseudo-Boolean inequality set. Obviously for each pseudo-Boolean inequality in expand(∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d) there is a corresponding strongest extended clause in expand(∑_{i=1}^{m} S_{i}^{k_{i}} ≥ β) and we have

expand(SCP′(∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d)) = SCP(expand(∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d)) .

A compact strict reduction of a compact pseudo-Boolean inequality set ∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d is

∑_{i=1}^{m} c_{i}S_{i}^{k′_{i}} ≥ d − ∑_{i=1}^{m} c_{i} · (k_{i} − k′_{i})

where either k′_{i} = k_{i} or k′_{i} = k_{i} − 1 for all 1 ≤ i ≤ m. Note that c_{i}S_{i}^{k′_{i}} disappears if k′_{i} = 0. We denote by SRed′(∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d) the set of all compact strict reductions of a compact pseudo-Boolean inequality set. Obviously we have

expand(SRed′(∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d)) = SRed(expand(∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d)) .

The transformation method using compact sets is now straightforward. For a compact pseudo-Boolean inequality set ∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d we have

expand(SCP′(SRed′(∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d))) = SCP(SRed(expand(∑_{i=1}^{m} c_{i}S_{i}^{k_{i}} ≥ d))) .

The practical advantage is that we avoid redundant computation of identical strict reductions modulo literal renaming because they are grouped together in a single compact pseudo-Boolean inequality set. Generalizing Theorem 4.9 for compact sets is immediate and an implementation of the transformation method using compact sets is similar to the implementation sketched in Sect. 5.

Example 6.4 [a] Let us transform the pseudo-Boolean inequality

5 · A + 5 · B + 4 · C + 3 · D + 3 · E + 3 · F ≥ 12

then 32 strict reductions need to be considered. If we transform the equivalent compact pseudo-Boolean inequality set

5 · {A, B}^{2} + 4 · {C}^{1} + 3 · {D, E, F }^{3} ≥ 12

then only 11 compact strict reductions are possible. The set of equivalent strongest extended clause is

\begin{aligned}\{A + B + C + D + E + F & ≥ & 3, \\ A + B + C + D & ≥ & 2, \\ A + B + C + E & ≥ & 2, \\ A + B + C + F & ≥ & 2\} . \end{aligned}

The compact variant generates

\begin{aligned}\{\{A\}^{1} + \{B\}^{1} + \{C\}^{1} + \{D\}^{1} + \{E\}^{1} + \{F \}^{1} & ≥ & 3, \\ \{A\}^{1} + \{B\}^{1} + \{C\}^{1} + \{D, E, F \}^{1} & ≥ & 2\} . \end{aligned}

So by exploiting the symmetry property of literals we avoid redundant computation and obtain a more compact result.

[b] The pseudo-Boolean inequality of Example 5.1[c] generates 4282 extended clauses in 4.8 seconds cpu time on a SPARC-10/31. The implementation using symmetries takes 0.77 seconds cpu time for generating the 4282 extended clause where 0.49 seconds are used to expand the 253 compact non redundant extended clause sets. The transformation itself takes only 0.18 seconds.

The very compact representation of Example 6.4[b] suggests to further investigate the compact extended clause set representation of extended clauses. If we can find efficient symbolic solution methods working directly on the compact representation even large 0-1 problems are in the scope of these methods. This issue will be investigated in the future.

7 Detection of Fixed Literals

We present a method for checking whether a set of pseudo-Boolean inequalities S dominates an extended clause L_{i} ≥ 1 for some literal L_{i}. For such an L_{i} we then have α(L_{i}) = 1 for all assignments α ∈ Ext(S), that is the literal L_{i} is fixed and S can be simplified to a set of pseudo-Boolean inequalities S′ not containing L_{i} nor \overline{L_{i}} such that

Ext(S) = Ext(S′ ∪ {L_{i} ≥ 1}) .

A similar simplification is possible if several literals need to be fixed. Let L be a set of literals such that S dominates L_{i} ≥ 1 for all L_{i} ∈ L. We can then simplify S to a set of pseudo-Boolean inequalities S′ not containing L_{i} nor \overline{L_{i}} for all L_{i} ∈ L such that

Ext(S) = Ext(S′ ∪ {L ≥ |L|}) .

Note that L ≥ |L| dominates L_{i} ≥ 1 for all L_{i} ∈ L. We show how to find some of the fixed literals in L and how to build the simplified set of pseudo-Boolean inequalities S′.

We know that S dominates L_{i} ≥ 1 if and only if S∪\{\overline{L_{i}} ≥ 1\} is unsatisfiable. Obviously, checking whether S ∪ \{\overline{L_{i}} ≥ 1\} is unsatisfiable is in general NP-complete. We present an approximation of the unsatisfiability test based on the idea of unit relaxation [Hoo88, Hoo89]. We first briefly recall unit resolution for classical clauses and then generalize the concept to pseudo-Boolean inequalities.

Classical clauses are pseudo-Boolean inequalities where all coefficients and the right-hand side are 1. A classical clause L_{i} ≥ 1 is called unit clause and its literal L_{i} is called unit literal. Application of resolution restricted to the case that at least one father is a unit clause is called unit resolution or clausal chaining. The resolvent of a unit clause L_{i} ≥ 1 and a classical clause L ≥ 1 is defined by

ures(L_{i}, L ≥ 1) := \{ \begin{matrix}L \ \{\overline{L_{i}}\} ≥ 1 & if & \overline{L_{i}} ∈ L \\ ⊤ & if & L_{i} ∈ L \\ L ≥ 1 & otherwise . \end{matrix}

Because {ures(L_{i}, L ≥ 1), L_{i} ≥ 1} dominates L ≥ 1 we can replace L ≥ 1 by ures(L_{i}, L ≥ 1). For a set of classical clauses S we define

ures(L_{i}, S) := {ures(L_{i}, L ≥ 1) | L ≥ 1 ∈ S and ures(L_{i}, L ≥ 1) ≠ ⊤} .

Note that there are no tautologies ⊤ in ures(L_{i}, S). We derive that

Ext(S) = Ext(ures(L_{i}, S) ∪ {L_{i} ≥ 1})

if S dominates L_{i} ≥ 1. Unit resolution for a set of classical clauses S can be described by the procedure ur.

ur(S)

U := ∅

while ∃ L_{i} ≥ 1 ∈ S

S := ures(L_{i}, S)
U := U ∪ {L_{i}}

endwhile return S

end ur

We denote by ul(S) := U the set of unit literals L_{i} of the unit clauses L_{i} ≥ 1 detected after applying ur(S). If ur(S) contains the the empty clause □, then S is unsatisfiable and we say the unit relaxation of S is unsatisfiable. Note that the unit relaxation of a set of classical clauses S is satisfiable if and only if the linear programming relaxation of S is satisfiable [Hoo88]. We know that S is satisfiable if and only if ur(S) is satisfiable. Each satisfying assignment α of S is a satisfying assignment of ur(S) and α(L_{i}) = 1 for all L_{i} ∈ ul(S), therefore

Ext(S) = Ext(ur(S) ∪ {L_{i} ≥ 1 | L_{i} ∈ ul(S)}) .

For generalizing the concept of unit relaxation to arbitrary linear pseudo-Boolean inequalities we need to know whether a pseudo-Boolean inequality dominates L_{i} ≥ 1 for some L_{i}, that is whether there is a literal L_{i} that can be fixed.

Lemma 7.1 A pseudo-Boolean inequality cL ≥ d dominates L_{i} ≥ 1 if and only if

c_{i}L_{i} ∈ cL  and  s(c) − c_{i} < d ,

where s(c) denotes the sum over all coefficients of c.

PROOF: Let c′L′ be cL\{c_{i}L_{i}} and let α be in Ext(cL ≥ d). Then α(c_{i}L_{i})+α(c′L′) ≥ d. Note that s(c) − c_{i} = s(c′). Suppose that s(c′) < d. Since α(c′L′) ≤ s(c′) < d we have α(c_{i}L_{i}) > 0 and therefore α(L_{i}) = 1. Suppose that s(c′) ≥ d then each α such that α(L′) = |L′| and α(L_{i}) = 0 is in Ext(cL ≥ d). ⊓ ⊔

If a pseudo-Boolean inequality cL ≥ d dominates L_{i} ≥ 1 we call L_{i} unit literal w.r.t. cL ≥ d.

Lemma 7.2 If a pseudo-Boolean inequality cL ≥ d dominates L_{i} ≥ 1 where c_{i}L_{i} ∈ cL then cL ≥ d dominates L_{j} ≥ 1 for all c_{j}L_{j} ∈ cL where c_{j} ≥ c_{i}.

PROOF: If s(c)−c_{i} < d then s(c)−c_{j} < d because c_{j} ≥ c_{i} and therefore Lemma 7.1 applies. But then cL ≥ d dominates L_{j} ≥ 1. ⊓ ⊔

By Lemma 7.2 we see that a pseudo-Boolean inequality cL ≥ d dominates L_{i} ≥ 1 for some L_{i} if and only if cL ≥ d dominates L_{j} ≥ 1 where L_{j} is a literal having the largest coefficient in cL ≥ d. We define

fixed(cL ≥ d) := \{ \begin{matrix}L_{j} & if s(c) − c_{j} < d where c_{j}L_{j} ∈ cL and c_{j} ≥ c_{i} for all c_{i} ∈ c, \\ ⊥ & otherwise. \end{matrix}

If there are several possibilities for L_{j} then any of them can be chosen. We know then that fixed(cL ≥ d) = L_{j} if cL ≥ d dominates L_{j} ≥ 1. If fixed(cL ≥ d) = ⊥ we know that there is no literal L_{j} such that cL ≥ d dominates L_{j} ≥ 1. Given a unit literal L_{i} we can simplify a pseudo-Boolean inequality cL ≥ d. We define

fix(L_{i}, cL ≥ d) := \{ \begin{matrix}⊤ & if & d − c_{i} ≤ 0 and c_{i}L_{i} ∈ cL \\ cL \ c_{i}L_{i} ≥ d − c_{i} & if & d − c_{i} > 0 and c_{i}L_{i} ∈ cL \\ □ & if & s(c) − c_{i} < d and c_{i}\overline{L_{i}} ∈ cL \\ cL \ c_{i}\overline{L_{i}} ≥ d & if & s(c) − c_{i} ≥ d and c_{i}\overline{L_{i}} ∈ cL \\ cL ≥ d & if & neither L_{i} nor \overline{L_{i}} in L; \end{matrix}

which formally defines the operation of replacing the literal L_{i} by 1 and bringing the constant c_{i} to the right-hand side. Special cases arise when the inequality becomes tautologous (⊤) or unsatisfiable (□) after fixing.

We derive that

Ext({cL ≥ d, L_{i} ≥ 1}) = Ext({fix(L_{i}, cL ≥ d), L_{i} ≥ 1}) .  (25)

Note that fixing a literal L_{i} in a pseudo-Boolean inequality cL ≥ d may only produce a tautology if L_{i} ∈ L and may only produce □ if \overline{L_{i}} ∈ L. Given a set of pseudo-Boolean inequalities S we denote by fix(L_{i}, S) the set of all pseudo-Boolean inequalities fix(L_{i}, cL ≥ d) ≠ ⊤ where cL ≥ d in S. Note that no tautologies are in fix(L_{i}, S). We present now the generalization pbur (pseudoboolean unit resolution) of the unit resolution procedure ur for a set S of linear pseudo-Boolean inequalities.

      pbur(S)

U := ∅

while ∃ cL ≥ d ∈ S ∧ fixed(cL ≥ d) ≠⊥

S := fix(fixed(cL ≥ d), S)
U := U ∪ {fixed(cL ≥ d)}

endwhile return S

      end pbur

We denote by pbul(S) := U the set of all unit literals fixed(cL ≥ d) detected after applying pbur(S). Obviously S is satisfiable if and only if pbur(S) is satisfiable and each satisfying assignment α of S is a satisfying assignment of pbur(S) and α(L_{i}) = 1 for all L_{i} ∈ pbul(S). We say that the pseudo-Boolean unit relaxation of S is unsatisfiable if □ ∈ pbur(S). If S contains only classical clauses then obviously ur(S) = pbur(S) and therefore □ ∈ pbur(S) if and only if □ ∈ ur(S). If the pseudo-Boolean unit relaxation of S is unsatisfiable then the linear programming relaxation of S is unsatisfiable. The converse no longer holds. Consider for example

\{1 · A + 1 · B + 1 · C ≥ 2, 1 · \overline{A} + 1 · \overline{B} + 1 · \overline{C} ≥ 2\} .

Note that because of (25) we have in pbur as invariant of the while-loop that

Ext(S_{i} ∪ {U_{i} ≥ |U_{i}|}) = Ext(S_{i+1} ∪ {U_{i+1} ≥ |U_{i+1}|}) ,

where S_{i} resp. U_{i} represents the actual S resp. U in the i-th iteration. So for a set of pseudo-Boolean inequalities S we have

Ext(S) = Ext(pbur(S) ∪ {pbul(S) ≥ |pbul(S)|}) .  (26)

A set of literals that need to be fixed is the set of unit literals pbul(S). Pseudo-Boolean unit resolution is a procedure detecting this set of literals.

Example 7.3 Let S be

\begin{aligned}\{5 · A + 4 · B + 3 · C + 2 · D & ≥ & 10, \\ 8 · \overline{A} + 6 · D + 4 · E + 3 · F & ≥ & 8\} \end{aligned}

and let us follow a computation of pbur(S). We obtain first fixed(5·A+4·B+3·C+2·D ≥ 10) = A and simplify S to fix(A, S).

\begin{aligned}\{4 · B + 3 · C + 2 · D & ≥ & 5, \\ 6 · D + 4 · E + 3 · F & ≥ & 8\} \end{aligned}

We next have fix(6 · D + 4 · E + 3 · F ≥ 8) = D and obtain fix(D, fix(A, S)).

\begin{aligned}\{3 · B + 3 · C & ≥ & 3, \\ 2 · E + 2 · F & ≥ & 2\} \end{aligned}

Since now for all pseudo-Boolean inequalities fix returns ⊥ we have

Ext(S) = Ext({3 · B + 3 · C ≥ 3, 2 · E + 2 · F ≥ 2, A + D ≥ 2}) .

Transforming the remaining pseudo-Boolean inequalities is trivial and we obtain

Ext(S) = Ext({B + C ≥ 1, E + F ≥ 1, A + D ≥ 2}) .

When a pseudo-Boolean inequality has been simplified by fixing literals then transforming the simplified pseudo-Boolean inequality is simpler, that is fewer strongest extended clauses are generated.

We know that a set of pseudo-Boolean inequalities S dominates L_{i} ≥ 1 for some literal L_{i} if and only if (S ∪\{\overline{L_{i}} ≥ 1\}) is unsatisfiable. We approximate the unsatisfiability test by checking whether the unit relaxation of S ∪ \{\overline{L_{i}} ≥ 1\} is unsatisfiable, that is whether □ ∈ pbur(S ∪ \{\overline{L_{i}} ≥ 1\}). We get the procedure fixing that detects some of the literals L_{i} for which α(L_{i}) = 1 for all satisfying assignments α of a set of pseudo-Boolean inequalities S.

      fixing(S)

K := ∅

while ∃L_{i} : □ ∈ pbur(S ∪ \{\overline{L_{i}} ≥ 1\})

K := K ∪ pbul(S ∪ {L_{i} ≥ 1})
S := pbur(S ∪ {L_{i} ≥ 1})

endwhile return K

      end fixing

Note that S dominates fixing(S) ≥ |fixing(S)|. Let K be fixing(S) then

Ext(S) = Ext(pbur(S ∪ {K ≥ |K|}) ∪ {K ≥ |K|}) .

Note that fixing is a stronger procedure for detecting fixed literals of a set of pseudo-Boolean inequalities than pseudo-Boolean unit resolution and we have

                               fixing(S) ⊇ pbul(S) .

Example 7.4 Let S be

\begin{aligned}\{5 · A + 4 · B + 3 · C + 2 · D & ≥ & 7, \\ 3 · \overline{B} + 3 · D + 2 · \overline{C} & ≥ & 4\} \end{aligned}

then none of the two pseudo-Boolean inequalities dominates L_{i} ≥ 1 for some literal L_{i}. Let us apply fixing to S and start with calculating pbur(S ∪ \{\overline{A} ≥ 1\}). We first obtain fix(\overline{A}, S).

\begin{aligned}\{4 · B + 3 · C + 2 · D & ≥ & 7, \\ 3 · \overline{B} + 3 · D + 2 · \overline{C} & ≥ & 4\} \end{aligned}

Now fixed(4 · B + 3 · C + 2 · D ≥ 7) = B and we calculate fix(B,fix(\overline{A}, S)).

\begin{aligned}\{3 · C + 2 · D & ≥ & 3, \\ 3 · D + 2 · \overline{C} & ≥ & 4\} \end{aligned}

We next derive fixed(3 · C + 2 · D ≥ 3) = C and fix(C, fix(B, fix(\overline{A}, S))) gives

\begin{matrix}\{ & & ⊤, \\ 3 · D & ≥ & 4\} \end{matrix}

where 3 · D ≥ 4 is □. We conclude that S ∪ \{\overline{A} ≥ 1\} is unsatisfiable. Thus S dominates A ≥ 1 and we can replace S by fix(A, S) ∪ {A ≥ 1}.

\begin{aligned}\{2 · B + 2 · C + 2 · D & ≥ & 2, \\ 3 · \overline{B} + 3 · D + 2 · \overline{C} & ≥ & 4, \\ A & ≥ & 1\} . \end{aligned}

Note that 2 · B + 2 · C + 2 · D ≥ 2 is already normalized. There is no further literal L_{i} such that □ ∈ S′ ∪ \{\overline{L_{i}} ≥ 1\} and so fixing ends.

For example on the constraint set of a 0-1 integer optimization problem “air01” found on MI-PLIB [BBI92] fixing detects that 130 out of the 771 boolean variables have to be fixed. On the other side fixing is a rather costly process. Suppose that n variables occur in S then for a complete application of fixing we have to compute 2n unit resolutions if fixing detects no fixed literals.

8 Constrained Simplification

Typically a pseudo-Boolean inequality cL ≥ d is part of a set of pseudo-Boolean inequalities S. We present reformulation techniques for a pseudo-Boolean inequality that constrain the reformulation of cL ≥ d w.r.t. S. In the previous sections we presented a method that reformulated a pseudo-Boolean inequality cL ≥ d as a set of extended clauses S′ such that

Ext(cL ≥ d) = Ext(S′) .

Since cL ≥ d is part of a set of pseudo-Boolean inequalities S it is sufficient if cL ≥ d is equivalent to S′ with respect to the context S, that is only

Ext(S ∪ {cL ≥ d}) = Ext(S ∪ S′)

need to hold. Assume that S′ can also be a set of pseudo-Boolean inequalities. Then replacing cL ≥ d by S′ is useful only if S′ is in some sense simpler than cL ≥ d.

We present in Sect. 8.1 a method that generates stronger pseudo-Boolean inequality c′L′ ≥ d′ from cL ≥ d, that is Ext(c′L′ ≥ d′) ⊆ Ext(cL ≥ d), for which

Ext(S ∪ {cL ≥ d}) = Ext(S ∪ {c′L′ ≥ d′})

holds. So if cL ≥ d is part of the set of pseudo-Boolean inequalities S we can replace cL ≥ d by the stronger pseudo-Boolean inequality c′L′ ≥ d′. It is often possible to transform some simple pseudo-Boolean inequalities in S into a small equivalent set of extended clauses which can then be used to strengthen cL ≥ d. Since extended clauses are computationally easier to handle we restrict ourself mainly to the case that the context S is a set of extended clauses. So the goal is to construct a pseudo-Boolean inequality c′L′ ≥ d′ that dominates cL ≥ d but equivalence w.r.t. S, that is Ext(S ∪ {cL ≥ d}) = Ext(S ∪ {c′L′ ≥ d′}), still holds. Transforming such a strengthened pseudo-Boolean inequality c′L′ ≥ d′ instead of cL ≥ d generates stronger extended clauses.

In Sect. 8.2 we show how to replace cL ≥ d by a set of pseudo-Boolean inequalities S′ w.r.t. the context S such that Ext(S ∪ {cL ≥ d}) = Ext(S ∪ S′). The pseudo-Boolean inequalities in S′ are simpler in the sense that each of them contains less literals than cL ≥ d. The method can be applied when the original pseudo-Boolean inequality cL ≥ d is too large to be transformed completely. We then hope to transform more easily some of the pseudo-Boolean inequalities in S′ and afterwards strengthen the set of extended clauses which again may lead to a strengthening of the remaining pseudo-Boolean inequalities in S′.

We present a variant of the transformation method in Sect 8.3. We assume again that the context of the pseudo-Boolean inequality cL ≥ d is a set of extended clauses S. We transform cL ≥ d into an equivalent set of extended clauses S′ such that Ext(S ∪ {cL ≥ d}) = Ext(S ∪ S′) but the number of extended clauses in S′ is reduced or, optionally, the generated extended clauses are stronger than the one of the unconstrained transformation.

The simplification of a pseudo-Boolean inequality constrained by a context S is common to the methods presented in this section. In the context of constraint logic programming equivalence preserving reformulation of constraints into simpler ones w.r.t. a context is called relative simplification [Smo94]; an essential functionality of constraint solvers for concurrent constraint languages.

8.1 Coefficient Reduction

We use the context S for reducing one of the coefficients in the pseudo-Boolean inequality cL ≥ d. The resulting pseudo-Boolean inequality dominates cL ≥ d but is equivalent to cL ≥ d w.r.t. the context S.

Let c_{i}L_{i} be a product of cL ≥ d and let c′L′ be cL \ {c_{i}L_{i}}. We search for a pseudo-Boolean inequality c′_{i}L_{i} + c′L′ ≥ d where c′_{i} < c_{i} and therefore c′_{i}L_{i} + c′L′ ≥ d dominates cL ≥ d, and

Ext(S ∪ {c′_{i}L_{i} + c′L′ ≥ d}) = Ext(S ∪ {cL ≥ d}) .  (27)

Since c′_{i}L_{i} + c′L′ ≥ d dominates cL ≥ d we know that SCP(SRed(c′_{i}L_{i} + c′L′ ≥ d)) dominates SCP(SRed(cL ≥ d)). Because our transformation method generates a set of prime extended clauses we further know that each extended clause in SCP(SRed(cL ≥ d)) is dominated by an extended clause in SCP(SRed(c′_{i}L_{i} + c′L′ ≥ d)). Transforming c′_{i}L_{i} + c′L′ ≥ d instead of cL ≥ d generates therefore only stronger extended clauses, that is every extended clause we obtain by transforming cL ≥ d is dominated by an extended clause obtained by transforming c′_{i}L_{i} + c′L′ ≥ d.

We next describe how to derive a coefficient c′_{i} such that (27) holds. The key idea is to deduce a lower bound b for the pseudo-Boolean term c′L′ w.r.t. S ∪ {L_{i} ≥ 1}.

Proposition 8.1 If S ∪ {L_{i} ≥ 1} dominates c′L′ ≥ b and c_{i} > d − b then

Ext(S ∪ {c_{i}L_{i} + c′L′ ≥ d}) = Ext(S ∪ {(d − b)L_{i} + c′L′ ≥ d}) .

We then have reduced the coefficient c_{i} to c′_{i} = d − b < c_{i}.

PROOF: The direction ⊇ is obvious since c_{i} > d − b and therefore (d − b)L_{i} + c′L′ ≥ d dominates c_{i}L_{i} + c′L′ ≥ d. It remains to show ⊆. Let α be in Ext(S ∪ {c_{i}L_{i} + c′L′ ≥ d}). We

show that then α is in Ext(S ∪ {(d − b)L_{i} + c′L′ ≥ d}) by case analysis on α(L_{i}).

α(L_{i}) = 0: Since then α(c_{i}L_{i} + c′L′) = α((d − b)L_{i} + c′L′) = α(c′L′) we know that α(c_{i}L_{i} +

c′L′) ≥ d if and only if α((d − b)L_{i} + c′L′) ≥ d.

α(L_{i}) = 1: It is sufficient to show that α((d − b)L_{i} + c′L′) ≥ d since α is in Ext(S). Because α(L_{i}) = 1 we have α((d − b)L_{i} + c′L′) = (d − b) + α(c′L′) and it remains to show that (d − b) + α(c′L′) ≥ d which simplifies to α(c′L′) ≥ b. Since S ∪ {L_{i} ≥ 1} dominates c′L′ ≥ b we have α(c′L′) ≥ b for all assignments α ∈ Ext(S) where α(L_{i}) = 1. ⊓ ⊔

Dietrich et al. [DEC93] present a similar coefficient reduction technique where ≤-inequalities are used instead of ≥-inequalities. A necessary condition for the application of coefficient reduction is that S ∪ {L_{i} ≥ 1} dominates cL ≥ d. Otherwise S does not dominate c′L′ ≥ d − c_{i} and therefore for each lower bound b of c′L′ w.r.t. S ∪ {L_{i} ≥ 1} we have b ≤ d − c_{i} which contradicts c_{i} > d − b.

Example 8.2 Let cL ≥ d be

10 · A + 5 · B + 4 · C + 3 · D + 3 · E ≥ 10 .  (28)

Good candidates for coefficient reductions are obviously coefficient/literal pairs c_{i}L_{i}, where the coefficient c_{i} is relatively large w.r.t. the right-hand side because then the necessary condition, S ∪ {L_{i} ≥ 1} dominates cL ≥ d, is more likely to hold. Let us choose 10 · A and since the coefficient 10 equals the right-hand side we know that S ∪ {A ≥ 1} dominates (28) for all sets of extended clauses S. We can reduce the coefficient 10 if we find some lower bound b > 0 for the pseudo-Boolean term 5 · B + 4 · C + 3 · D + 3 · E. Suppose that S contains the extended clause \overline{A} + B + C + F ≥ 2. Since \{\overline{A} + B + C + F ≥ 2, A ≥ 1\} dominates B + C ≥ 1 we know that either B or C has to be 1. Therefore we can derive the lower bound b = 4.

\{\overline{A} + B + C + F ≥ 2, A ≥ 1\} dominates 5 · B + 4 · C + 3 · D + 3 · E ≥ 4

Following Prop. 8.1 we obtain c′_{i} = 6 and c′_{i}L_{i} + cL ≥ d is

6 · A + 5 · B + 4 · C + 3 · D + 3 · E ≥ 10 .

When transforming both pseudo-Boolean inequalities c_{i}L_{i} + c′L′ ≥ d and c′_{i}L_{i} + c′L′ ≥ d we see that the former generates only extended clauses with right-hand side 1 whereas the latter generates for example the strongest extended clause A + B + C + D ≥ 2.

In order to obtain an ideal coefficient reduction we need to derive the maximal lower bound b_{min} of c′L′ w.r.t. S ∪ {L_{i} ≥ 1}. Because this involves solving the NP-complete problem

min : c′L′ w.r.t. S ∪ {L_{i} ≥ 1}

we only approximate the best lower bound b_{min}.

We propose the following procedure to obtain a valid lower bound b. Because the constraint set contains the unit literal L_{i} we first simplify the set of extended clauses by replacing S ∪ {L_{i} ≥ 1} by pbur(S ∪ {L_{i} ≥ 1}). Note that S ∪ {L_{i} ≥ 1} dominates pbur(S ∪ {L_{i} ≥ 1}). We then fix the literals of pbul(S ∪ {L_{i} ≥ 1}) in the objective function. For a set of literals K we define

o reduce(c′L′, K) := \{c_{j}L_{j} | c_{j}L_{j} ∈ c′L′, L_{j} ∉ K and \overline{L_{j}} ∉ K\}

and the updated objective function then is ĉL̂ := o reduce(c′L′, pbul(S ∪ {L_{i} ≥ 1})). Summing up the coefficients of the literals that are fixed to 1 gives us the constant b̂ which can be added to the lower bound that we obtain from the approximation of the minimum for ĉL̂. For a set of literals K we define

sum fixed(c′L′, K) := ∑_{c_{j}L_{j}∈c′L′:L_{j}∈K} c_{j}

and the desired constant then is b̂ := sum fixed(c′L′, pbul(S ∪ {L_{i} ≥ 1})). The minimum of c′L′ w.r.t. S ∪ {L_{i} ≥ 1} is then the same as the minimum of ĉL̂ + b̂ w.r.t. pbur(S ∪ {L_{i} ≥ 1}). We next consider the problem of approximating the minimum of ĉL̂ w.r.t. the set of extended clauses pbur(S ∪ {L_{i} ≥ 1}), where no extended clause in pbur(S ∪ {L_{i} ≥ 1}) dominates an extended clause of the form L_{i} ≥ 1. In other words no more obvious fixings apply.

We derive a set of extended clause S′ from the set pbur(S ∪{L_{i} ≥ 1}) such that S′ is dominated by pbur(S ∪ {L_{i} ≥ 1}) and S′ contains only literals also occuring in L̂. For a set of literals K and a set of extended clauses T we define

c reduce(T, K) := \{K′ ≥ β′ | \begin{matrix}K′ ⊎ K′′ ≥ β ∈ T, \\ β′ = β − |K′′| ≥ 1, \\ K′′ ⊆ K and K ∩ K′ = ∅ \end{matrix} \}

which is the set of all strict reductions of the extended clauses in T where all literals in K have been eliminated. The set of extended clauses S′ then is c reduce(pbur(S ∪ \{L_{i} ≥ 1\}), L \ (L̂ ∪ \overline{L̂})).

We now give a greedy like approach to obtain a valid lower bound b of ĉL̂ w.r.t. the set of extended clauses S′. For each extended clause K′ ≥ β′ in S′ we define

b_{K′≥β′} := s(ĉ′) where ĉ′L̂′ ⊆ ĉL̂, L̂′ ⊆ K′, |L̂′| = β′ and max(ĉ′) ≤ min(ĉ \ ĉ′) .

That is b_{K′≥β′} is the sum of the smallest β′ coefficients of ĉL̂ whose literals are in K′. So for each α ∈ Ext(K′ ≥ β′) we have α(ĉL̂) ≥ b_{K′≥β′} and so a first valid lower bound of ĉL̂ is b_{K′≥β′}. Let us select some bound b_{K′≥β′}. For assuring the bound b_{K′≥β′} we considered all literals occurring in K′. Note that the bound is also valid for the subterm of the objective function containing only the literals of K′. We can therefore safely replace this subterm in the objective function by the bound b_{K′≥β′} and minimize the simpler objective function. Hence a valid lower bound of ĉL̂ can be obtained by solving the simpler minimization problem

min : o reduce(ĉL̂, K′) + b_{K′≥β′} w.r.t. S′

which can again be solved by the same approach. We obtain the following algorithm calculating a valid lower bound b of ĉL̂ w.r.t. S′.

      lower bound(ĉL̂, S′)

b := 0

while ĉL̂ ≠ ∅ ∧ S′ ≠ ∅ K′ ≥ β′ := select clause(ĉL̂, S′) b := b + b_{K′≥β′} S′ := c reduce(S′, K′) ĉL̂ := o reduce(ĉL̂, K′)

endwhile return b

      end lower bound

The procedure select clause selects an extended clause that is used for deriving the current bound. We use the following heuristic. We choose the extended clause K′ ≥ β′ that maximizes

\frac{b_{K′≥β′}}{∑_{c_{i}L_{i}∈ĉL̂:L_{i}∈K′} c_{i}} .

The heuristic reflects that the bound is the largest or best w.r.t. the sum of the coefficients it has consumed. The computed lower bound b of c′L′ w.r.t. S ∪ {L_{i} ≥ 1} then is

sum fixed(c′L′, K) + lower bound(o reduce(c′L′, K), c reduce(pbur(S ∪ {L_{i} ≥ 1}), L′ \ K)) ,

where K = pbul(S ∪ {L_{i} ≥ 1}).

Example 8.3 Let cL ≥ d be

5 · A + 4 · B + 4 · C + 4 · D + 3 · E + 2 · F ≥ 11  (29)

and let the set of extended clauses S be

\{\overline{A} + B ≥ 1, C + D + G ≥ 2, D + E + F ≥ 1\} .

Let us reduce the the coefficient 5 of the literal A. We apply pseudo-Boolean unit resolution to S ∪ {A ≥ 1} and obtain

pbur(S ∪ {A ≥ 1}) = {C + D + G ≥ 2, D + E + F ≥ 1} and
pbul(S ∪ {A ≥ 1}) = {A, B} .

We next reduce pbur(S ∪ {A ≥ 1}) such that only the literals of the objective function remain, that is we eliminate all literals in L \ \{C, D, E, F, \overline{C}, \overline{D}, \overline{E}, \overline{F} \} and obtain

{C + D ≥ 1, D + E + F ≥ 1} .

We update the objective function c′L′ by calculating

sum fixed(4 · B + 4 · C + 4 · D + 3 · E + 2 · F, {A, B}) = 4
o reduce(cL, {A, B}) = 4 · C + 4 · D + 3 · E + 2 · F

and then call lower bound. Calculating the b_{K′≥β′} yields

b_{C+D≥1} = 4 b_{D+E+F ≥1} = 2

and since 4/8 > 2/9 we select C + D ≥ 1. Updating the objective function and the extended clause set gives

o reduce(4 · C + 4 · D + 3 · E + 2 · F, {C, D}) = 3 · E + 2 · F
c reduce({C + D ≥ 1, D + E + F ≥ 1}, {C, D}) = ∅

and hence lower bound stops and returns 4. The overall bound b then is 4 + 4 = 8 and therefore S ∪ {A ≥ 1} dominates

4 · B + 4 · C + 4 · D + 3 · E + 2 · F ≥ 8 .

By Prop. 8.1 we have 5 = c_{i} > d − b = 11 − 8 = 3 and can so reduce the coefficient 5 of A to 3. We finally obtain the stronger pseudo-Boolean inequality

4 · B + 4 · C + 4 · D + 3 · A + 3 · E + 2 · F ≥ 11

which is equivalent to (29) w.r.t. to the context S.

The presented method for deriving a lower bound of c′L′ w.r.t. S ∪{L_{i} ≥ 1} yields good bounds when the set of extended clauses S is sparse or if the set of extended clauses S is nearly prime. Note that any method can be used to obtain a valid lower bound and the better the approximation of b_{min} the more likely it is that coefficient reduction applies.

8.2 Constrained Strict Reductions

We next consider a method that replaces a pseudo-Boolean inequality cL ≥ d by a set of pseudo-Boolean inequalities S′ such that cL ≥ d is equivalent to S′ w.r.t. a set of extended clauses S.

Ext(S ∪ {I}) = Ext(S ∪ S′)

In the previous section we focused on deriving lower bounds for a pseudo-Boolean subterm of the original pseudo-Boolean inequality and so strengthened the pseudo-Boolean inequality and therefore the extended clauses generated by the transformation method. Application of coefficient reduction is always an improvement. Conversely to the method of Sect. 8.1 we allow here that S′ is weaker than cL ≥ d, that is Ext(S′) ⊇ Ext(cL ≥ d). The set S′ is simpler because the pseudo-Boolean inequalities in S′ contain less literals than cL ≥ d. Unfortunately we may loose strong extended clauses when transforming the pseudo-Boolean inequalities in S′ instead of cL ≥ d. On the other side we possibly reduce the number of generated extended clauses. The idea is that some of the pseudo-Boolean inequalities in S′ are easier to transform than cL ≥ d. Combining the obtained strongest extended clauses with S may strengthen S which again may lead to further simplifications.

When transforming a pseudo-Boolean inequality cL ≥ d we need to calculate all strict reductions SRed(cL ≥ d). We show how to reduce the number of necessary strict reductions, that is we constrain the generation of strict reductions and so reduce the number of generated extended clauses.

Proposition 8.4 Let cL ≥ d be a pseudo-Boolean inequality and let L′ ≥ β be an extended clause where L′ ⊆ L. Let S′ be the set of pseudo-Boolean inequalities

\{ĉL̂ ≥ d̂| \begin{matrix}ĉL̂ = cL \ c′′L′′, \\ d̂= d − s(c′′), \\ c′′L′′ ⊆ cL, \\ L′′ ⊆ L′ and |L′′| = β \end{matrix} \}

then Ext({L′ ≥ β, cL ≥ d}) = Ext({L′ ≥ β} ∪ S′). Note that S′ is the set of all strict reductions of cL ≥ d, where the set of literals L′′ for all L′′ ⊆ L′ and |L′′| = β has been eliminated.

PROOF: Since S′ ⊆ SRed(cL ≥ d) we know that cL ≥ d dominates S′. It remains to show that every satisfying assignment α of {L′ ≥ β} ∪ S′ is a satisfying assignment of cL ≥ d. Let α be in Ext({L′ ≥ β} ∪ S′). Let L′′′ ⊆ L′ be the set of literals such that for each L_{i} ∈ L′′′ we have α(L_{i}) = 1. Because L′ ≥ β we know that |L′′′| ≥ β. Let L′′ be a subset of L′′′ such that |L′′| = β. We select the strict reduction ĉL̂ ≥ d − s(c′′) from S′ where L′′ has been eliminated. We denote by s(c′′) the sum over the coefficients c_{i} for all c_{i}L_{i} ∈ c′′L′′. Because α is a solution of S′ we know that α(ĉL̂) ≥ d − s(c′′) and therefore α(ĉL̂) + s(c′′) ≥ d. Because α(ĉL̂) + s(c′′) = α(cL) we have α(cL) ≥ d. ⊓ ⊔

Example 8.5 Let cL ≥ be

c_{1} · A + c_{2} · B + c_{3} · C + cL ≥ d

and suppose that the extended clause A + B + C ≥ 2 is dominated by an extended clause in the context S. Note that c_{1}, c_{2}, c_{3} can be every coefficients of cL ≥ d, not necessarily the largest ones. We can then replace cL ≥ d by S′ =

{c_{1} · A + cL ≥ d − (c_{2} + c_{3}),
c_{2} · B + cL ≥ d − (c_{1} + c_{3}),
c_{3} · C + cL ≥ d − (c_{1} + c_{2})}

according to Prop. 8.4 and have Ext(S ∪ {cL ≥ d}) = Ext(S ∪ S′).

The use of Prop. 8.4 is only practicable if the number of pseudo-Boolean inequalities it generates is not too high. Note that Prop. 8.4 generates \binom{|L′|}{β} extended clauses. So most reasonably it is applicable if β is close to |L′| since then the number of pseudo-Boolean inequalities is small and the number of deleted literals is high. In Example 8.5 we used an extended clause, where |L′| − β = 1 and so \binom{|L′|}{β} = |L′|. Extended clauses of the form L′ ≥ |L′| − 1 are also called clique inequalities or special ordered set constraints [NW88] and frequently occur in practical pseudo-Boolean constraint sets.

One problem of the application of Prop. 8.4 is that we may loose strong extended clauses.

Example 8.6 [a] Let cL ≥ d be

5 · A + 4 · B + 3 · C ≥ 6

then cL ≥ d is equivalent to A + B + C ≥ 2. Applying Prop. 8.4 on cL ≥ d with the extended clause A + B ≥ 1 gives the set of pseudo-Boolean inequalities

{5 · A + 3 · C ≥ 2, 4 · B + 3 · C ≥ 1}  (30)

equivalent to cL ≥ d w.r.t. {A + B ≥ 1}. Transforming the pseudo-Boolean inequalities in (30) yields

{A + C ≥ 1, B + C ≥ 1} .

Now Prop. 8.4 assures that

Ext({A + C ≥ 1, B + C ≥ 1, A + B ≥ 1}) = Ext({A + B + C ≥ 2})

but the better formulation of cL ≥ d is obviously {A + B + C ≥ 2}. Indeed in [Bar94] we describe how to obtain this better formulation if only {A + C ≥ 1, B + C ≥ 1} and A + B ≥ 1 are given.

[b] Let cL ≥ d be

d · A + c_{i} · B + cL ≥ d

then we know that all generated extended clauses have degree 1. Suppose that there is a clique inequality in S dominating A + B ≥ 1. Then there is no strict reduction on A, because eliminating A would give a tautology. Because of Prop. 8.4 we know that cL ≥ d is equivalent to

(d − c_{i}) · A + cL ≥ d − c_{i}

and we are sure that we do not miss a strongest extended clause. So applications of Prop. 8.4 where all but one^{3} of the generated strict reductions are dominated by the context are safe.

Another problem is that transforming the pseudo-Boolean inequalities in the set S′ of Prop. 8.4 may involve redundant computation. While transforming the pseudo-Boolean inequalities of S′ in Example 8.5 we fully transform 3 times the strict reduction cL ≥ d − (c_{1} + c_{2} + c_{3}). We avoid the redundant computation by using Prop. 8.4 directly in the transformation routine.

Example 8.7 Let cL ≥ d be

c_{1} · A + c_{2} · B + c_{3} · C + cL ≥ d

as in Example 8.5 and suppose that c_{1} ≥ c_{2} ≥ c_{3}. We assume that the extended clause

A + B + C ≥ 2

is dominated by an extended clause in the context. Because of Prop. 8.4 we know that cL ≥ d is equivalent to the set of pseudo-Boolean inequalities S′ =

{c_{1} · A + cL ≥ d − (c_{2} + c_{3}),
c_{2} · B + cL ≥ d − (c_{1} + c_{3}),
c_{3} · C + cL ≥ d − (c_{1} + c_{2})} .

We now transform c_{1} · A + cL ≥ d − (c_{2} + c_{3}) completely with the standard transformation method but we start the transformation of c_{2} · B + cL ≥ d − (c_{1} + c_{3}) with the forbidden elimination on B since all extended clauses generated when B is eliminated are already obtained by the full transformation of c_{1} ·A+cL ≥ d−(c_{2} +c_{3}). Likewise we forbid elimination of C when transforming c_{3} · C + cL ≥ d − (c_{1} + c_{2}) and so avoid the redundant transformation of cL ≥ d − (c_{1} + c_{2} + c_{3}).

8.3 Constrained Transformation

We present a variant of the transformation method that restricts the number of generated extended clauses while transforming a pseudo-Boolean inequality cL ≥ d w.r.t. a set of extended clauses S. Let E be the set of non redundant extended clauses generated by the transformation of cL ≥ d then constrained transformation generates a smaller set E′ ⊆ E such that

Ext(S ∪ {cL ≥ d}) = Ext(S ∪ E′) .

While transforming a pseudo-Boolean inequality cL ≥ d we need to compute all strict reductions SRed(cL ≥ d). When proving the equivalence of SCP(SRed(cL ≥ d)) and cL ≥ d in Theorem 3.6 we show that for each non satisfying assignment α of cL ≥ d we find an extended clause L′ ≥ β in SCP(SRed(I)) such that α is not a satisfying assignment of L′ ≥ β. If α is not a satisfying assignment of the context S then we need not find an extended clause in SCP(SRed(cL ≥ d)) for which α is not a satisfying assignment. Hence the corresponding generated extended clause need not be added for preserving equivalence. We can so restrict the number of needed strict reductions and therefore the number of generated extended clauses. We first define a set of strict reductions of cL ≥ d taking into account the context S.

3If all generated strict reductions are dominated by the context then of course the whole pseudo-Boolean inequality is dominated by the context and can be ignored.

Definition 8.8 Let cL ≥ d be a pseudo-Boolean inequality, let S be a set of extended clauses and c′L′ ≥ d′ be a strict reduction of cL ≥ d. The set of literals L\L′ is the set of literals that have been eliminated from cL ≥ d in order to obtain c′L′ ≥ d′. We denote by SRed(cL ≥ d)_{|S} ⊆ SRed(cL ≥ d) the set of strict reductions of cL ≥ d such that

c′L′ ≥ d′ ∈ SRed(cL ≥ d)_{|S} iff S ∪ {L \ L′ ≥ |L \ L′|} is satisfiable .

We now show that the set SCP(SRed(cL ≥ d)_{|S}) of strongest extended clauses obtained from the smaller set of strict reductions is sufficient for the equivalence with cL ≥ d w.r.t. a set S of extended clauses.

Theorem 8.9 Let cL ≥ d be a pseudo-Boolean inequality and let S a set of extended clauses, then

Ext(S ∪ {cL ≥ d}) = Ext(S ∪ SCP(SRed(cL ≥ d)_{|S})) .

PROOF:

• Ext(S ∪ {cL ≥ d}) ⊆ Ext(S ∪ SCP(SRed(cL ≥ d))_{|S}) : as in Theorem 3.6.

• Ext(S ∪ {cL ≥ d}) ⊇ Ext(S ∪ SCP(SRed(cL ≥ d))_{|S}) :

We show that if α ∉ Ext(S ∪ {cL ≥ d}) then α ∉ Ext(S ∪ SCP(SRed(cL ≥ d)_{|S})) from which the theorem follows. Suppose that α ∉ Ext(S ∪ {cL ≥ d}). If α ∉ Ext(S) then obviously α ∉ Ext(S ∪ SCP(SRed(cL ≥ d)_{|S})). Suppose that α ∈ Ext(S) but α ∉ Ext(cL ≥ d). We show that in this case there is a strict reduction in SRed(cL ≥ d)_{|S} such that α is not a satisfying assignment of this reduction, hence α ∉ Ext(SCP(SRed(cL ≥ d)_{|S})) and thus α ∉ Ext(S ∪ SCP(SRed(cL ≥ d)_{|S})). Since α ∉ Ext(cL ≥ d) we know that α(cL) = d′ < d. Let Y be the set of literals L_{i} where α(L_{i}) = 1 and Z = L\Y, then ∑_{i:L_{i}∈Y} c_{i} = d′ < d. Let c′L′ ≥ d′ be ∑_{i:L_{i}∈Z} c_{i}L_{i} ≥ d−d′. Because d′ < d we know that d − d′ ≥ 1 and therefore c′L′ ≥ d′ is a strict reduction of cL ≥ d, obtained by eliminating the literals that are mapped to zero by α. We know furthermore that Y = L \ L′, hence α(L \ L′) ≥ |L \ L′|. Because α ∈ Ext(S) we know that α ∈ (S ∪ {L \ L′ ≥ |L \ L′|}) and therefore c′L′ ≥ d′ in SRed(cL ≥ d)_{|S}. Let SCP(c′L′ ≥ d′) be L′ ≥ β. We know that β ≥ 1 because d − d′ ≥ 1. Because α(L′) = 0 we derive that α ∉ Ext(SCP(c′L′ ≥ d′)) and therefore α ∉ Ext(SCP(SRed(cL ≥ d))), which establish the theorem. ⊓ ⊔

The proof of Theorem 8.9 is similar to the proof of Theorem 3.6. The main difference is that we additionally show that each strict reduction we need is in the restricted set of strict reductions. Theorem 3.6 can be seen as an instance of Theorem 8.9, where the set of extended clauses S is the empty set.

An implementation of the constrained transformation algorithm is now straightforward. For each strict reduction c′L′ ≥ d′ of cL ≥ d we maintain a set of extended clauses c′L′ ≥ d′_{S} := S ∪ {L \ L′ ≥ |L \ L′|}. By Theorem 8.9 we can eliminate the strict reduction c′L′ ≥ d′ from the transformation process if c′L′ ≥ d′_{S} is unsatisfiable. Note that if c′L′ ≥ d′_{S} is unsatisfiable then for each strict reduction c′′L′′ ≥ d′′ of c′L′ ≥ d′ the corresponding set of extended clauses {S ∪ {L \ L′′ ≥ |L \ L′′|} is unsatisfiable. Care must be taken when applying the strong redundancy criteria presented in Sect. 4. Suppose that a strict reduction c′L′ ≥ d′ is eliminated because c′L′ ≥ d′_{S} is unsatisfiable. Suppose furthermore that SCP(c′L′ ≥ d′) dominates an extended clause SCP(c′′L′′ ≥ d′′) where c′′L′′ ≥ d′′ is a strict reduction of c′L′ ≥ d′ and there is no other non redundant extended clause dominating SCP(c′L′ ≥ d′). In that case we have to add SCP(c′′L′′ ≥ d′′) or SCP(c′L′ ≥ d′) for preserving equivalence. The simplest way is to add SCP(c′L′ ≥ d′) always if c′L′ ≥ d′_{S} is unsatisfiable and then safely forbid further strict reductions of c′L′ ≥ d′, that is we not recursively transform c′L′ ≥ d′. When later inserting the transformed set of extended clauses into a larger set, redundant extended clauses can be deleted.

In the constrained transformation algorithm we need to solve again a satisfiability problem for the set of extended clauses S ∪{L\L′ ≥ |L\L′|}. Because this is an NP-complete problem we relax the problem again to checking whether the unit relaxation of S ∪ {L \ L′ ≥ |L \ L′|} is unsatisfiable. That is, at each node we check whether □ ∈ pbur(S ∪ {L \ L′ ≥ |L \ L′|}). Note that all literals in L \ L′ are unit literals and therefore unsatisfiability of S ∪ {L \ L′ ≥ |L \ L′|} is likely to be detected by unit resolution.

Example 8.10 Let cL ≥ d be

6 · A + 5 · B + 4 · C + 3 · D + 2 · E + F ≥ 13

and suppose that the extended clause \overline{B} +\overline{C} ≥ 1 is dominated by an extended clause in the context S. Hence S ∪ {B + C ≥ 2} is unsatisfiable which is detected by pseudo-Boolean unit resolution. The full transformation of cL ≥ d generates 5 extended clauses. One strict reduction of cL ≥ d is

6 · A + 3 · D + 2 · E + F ≥ 4  (31)

from which the two non redundant extended clauses

A + E + F ≥ 1 A + D ≥ 1

are derived. Since the set of extended clauses 6·A+3·D+2·E+F ≥ 4_{|S} is unsatisfiable, and therefore SRed(6·A+3·D+2·E+F ≥ 4)_{|S} = ∅, we need not consider 6·A+3·D+2·E+F ≥ 4 and constrained transformation generates only 3 extended clauses. Note that SCP(6 · A + 3 · D + 2 · E + F ≥ 4) is redundant and dominated by another extended clause from the remaining 3 and so we need not include SCP(6 · A + 3 · D + 2 · E + F ≥ 4).

Instead of deleting the strict reduction c′L′ ≥ d′ if c′L′ ≥ d′_{|S} is unsatisfiable we can use that fact for strengthening the generated extended clause. We explain the idea first on an example. Let cL ≥ d be

c_{1} · A + c_{2} · B + cL ≥ d .

and suppose that S ∪ {A + B ≥ 2} is unsatisfiable. Hence the strict reduction

cL ≥ d − (c_{1} + c_{2}) .  (32)

need not be considered. However because S ∪ \{A + B ≥ 2\} is unsatisfiable we know that \overline{A} + \overline{B} ≥ 1 is a valid extended clause w.r.t. S. So we can derive an upper bound for the pseudo-Boolean term c_{1} · A + c_{2} · B, namely \{\overline{A} + \overline{B} ≥ 1\} dominates c_{1} · A + c_{2} · B ≤ max(c_{1}, c_{2}). Therefore we derive the stronger pseudo-Boolean inequality

cL ≥ d − max(c_{1}, c_{2}) .  (33)

We miss no extended clause if we replace the strict reduction (32) by (33) but may only generate stronger extended clauses. Note that we derive here an upper bound for a pseudo-Boolean term and use the bound in order to strengthen the generated extended clauses.

Lemma 8.11 Let cL ≥ d be a pseudo-Boolean inequality and let c′L′ ≥ d′ be a strict reduction of cL ≥ d. Let S be a set of extended clauses such that c′L′ ≥ d′_{S} is unsatisfiable. Let c′′L′′ be cL \ c′L′ then

Ext(S ∪ {cL ≥ d}) = Ext(S ∪ (SCP(SRed(cL ≥ d)_{|S})) ∪ {c′L′ ≥ d′ + min(c′′)}) .

PROOF: The direction ⊇ is immediate by Theorem 8.9. It remains to show ⊆, that is S∪{cL ≥ d} dominates c′L′ ≥ d′+min(c′′). Let α ∈ Ext(S∪{cL ≥ d}) then we have α(cL) ≥ d and therefore α(c′L′) + α(c′′L′′) ≥ d. Since c′L′ ≥ d′_{S} = S ∪ {L′′ ≥ |L′′|} is unsatisfiable we know furthermore that S dominates \overline{L′′} ≥ 1, that is at least one literal of L′′ is mapped to 0 by α. We conclude that α(c′′L′′) ≤ s(c′′) − min(c′′) and since α(c′L′) + α(c′′L′′) ≥ d we have α(c′L′) + s(c′′) − min(c′′) ≥ d. Because d′ = d − s(c′′) we derive α(c′L′) + s(c′′) − min(c′′) ≥ d′ + s(c′′) which simplifies to α(c′L′) ≥ d′ + min(c′′). ⊓ ⊔

With Lemma 8.11 we can replace the strict reduction c′L′ ≥ d′ by the stronger pseudo-Boolean inequality c′L′ ≥ d′ + min(c′′) while preserving equivalence w.r.t. to the context S.

Example 8.12 Let cL ≥ d again be

6 · A + 5 · B + 4 · C + 3 · D + 2 · E + F ≥ 13

and suppose that S ∪{B +C ≥ 2} is unsatisfiable. A non redundant extended clause dominated by cL ≥ d is A + E + F ≥ 1. While eliminating B and C we detect unsatisfiability of S ∪ {B + C ≥ 2} and can replace the reduction

6 · A + 3 · D + 2 · E + F ≥ 4

by

6 · A + 3 · D + 2 · E + F ≥ 8

from which we derive the non redundant extended clause A + E ≥ 1 dominating A + E + F ≥ 1. Note that 6 · A + 3 · D + 2 · E + F ≥ 8 dominates A ≥ 1 which is obtained from the strongest extended clause of the strict reduction obtained when further eliminating {D, E, F }. So in this case we replace a non redundant extended clause by a stronger one but we may also derive new extended clauses that do not dominate other generated extended clause.

We propose to use Lemma 8.11 in the constrained transformation algorithm and to consider no further strict reductions of the stronger strict reduction c′L′ ≥ d′ + min(c′′) but only add SCP(c′L′ ≥ d′ + min(c′′))^{4} to the set of extended clauses. Note that we get the stronger extended clause SCP(c′L′ ≥ d′ + min(c′′)) with minimal computational effort and we have to add SCP(c′L′ ≥ d′) in any case in order to apply the redundancy criteria presented in Sect. 4.

Obviously, all results still hold if we use instead of a set of extended clauses as context a set of pseudo-Boolean inequalities for constraining the transformation. We presented the constrained transformation for extended clauses because we can strengthen the set of extended clauses using the deductive system “Generalized Resolution” [Hoo92, Bar94]. For such a strengthened set of extended clauses, unsatisfiability of c′L′ ≥ d′_{S} is typically more often detected by pseudo-Boolean unit resolution and therefore the set of generated extended clauses is even smaller. The presentation of the strengthening methods [Bar94] is not in the scope of this paper.

9 Applications

We present two applications of the transformation algorithm besides its use for the constraint solver of CLP(PB). We show how to enhance the symbolic deduction method “Generalized Resolution” [Hoo92] and we relate our method to traditional linear 0-1 integer programming [NW88].

9.1 Generalized Resolution

Hooker [Hoo92] defined the resolvent of two extended clauses as the classical resolvent of two classical clauses, each of them dominated by one of the extended clauses. We enhance the notion of resolvents between extended clauses and show how to efficiently implement the inference rule with help of the presented transformation method.

Example 9.1 Let

A + B + \overline{D} + E + \overline{F} + \overline{G} ≥ 4  (34)
\overline{A} + \overline{C} + \overline{D} + \overline{E} + F + G ≥ 3  (35)

be two extended clauses. The classical clause A + B + \overline{D} ≥ 1 is dominated by (34) and \overline{A} + \overline{C} + \overline{D} + \overline{E} ≥ 1 is dominated by (35). From these two classical clauses we obtain the classical resolvent B + \overline{C} + \overline{D} + \overline{E} ≥ 1 by resolving on A.

It is well known [Hoo88] that the resolvent of two classical clauses can be obtained by linear combination of the two classical clauses and the valid bounds L_{i} ≥ 0 and −L_{i} ≥ −1 for all literals L_{i}, and integer rounding. So resolvents are also cutting plane inequalities. It is easy to see that resolvents of extended clauses can also be obtained by linear combination and rounding since classical clauses dominated by extended clause are strict reductions that are obtained by adding the valid bound −L_{i} ≥ −1 for all literals L_{i} that are eliminated. We show that transforming the linear pseudo-Boolean inequality obtained by summing up two extended clauses generates all extended clauses that can be derived from the two extended clauses; among them all possible resolvents.

4Or better the non redundant extended clause dominating SCP(c′L′ ≥ d′+min(c′′)) on the path H_{k+1} of Prop. 4.8.

The sum of two pseudo-Boolean inequalities cL ≥ d and c′L′ ≥ d′ is the pseudo-Boolean inequality cL + c′L′ ≥ d + d′. We assume as usual that the sum of two pseudo-Boolean inequalities is brought into pseudo-Boolean normal form.

Proposition 9.2 Each resolvent of two extended clauses L ≥ d and L′ ≥ d′ is dominated by an extended clause in SCP(SRed(cL + c′L′ ≥ d + d′)).

PROOF: We first extract the literals that occur positive in one extended clause and negative the other. Let L_{R} + K = L and L′_{R} + \overline{K} = L′, where K = \{L_{i} | L_{i} ∈ L and \overline{L_{i}} ∈ L′\} and \overline{K} = \{\overline{L_{i}} | L_{i} ∈ K\}. The general representation^{5} of each classical clause that is dominated by L ≥ d is L_{C} + K_{C} ≥ 1, where |K_{C}| = 1 and |L_{R} \ L_{C}| + |K \ K_{C}| ≤ d − 1. Similarly the general representation of each classical clause that is dominated by L′ ≥ d′ is L′_{C} + K′_{C} ≥ 1, where |K′_{C}| = 1 and |L′_{R} \ L′_{C}| + |K′ \ K′_{C}| ≤ d′ − 1. We next extract the literals that occur in both L_{C} and L′_{C}. Let P ∪ Q = L_{C} and P ∪ Q′ = L′_{C} where L_{C} ∩ L′_{C} = P and Q ∩ Q′ = ∅. So the general representation of a resolvent of L ≥ d and L′ ≥ d′ is

P ∪ Q ∪ Q′ ≥ 1 .

Let us now investigate the sum of L ≥ d and L′ ≥ d′. We know that L + L′ ≥ d + d′ is equivalent to

L_{R} + L′_{R} + |K| ≥ d + d′(≥ |L_{R} \ L_{C}| + |L′_{R} \ L′_{C}| + 2 + 2 · (|K| − 1))

from which we derive

L_{R} + L′_{R} ≥ d + d′ − |K|(≥ |L_{R} \ L_{C}| + |L′_{R} \ L′_{C}| + |K|) .

A valid strict reduction of L + L′ ≥ d + d′ is

L_{C} + L′_{C} ≥ d + d′ − |K| − |L_{R} \ L_{C}| − |L′_{R} \ L′_{C}|(≥ |K| ≥ 1)

obtained by eliminating the literals in (L_{R} \ L_{C}) ∪ (L′_{R} \ L′_{C}). We rewrite L_{C} and L′_{C} and obtain

2 · P + Q + Q′ ≥ d + d′ − |K| − |L_{R} \ L_{C}| − |L′_{R} \ L′_{C}|(≥ |K| ≥ 1)

We apply the cutting plane operation of Sect. 3 and obtain

P + Q + Q′ ≥ ⌈\frac{d + d′ − |K| − |L_{R} \ L_{C}| − |L′_{R} \ L′_{C}|}{2}⌉ (≥ ⌈\frac{|K|}{2}⌉ ≥ ⌈\frac{1}{2}⌉ = 1)

which obviously implies P + Q + Q′ ≥ 1. Because each extended clause obtained by linear combination and rounding is dominated by a strongest extended clause the proposition is established. ⊓ ⊔

5Note that we consider only classical clauses that do not introduce new literals, because their resolvent is dominated by either one of the fathers, or by the resolvent of the valid classical clauses where we do not introduce new literals.

By Prop. 9.2 we can replace the original resolution rule of “Generalized Resolution” by a rule generating the equivalent set of extended clauses of the pseudo-Boolean inequality L + L′ ≥ d + d′ while preserving completeness.

Example 9.3 [Hoo92] Let

A + B + \overline{D} + E + \overline{F} + \overline{G} ≥ 4
\overline{A} + \overline{C} + \overline{D} + \overline{E} + F + G ≥ 3

be two extended clauses. With the enhanced resolution rule of Hooker [Hoo92] we may generate 12 different resolvents, where

B + \overline{C} + \overline{D} + \overline{E} + F + \overline{G} ≥ 2

is one of them. The sum of the two extended clauses is (already normalized) 2 · \overline{D} + B + \overline{C} ≥ 3. After transformation we obtain the two extended clauses

\overline{D} + \overline{C} + B ≥ 2 \overline{D} ≥ 1 ,

where each of the 12 resolvents is dominated by one of them.

So using the presented transformation method we generate fewer and stronger extended clauses than with the original resolution method. Note that there are no further non redundant resolution steps since resolution between the extended clauses in SCP(SRed(L + L′ ≥ d + d′)) are not possible since no literals occur negatively and positively in them. Additionally there is no literal occurring in L ≥ d or L′ ≥ d′ and negatively in an extended clause in SCP(SRed(L+L′ ≥ d+d′)). So the only possible resolution steps are the ones between L ≥ d and L′ ≥ d′. But they are all dominated by an extended clause in SCP(SRed(L + L′ ≥ d + d′)) because of Prop. 9.2. We just want to mention that we generate not only resolvents but also diagonal sums [Hoo92], generated by the other rule of “Generalized Resolution”. Note that the sum of A+B ≥ 1 and C+D ≥ 1 is A+B+C+D ≥ 2, which is already an extended clause. Since there is no other extended clause dominating A+B+C+D ≥ 2 that is derivable from A + B ≥ 1 and C + D ≥ 1 the strongest extended clause A + B + C + D ≥ 2 is non redundant. In fact we can show that {L ≥ d, L′ ≥ d′} ∪ SCP(SRed(L + L′ ≥ d + d′)) is prime.

9.2 0-1 Integer Programming

Extended cover inequalities of a linear 0-1 inequality, well known in 0-1 integer programming, can be related to the extended clauses generated by our transformation method. In a preprocessing phase of a linear programming based 0-1 optimization algorithm, branch-and-bound, valid extended cover inequalities can be added to the constraint set in order to strength the linear programming relaxation of the problem [NW88].

We show how to use the transformation method for generating these extended cover inequalities and how to restrict the transformation method in order to produce strong extended cover inequalities or extended cover inequalities over a special subset of variables. We test the method on a subset of 0-1 integer programming problems and report computational results.

9.2.1 Extended Clauses and Extended Cover Inequalities

Preprocessing 0-1 integer programming problems and applying constraint generation techniques have made large scale 0-1 problems solvable in reasonable time [CJP83, JKS85]. The wildly used branch-and-bound method for solving 0-1 integer optimization problems solves the linear programming (LP) relaxation of the problem and then branches on variables with fractional values in the current LP-solution. In a preprocessing phase valid 0-1 inequalities are generated, so called strong cuts, that better approximate the integral solution of the problem and solving the reformulated problem therefore typically require less branch and bound cycles.

The constraint set of a linear 0-1 integer programming problem consists of a set of linear 0-1 inequalities of the form

c_{1} · X_{1} + ⋯ + c_{n} · X_{n} ≤ d  (36)

which is equivalent to

−c_{1} · X_{1} − ⋯ − c_{n} · X_{n} ≥ −d

and can then be brought into pseudo-Boolean normal form.

An important constraint generation technique is presented in [NW88]. It is based mainly on the notion of minimal covers or minimal dependent sets.

Definition 9.4 [NW88] A set C ⊆ {1, …, n} is a minimal dependent set of a linear 0-1 inequality (36) if

∑_{i∈C\{j}} c_{i} ≤ d < ∑_{i∈C} c_{i}

for all j ∈ C.

Proposition 9.5 [NW88] If C is a minimal dependent set for a linear 0-1 inequality (36) then

∑_{i∈E(C)} X_{i} ≤ |C| − 1 ,  (37)

where

E(C) = C ∪ {k | 1 ≤ k ≤ n and c_{k} ≥ c_{j} for all j ∈ C}

is a valid inequality w.r.t. (36). The set of indices E(C) is called the extension of C and we call (37) an extended cover inequality.

Let us write (37) in pseudo-Boolean normal form.

∑_{i∈E(C)} \overline{X_{i}} ≥ |E(C) \ C| + 1  (38)

We know that

∑_{i∈E(C)} \overline{X_{i}} ≥ |E(C) \ C| + 2

is not a valid inequality, because otherwise

∑_{i∈E(C)} X_{i} ≤ |C| − 2

p0033  # Ineqs # Clauses # Nodes PrePro Solve LP-Sol. Optimum
Original  11  4  9685  0.00 59.89 2520.57  3089
Normal  11  4  1289  0.00  6.47 2819.36  3089
Simple  2  80  124  0.04  1.42 2846.00  3089
Full  0  8710  118  0.90 237.30 2846.00  3089

Figure 4: Computational Results for “p0033”

is valid which is not the case since C is minimal. Hence (38) is the strongest extended clause containing exactly the literals X_{i} for all i ∈ E(C). We can therefore use our transformation procedure to systematically construct the set of all strongest non redundant extended cover inequalities.

In a preprocessing phase for 0-1 integer programming extended cover inequalities are generated and added to the original constraint set. Because of our equivalence result we can replace the original inequality by its set of equivalent extended clauses.

Example 9.6 Let us look again at Example 5.1 on page 20.

[a] By writing the extended clauses as “≤-inequalities” we see that the two extended cover inequalities

\begin{aligned}X_{1} + X_{2} + X_{3} + X_{4} + X_{5} & ≤ & 3 \\ X_{1} + X_{2} + X_{3} & ≤ & 2 \end{aligned}

are equivalent to the linear 0-1 inequality

79 · X_{1} + 53 · X_{2} + 53 · X_{3} + 45 · X_{4} + 45 · X_{5} ≤ 178 .

[b] The single extended cover inequality

X_{1} + X_{6} + X_{7} + X_{9} ≤ 1

is equivalent to the linear 0-1 inequality

774 · X_{1} + 76 · X_{2} + 22 · X_{3} + 42 · X_{4} + 21 · X_{5} + 760 · X_{6} + 818 · X_{7} + 62 · X_{8} + 785 · X_{9} ≤ 1500 .

So for Example 9.6[a],[b] a full transformation is suitable. For Example 5.1[c] the number of extended clauses is too large and we need to restrict the number of extended clauses we generate. A trivial, but powerful, approach is to transform only simple pseudo-Boolean inequalities.

For example the complete constraint set of a 0-1 integer programming problem [NW88, page465], also available in MIPLIB [BBI92] as problem “p0033”, consists of 15 inequalities where 4 of them are already extended clauses. From the remaining 11 inequalities 9 are simple, that is they are equivalent to only a few extended clauses and just 2 inequalities produce more than 4000 extended clauses. So a naive approach is to transform the 13 simple inequalities completely and leave the 2 hard inequalities unchanged. We ran the commercial mixed integer solver CPLEX 2.1 on the original and the preprocessed problem. The results are reported in Fig. 4. In the columns we denote by “Ineqs” the number of inequalities with coefficients > 1 and by “Clauses” the number of extended clauses. “Nodes” is the number of nodes the branch and bound method of CPLEX needed in order to find the optimal solution and prove optimality. “PrePro” is the time in user cpu seconds on a SPARC-10 used by the Prolog implementation of the transformation method in order to preprocess the problem. “Solve” is the time in user cpu seconds CPLEX needed to solve the problem. By “LP-Sol.” we denote the optimal solution of the linear programming relaxation of the problem and by “Optimum” the integer optimal solution. The rows describe 4 different formulations of “p0033”. In “Original” we solve the original problem as found in MIPLIB. In “Normal” we solve the problem after bringing each inequality into pseudo-Boolean normal form.

Bringing an inequality into pseudo-Boolean normal form includes coefficient reduction as presented in [CJP83] and for “p0033” we obtain a speedup of factor 9. This is reflected by the better optimal solution of the linear programming relaxation of the problem and the number of linear programs solved (“Nodes”). Transforming the simple inequalities completely generates a larger problem (82 versus 15 constraints) but we obtain a speedup of factor 4 which is again due to a better linear programming relaxation. Note that the time consumed by the preprocessing phase is very small w.r.t. the “Solve”-time. A complete transformation of all inequalities shows to be too clumsy. The size of the problem (8710 versus 15 inequalities) slows down the linear programming solver although even fewer nodes are needed. Using constrained transformation as presented in Sect. 8.3, that is we transform each inequality completely where the context is the set of all remaining inequalities, generates only 4484 extended clauses. So when a complete transformation is required constrained transformation is advantageous. Since complete transformation of a constraint set of a 0-1 integer optimization problem is not suitable in the context of preprocessing we no longer consider constrained transformation. For preprocessing 0-1 integer programming problems we need to make our transformation method more flexible.

9.2.2 Restrictions

By restricting the number of generated extended clauses we can use the transformation method as generator of extended cover inequalities, that is strongest extended clauses, in the preprocessing phase for solving 0-1 integer optimization problems. We show how to focus on extended clauses that are sufficiently strong and restrict the number extended clauses by focusing on a set of variables.

We first give a measure of extended clauses describing their quality and show how to adopt the transformation method in order to obtain only extended clauses better than or equal to a given quality border. The weakness w of an extended clause L ≥ d is defined by

w(L ≥ d) := |L| − d .

Note that w(L ≥ d) ≤ w(L′ ≥ d′) is a necessary condition for L ≥ d dominates L′ ≥ d′, which is obvious from Lemma 2.5. Ordering extended clauses w.r.t. their negative weakness gives us therefore an approximation of the domination relation. We say that L ≥ d is stronger than L′ ≥ d′ if w(L ≥ d) ≤ w(L′ ≥ d′).

Given a pseudo-Boolean inequality we can easily determine the minimal weakness of all extended clauses the transformation method generates.

Lemma 9.7 Let cL ≥ d be a pseudo-Boolean inequality in normal form and β be such that

∑_{i=1}^{β} c_{n−i−1} < d ≤ ∑_{i=1}^{β+1} c_{n−i−1}  (39)

then β′ = |L|−β−1 is the smallest weakness of all extended clauses generated by the transformation method.

PROOF: We know that

∑_{i=1}^{n−β} c_{i}L_{i} ≥ d − ∑_{i=1}^{β} c_{n−i−1}

is a valid strict reduction of cL ≥ d. The right-hand side of its corresponding strongest extended clause is 1 because of (39) and therefore its weakness is n − β − 1 = β′. We next show that there is no extended clause with a smaller weakness. Let us recall (13) which states that the degree of the extended clauses along a path are either equal or exactly one smaller. On the other side the number of literals in the extended clauses along a path are always one smaller. So we conclude that the weakness of the extended clauses along a path are either equal or decrease. In order to determine the minimal weakness it is therefore sufficient to consider only the leaves of the graph, that is all extended clauses where the right hand side equals 1. So we need to investigate all strict reductions

∑_{i∈M} c_{i}L_{i} ≥ d − ∑_{i∈N\M} ,  (40)

where M ⊆ N such that ∑_{i∈M} c_{i} < d and c_{max(N\M)} + ∑_{i∈M} c_{i} ≥ d. The weakness of these extended clauses is |M| − 1 and we search for an M with a minimal cardinality. Obviously {1, …, β} is an M with minimal cardinality since ∑_{i=1}^{β} c_{i} ≥ ∑_{i∈M} c_{i} for all M satisfying (40). ⊓ ⊔

We can easily adopt our transformation method to generating only extended clauses having a weakness less than or equal to a given bound by applying Lemma 9.7 to every strict reduction we construct and abandon further reductions if the minimal weakness is greater than the bound. So by Lemma 9.7 we can filter out the generation of extended clauses that do not have a weakness less or equal the bound. Note that we avoid unnecessary computation of branches that do not lead to extended clauses that are strong enough.

A very popular and strong class of extended clauses that can so be generated are extended clauses with weakness 1. They are also called cliques or special ordered set constraints and have proven to be useful for preprocessing 0-1 integer programming problems. With the method presented here in combination with Lemma 9.7 we can generate extended clauses having an arbitrary weakness limit and generalize so existing methods that generate only cliques.

Another possibility is to generate only extended clauses from a pseudo-Boolean inequality containing a special subset of variables. Suppose that we have a clique inequality for some variables and have no extended clauses containing the remaining variables. So we are interested in generating extended clauses where these set of remaining variables V occurs. Another interesting set of variables is the one with large coefficients in the objective function, since they are mainly responsible for the resulting objective function value.

Name  # Ineqs # Clauses # Nodes PrePro Solve LP-Sol. Opt.
p0033-Original  11  4  9685  0.00 59.89 2520.57 3089
p0033-Normal  11  4  1289  0.00  6.47 2819.36 3089
p0033-Simple  2  80  124  0.04  1.42 2846.00 3089
p0040-Original  23  20  96  0.00  0.55 61796.54 62027
p0040-Normal  23  20  59  0.00  0.32 61829.08 62027
p0040-Simple  0  24  0  0.03  0.05 62027.00 62027
p0201-Original  33  100  5238  0.00 167.95 6875.00 7615
p0201-Normal  33  100  2775  0.00 90.42 7125.00 7615
p0201-Simple F  30  106  2273  0.33 84.83 7125.00 7615
p0201-WL(9) F  30  112  1258  0.43 47.47 7125.00 7615
p0548-Original  89^{1}  63  &  0.00  &  315.25 8691
p0548-Normal  89  63  &  0.02  & 4568.75 8691
p0548-Simple F  52  508  &  0.54  & 6617.47 8691
p0548-WL(1) CR F  52  672  &  8.10  & 7306.68 8691
p2756-Original  378^{2}  352  &  0.00  & 2688.75 3124
p2756-Normal  378  352  &  2.35  & 2701.14 3124
p2756-WL(1) CR F  343  2096  & 256.50  & 2701.75 3124
lseu-Original  11  17  55526  0.00 791.60  834.68 1120
lseu-Normal  11  17  28551  0.00 465.65  944.75 1120
lseu-Simple  7  22  18032  0.00 275.02  985.54 1120

1 originally 176 but 10 inequalities are tautologies and 14 become tautologous after fixing 2 originally 755 but 6 inequalities are tautologies and 19 become tautologous after fixing & out of memory

Figure 5: Some Computational Results

We obtain valid extended clauses containing a special set V of variables if we transform a strict reduction of the pseudo-Boolean inequality, where we have eliminated in advance all literals containing the variables that are not in V. Another reason to transform a strict reduction and not the whole pseudo-Boolean inequality is given if the pseudo-Boolean inequality contains some relatively large and some relatively small coefficients. The generated strongest extended clauses typically contain the literals with the largest coefficients and eliminating literals with small coefficients in advance focus on these strong extended clauses. Note that we can obtain strong extended clauses also by restricting the weakness as showed at the beginning of this section. By eliminating literals in advance we reduce the size of the search tree of the transformation method but in exchange only approximate the strongest extended clauses. The approach can be used if the pseudo-Boolean inequalities are too large to be transformed completely.

9.2.3 Computational Results

We have tested the preprocessing approach on some pure 0-1 integer programming problems found in MIPLIB [BBI92]. For the format of the figures see Sect. 9.2.1, page 44. Additionally we denote by “F” whether variables have been fixed using the fixing procedure presented in Sect. 7 and with “WL(w)” that for the non simple inequalities the generation of extended clauses has been limited to the maximal weakness w.

We obtain promising results on the smaller examples of the “pxxxx” problem set [CJP83] since these are sparse problems and considering each inequality on its own is promising under this premise. On dense problems we can not expect similar improvements. We denote by “CR” whether coefficient reduction, as presented in Sect. 8.1 has been successfully applied to problem. Coefficient reduction is tried on the literal with the largest coefficient in each pseudo-Boolean inequality that can not be simply transformed. The set of extended clauses that is used for the coefficient reduction is the set of extended clauses generated by the transformation of all simple pseudo-Boolean inequalities. Coefficient reduction was not very successful in the preprocessing phase^{6}.

The presented techniques can be used in a preprocessing phase when solving 0-1 integer programming problems. They have shown to be useful on sparse problems. Significant speedups can be obtained when the optimal solution of the linear programming relaxation of the partially transformed problem is better than in the original problem. In the context of 0-1 integer optimization we generalized the generation of clique inequalities (extended clauses with weakness 1) to the generation of extended clauses with an arbitrary weakness limit. The transformation method can also be used as a cut generator in a branch-and-bound algorithm. When searching an extended clause violating the fractional solution of the current linear programming relaxation we can extract just the needed extended clause. With the given redundancy criteria we assure that we select the best possible extended clause. Assume for example that the variables A, B have the fractional value 0.5 in the current LP-solution and that a pseudo-Boolean inequality cL ≥ d of the constraint set dominates the non redundant extended clause A + B + C ≥ 2, that is A + B + C ≥ 2 is in SCP(SRed(cL ≥ d)). A naive approach is to just add the extended clause A + B ≥ 1 which is also in SCP(SRed(cL ≥ d)). Because of the redundancy criteria we choose A + B + C ≥ 2 and so forbid further fractional solutions, among them for example B = C = 0.5.

Note that the main feature of the transformation method is that on the obtained set of extended clauses the deductive system “Generalized Resolution” [Hoo92] can be applied. So information coming from several pseudo-Boolean inequalities are used and may lead to stronger extended clauses. In [Bar94] we investigate the strengthening of extended clauses by using a restricted version of “Generalized Resolution”. The output of the transformed and strengthened constraint set can be stored in a table and extended clauses serving as cuts can then be selected by need from the branch-and-cut algorithm. This is subject to further research.

10 Conclusion

The nice properties of extended clauses — that the domination relation is easily decidable and 0-1 solutions spaces can be represented more compactly than with classical clauses — suggests to use them as basic formulas of the constraint solver for CLP(PB), a constraint logic programming language over pseudo-Boolean constraints. We have presented a method for transforming an arbitrary linear pseudo-Boolean inequality into a minimal set of extended clauses while preserving the 0-1 solution space. Although we may generate an exponential number of extended clauses, the method generates significantly fewer extended clauses than a transformation into classical clauses. With the presented transformation method we can deal with pseudo-Boolean inequalities arising in practical applications. This has been achieved by developing specialized strong redundancy criteria that efficiently ensure that the set of generated extended clauses is minimal. The compact representation of pseudo-Boolean inequalities and extended clauses speeds up the transformation process, and so allows to process even very large pseudo-Boolean inequalities with special structure. Direct manipulation of the compact representations of extended clauses is the subject of further research. Simplification methods that take into account that pseudo-Boolean inequalities are typically part of a set of constraints are presented and the transformation method is generalized to constrained transformation.

6We feel that coefficient reduction would be more successful when applied on the pseudo-Boolean inequalities constructed while exploring the branch and bound tree of CPLEX, since then some literals are fixed and so better bounds may be obtained for the simpler pseudo-Boolean inequalities.

Reformulation of a linear 0-1 inequality into a set of extended clauses is motivated by the idea of solving 0-1 problems with the deductive method “Generalized Resolution” [Hoo92] in the context of constraint logic programming. We feel that the use of extended clauses for representing 0-1 solution spaces arising from combinatorial problems is suitable. Future research consists of adapting “Generalized Resolution” for extended clauses as a constraint solver for pseudo-Boolean constraints.

References

[Bar93] P. Barth. Linear 0-1 inequalities and extended clauses. In Logic Programming and Automated Reasoning : international conference LPAR ’93; St. Petersburg, Russia; proceedings, July 1993.

[Bar94] P. Barth. Simplifying clausal satisfiability problems. submitted, 1994.

[BB93] P. Barth and A. Bockmayr. Solving 0-1 problems in CLP(PB). In Proc. 9th Conf. Artificial Intelligence for Applications (CAIA), Orlando. IEEE, 1993.

[BBI92] R.E. Bixby, E.A. Boyd, and R. Indovina. MIPLIB: A Test Set of Mixed-Integer Programming Problems. SIAM News, 25(16), 1992.

[BM84] E. Balas and J. B. Mazzola. Nonlinear 0-1 programming: I. Linearization techniques. Mathematical Programming, 30:1–21, 1984.

[Boc93] A. Bockmayr. Logic programming with pseudo-Boolean constraints. In F. Benhamou and A. Colmerauer, editors, Constraint Logic Programming - Selected Research, chapter 18, pages 327 – 350. MIT Press, 1993.

[CD93] P. Codognet and D. Diaz. Boolean constraint solving using clp(FD). In D. Miller, editor, Logic Programming. Proceedings of the 1993 international symposium, 1993.

[CJP83] H. Crowder, E.L. Johnson, and M. Padberg. Solving large-scale zero-one linear programming problems. Operations Research, 31(5):803–834, September 1983.

[DEC93] B.L. Dietrich, L.F. Escudero, and F. Chance. Efficient reformulation for 0-1 pograms - methods and compuational results. Discrete Applied Mathematics, 42:147–175, 1993.

[GG80] D. Granot and F. Granot. Generalized covering relaxation for 0-1 programs. Operations Research, 28:1442–1450, 1980.

[GH71] F. Granot and P. L. Hammer. On the use of boolean functions in 0-1 programming. Methods of Operations Research, 12:154–184, 1971.

[Hoo88] J. N. Hooker. A quantitative approach to logical inference. Decision Support Systems, 4:45 – 69, 1988.

[Hoo89] J. N. Hooker. Input proofs and rank one cutting planes. ORSA Journal for Computing, 1:137 – 145, 1989.

[Hoo92] J. N. Hooker. Generalized resolution for 0-1 linear inequalities. Annals of Mathematics and Artificial Intelligence, 6:271–286, 1992.

[HR68] P.L. Hammer and S. Rudeanu. Boolean Methods in Operations Research and Related Areas. Springer-Verlag, 1968.

[Jac92] Peter Jackson. Computing prime implicates incrementally. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, pages 253–267, Saratoga Springs, NY, June 1992. Springer LNAI 607.

[JKS85] E.L. Johnson, M. Kostreva, and U.H. Suhl. Solving 0-1 integer programming problems arising from large scale planning models. Operations Research, 33(4):803–819, July 1985.

[JL87] J. Jaffar and J.-L. Lassez. Constraint logic programming. In Proc. 14th ACM Symp. Principles of Programming Languages, Munich, 1987.

[NW88] G. L. Nemhauser and L. A. Wolsey. Integer and Combinatorial Optimization. Series in Discrete Mathematics and Optimization. Wiley–Interscience, 1988.

[Rob65] J.A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.

[Smo94] Gert Smolka. A calculus for higher-order concurrent constraint programming with deep guards. Research Report RR-94-03, Deutsches Forschungszentrum für Künstliche Intelligenz, Stuhlsatzenhausweg 3, D-66123 Saarbrücken, Germany, February 1994.

[SR90] V. A. Saraswat and M. Rinard. Concurrent constraint programming. In 17th Annual ACM Symp. Principles of Programming Languages, San Francisco, 1990.

[VH89] P. Van Hentenryck. Constraint satisfaction in logic programming. MIT Press, 1989.

Index

□, 4 ⊧, see domination ⊤, see tautology 0-1 inequality, see pseudo-Boolean inequality

assignment, 4

branch-and-bound, 43 branch-and-cut, 48

classical clause, 2 clique inequality, 35, 46 CLP(PB), 2 coefficient reduction, 6, 30–33, 45 compact representation, 21 context, 29 CP, see cutting plane CPLEX, 44

c reduce, 32

cutting plane, 8, 43, 48

domination, 7, 12, 45

expand, 22 Ext, see extension extended clause, 2, 4

degree, 4

normal form of sets, 8 strongest, 8, 9, 23 valid, 8

extended cover inequality, 43 extension, 7

fix, 26
fixed, 26

fixed literals, 24

fixing, 28

Generalized Resolution, 2, 40

get beta, 19

greedy heuristic, 32

integer rounding, 8, 40

knapsack problem, 7 linear combination, 8, 40 linear programming relaxation, 25, 27, 43 linearization, 3

                                            lower bound, 32

minimal cover, 43 MIPLIB, 29, 44

                                            o reduce, 31

path, 12

                                            pbul, 27
                                            pbur, 26

preprocessing, 43 prime, 2, 3, 12 product, 4 pseudo-Boolean inequality, 5

normal form, 5 valid, 7

unit relaxation, 27 unit resolution, 26, 38

reduction, 7

strict, 7, 10 constrained, 34 graph view, 12 redundancy, 12–18, 36, 40 resolution, 40 restriction, 45

SCP, see extended clause, strongest simplification, 29 solved form, 2 SRed, see reduction, strict

                                            sumfixed, 31

symmetry, 21–24

tautology, 4, 5

                                            transform, 20

transformation, 3, 11, 18, 20, 23, 41, 44 constrained, 36

ul, 25 unit

clause, 25 literal, 25 resolution, 25

unit literal, 26 unit relaxation, 24 ur, 25

ures, 25

weakness, 45