Logic Programming with Pseudo-Boolean Constraints

Alexander Bockmayr

MPI–I–91–227 April/December 1991 Author’s Address

Alexander Bockmayr, Max-Planck-Institut für Informatik, Im Stadtwald, D-6600 Saarbrücken, bockmayr@mpi-sb.mpg.de

Publication Notes

The present report has been submitted for publication elsewhere and will be copyrighted if accepted.

Acknowledgements

I would like to thank Peter Barth, David Basin and Harald Ganzinger for their comments on a preliminary version of this paper.

Abstract

Boolean constraints play an important role in various constraint logic programming languages. In this paper we consider pseudo-Boolean constraints, that is equations and inequalities between pseudo-Boolean functions. A pseudo-Boolean function is an integer-valued function of Boolean variables and thus a generalization of a Boolean function. Pseudo-Boolean functions occur in many application areas, in particular in problems from operations research. An interesting connection to logic is that inference problems in propositional logic can be translated into linear pseudo-Boolean optimization problems. More generally, pseudo-Boolean constraints can be seen as a particular way of combining two of the most important domains in constraint logic programming: arithmetic and Boolean algebra.

In this paper we define a new constraint logic programming language CLP(PB) for logic progamming with pseudo-Boolean constraints. The language is an instance of the general constraint logic programming language scheme CLP(X) and inherits all the typical semantic properties. We show that any pseudo-Boolean constraint has a most general solution and give variable elimination algorithms for pseudo-Boolean unification and unconstrained pseudo-Boolean optimization. Both algorithms subsume the wellknown Boolean unification algorithm of Büttner and Simonis.

Keywords

Constraint Logic Programming, Operations Research, Pseudo-Boolean Unification, Pseudo-Boolean Optimization, 0-1 Programming

Contents

1 Introduction 2 2 Boolean and Pseudo-Boolean Functions 3 3 Logic Programming with Pseudo-Boolean Constraints 7 4 Solving Pseudo-Boolean Constraints 8

4.1 A Variable Elimination Algorithm for Pseudo-Boolean Unification . . . . . . . . . . 8 4.2 Solving Arbitrary Pseudo-Boolean Constraints . . . . . . . . . . . . . . . . . . . . . 11

5 Pseudo-Boolean Optimization 11 5.1 The Basic Algorithm for Pseudo-Boolean Optimization . . . . . . . . . . . . . . . . . 12 5.2 The Special Version of the Basic Algorithm . . . . . . . . . . . . . . . . . . . . . . . 16

6 Example 17 7 Conclusion and Further Research 18 A Tree-Width of a Graph 20

1 Introduction

Boolean constraints play an important role in various constraint logic programming languages [Col87, DvHS^{+}88, ASS^{+}88]. In this paper we consider pseudo-Boolean constraints, that is equations and inequalities between pseudo-Boolean functions. A pseudo-Boolean function is an integer-valued function f : {0, 1}^{n} → Z and thus generalizes the notion of a Boolean function f : {0, 1}^{n} → {0, 1}.

Pseudo-Boolean functions have been studied for a long time [HR68]. There exist many interesting methods and results on the solution of pseudo-Boolean constraints that have been developed mainly in the area of operations research. It seems very natural to apply these techniques in the context of constraint logic programming. A constraint logic programming language can be considerably enhanced by allowing pseudo-Boolean constraints. Many problems from various application areas can be expressed very naturally using pseudo-Boolean functions.

Consider for example the following knapsack problem. Suppose there is a vessel with capacity w and goods g_{i} with weight w_{i} and value v_{i} for i = 1, …, 12. We introduce a Boolean variable X_{i}, i = 1, …, 12, which indicates whether or not the good g_{i} is loaded on the vessel. The possible cargos not exceeding the capacity of the vessel can be determined by the following Horn clause involving a pseudo-Boolean constraint

        cargo(X1,. . .,X12) :-
                     w1*X1 +. . . + w12*X12 ≤ w.

If we want to find the most valuable cargo, this can be done using a metapredicate max/2 that maximizes a pseudo-Boolean function subject to some pseudo-Boolean constraint.

        most-valuable-cargo(X1,. . .,X12) :-
                            max(v1*X1 +. . . + v12*X12, cargo(X1,. . .,X12)).

An interesting connection between logic and pseudo-Boolean optimization is that inference problems in propositional logic can be translated into linear pseudo-Boolean optimization problems.

For example, suppose we want to know whether X_{2} is implied by the set of clauses

X_{1} ∨ X_{2} ∨ X_{3},
\overline{X}_{1} ∨ X_{2} ∨  \overline{X}_{4},
\overline{X}_{1} ∨  X_{3},
\overline{X}_{1} ∨  \overline{X}_{3} ∨ X_{4},
X_{1} ∨  \overline{X}_{3}  ?

In order to solve this problem we may minimize X_{2} subject to

+X_{1} +X_{2} +X_{3}  ≥ 1,
−X_{1} +X_{2}  −X_{4} ≥ 1 − 2,
−X_{1} +X_{3} ≥ 1 − 1,
−X_{1}  −X_{3} +X_{4} ≥ 1 − 2,
+X_{1}  −X_{3}  ≥ 1 − 1

The logical implication holds if and only if the minimum of X_{2} is equal to 1.

There are many remarkable parallels between theorem proving and mathematical programming. The logical concepts of resolution, extended resolution, input and unit refutation, the Davis-Putnam-Procedure, and drawing of inferences pertinent to a given topic are closely related to the mathematical concepts of cutting planes, Chvátal’s method, elementary closure, branch and bound, and projection of a polytope, respectively (see [Hoo88] for a survey).

More generally, pseudo-Boolean constraints can be seen as a particular way of combining two of the most important domains in constraint logic programming: arithmetic and Boolean algebra.

So far we considered only linear pseudo-Boolean functions. In many applications however one has to deal with non-linear functions and non-linear constraints. For example, suppose that we want to model the interaction of n objects ob_{1}, ob_{2}, …, ob_{n}, each of which can be chosen (X_{i} = 1) or not (X_{i} = 0). For any pair of objects (ob_{i}, ob_{j}) let a_{ij} measure the interaction between ob_{i} and ob_{j}. If the global interaction is given by the sum of the interactions between all pairs of chosen objects, then it can be written as a quadratic pseudo-Boolean function ∑_{i=1}^{n} ∑_{j=1}^{n} a_{ij}X_{i}X_{j} of the n variables X_{1}, …, X_{n}. Maximizing or minimizing the global interaction means maximizing or minimizing this pseudo-Boolean function.

Typical applications of non-linear pseudo-Boolean functions include sequencing problems, timetable scheduling, coding theory, plant location [HR68], inter-city traffic [Rhy70], kinetic energy in spin-glass models [KGV83], or supply support of space stations [FGGB66].

The organization of the paper is as follows: We start in Section 2 with some basic facts about Boolean and pseudo-Boolean functions. In Section 3 we define a new constraint logic programming language CLP(PB) for logic progamming with pseudo-Boolean constraints which is an instance of the general constraint logic programming language scheme CLP(X). In Section 4 we present some of the ideas that can be used in order to solve pseudo-Boolean constraints. We show that any system of pseudo-Boolean constraints has a most general solution and give a variable elimination algorithm for computing most general pseudo-Boolean unifiers. In Section 5 we consider the problem of optimizing pseudo-Boolean functions. We present a variable elimination algorithm for pseudo-Boolean optimization and discuss its relationship to the well-known Boolean unification algorithm of Büttner and Simonis [BS87]. In Section 6 we give a typical example for the application of our concepts. Finally, Section 7 contains the conclusion and a discussion of further work.

2 Boolean and Pseudo-Boolean Functions

We begin with some basic facts about Boolean and pseudo-Boolean functions. At some places we will use the terminology of equational logic (see [HO80] for additional information).

Definition 1 A Boolean function is a mapping f : {0, 1}^{n} → {0, 1}.

A pseudo-Boolean function is a mapping g : {0, 1}^{n} → Z where Z denotes the ring of integer numbers.

If g : {0, 1}^{n} → Z is a pseudo-Boolean function, then the Boolean function g^{≠} : {0, 1}^{n} → {0, 1} defined by

g^{≠}(X_{1}, …, X_{n}) = \{ \begin{matrix}1 & if g(X_{1}, …, X_{n}) ≠ 0 \\ 0 & if g(X_{1}, …, X_{n}) = 0 \end{matrix}

is called the reduct of g.

Next we introduce a signature that allows to express Boolean and pseudo-Boolean functions as terms.

Definition 2 Consider the order-sorted signature with two sort symbols bool ⊆ integer and the sets of function symbols

F_{bool} = \{0, 1 :→ bool, \overline{·} : bool → bool
⊕, ∧, ∨ : bool × bool → bool}
F_{psbool} = {0, 1 :→ integer,
+, ∗ : integer × integer → integer,
− : integer → integer}

Let

V_{bool} = {X, Y, Z, X_{1}, X_{2}, …}
V_{integer} = {x, y, z, x_{1}, x_{2}, …}

denote countably infinite sets of variables of sort bool and integer. The terms in the term algebra T (F_{bool}, V_{bool}) are called Boolean terms and those in T (F_{psbool}, V_{bool}) pseudo-Boolean terms.

By interpreting \overline{·} as negation, ⊕ as sum modulo 2, ∧ as conjunction, and ∨ as disjunction, any Boolean term t ∈ T (F_{bool}, V_{bool}) containing n variables generates a n-ary Boolean function t̂: {0, 1}^{n} → {0, 1}. Similarly, by interpreting the function symbols +, ∗, − as the usual arithmetical operations on integer numbers any pseudo-Boolean term t ∈ T (F_{psbool}, V_{bool}) containing n variables generates a n-ary pseudo-Boolean function t̂: {0, 1}^{n} → Z.

For example, the Boolean term X ⊕ Y ⊕ X ∧ Y generates the Boolean function f : {0, 1}^{2} → {0, 1}, f(0, 0) = 0, f(0, 1) = f(1, 0) = f(1, 1) = 1. The pseudo-Boolean term X+Y +X∗Y generates the pseudo-Boolean function g : {0, 1}^{2} → Z, g(0, 0) = 0, g(0, 1) = g(1, 0) = 1, g(1, 1) = 3.

Conversely, any Boolean or pseudo-Boolean function has a canonical term representation, the polynomial normal form, which is introduced in the next proposition.

Proposition 3 1. For any Boolean function f : {0, 1}^{n} → {0, 1} there is up to associativity and commutativity of ⊕, ∧ a unique Boolean term of the form

⨁_{I∈Ω} ⋀_{i∈I} X_{i},  (1)

with a collection Ω of subsets of {1, …, n}, that generates f.

2. For any pseudo-Boolean function g : {0, 1}^{n} → Z there is up to associativity and commutativity of +, * a unique pseudo-Boolean term of the form

∑_{I∈Ω} c_{I} ∏_{i∈I} X_{i},  (2)

with a collection Ω of subsets of {1, …, n} and coefficients c_{I} ∈ Z \ {0}, that generates g.

Proof: See [HR68] □

Example 4 The function g : {0, 1}^{3} → Z defined by the table

X Y Z g(X,Y,Z)
0 0 0  -5
0 0 1  0
0 1 0  0
0 1 1  0
1 0 0  -3
1 0 1  8
1 1 0  0
1 1 1  6

has the polynomial normal form

g(X, Y, Z) = −5 + 2X + 5Y + 5Z − 2XY + 6XZ − 5Y Z

Note that there exist also other representations, for example

g(X, Y, Z) = 2X\overline{Y} + 6XZ − 5\overline{Y} \overline{Z},

where \overline{X} is an abbreviation for 1 − X.

In order to obtain a syntactic characterization of those terms that generate the same function we need equational theories for Boolean and pseudo-Boolean terms. An equational theory is a congruence relation ≡_{E} on the term algebra which is generated by a set of equations E. For two terms s, t we have s ≡_{E} t if and only if s and t can be proven equal using the equations in E [HO80].

Definition 5 1. The equational theory ≡_{B} of Boolean terms is generated by the set of equations

B = {X ⊕ (Y ⊕ Z) ≐ (X ⊕ Y) ⊕ Z,
X ⊕ 0 ≐ X,
X ⊕ X ≐ 0,
X ⊕ Y ≐ Y ⊕ X,
X ∧ (Y ∧ Z) ≐ (X ∧ Y) ∧ Z,
X ∧ 1 ≐ X,
X ∧ Y ≐ Y ∧ X,
X ∧ (Y ⊕ Z) ≐ (X ∧ Y) ⊕ (X ∧ Z),
X ∧ X ≐ X,
\overline{X} ≐ X ⊕ 1,
X ∨ Y ≐ (X ⊕ Y) ⊕ X ∧ Y }

2. The equational theory ≡_{P B} of pseudo-Boolean terms is generated by the set of equations

P B = {x + (y + z) ≐ (x + y) + z,
x + 0 ≐ x,

x + (−x) ≐ 0,
x + y ≐ y + x,
x ∗ (y ∗ z) ≐ (x ∗ y) ∗ z,
x ∗ 1 ≐ x,
x ∗ y ≐ y ∗ x,
x ∗ (y + z) ≐ (x ∗ y) + (x ∗ z),
X ∗ X ≐ X}

The next proposition shows that two terms denote the same function iff they are congruent modulo the equational theory ≡_{P B} or ≡_{B} respectively.

Proposition 6 1. Two Boolean terms s, t ∈ T (F_{bool}, V_{bool}) generate the same Boolean function

iff they are congruent modulo the theory B, that is ŝ = t̂ iff s ≡_{B} t.

2. Two pseudo-Boolean terms s, t ∈ T (F_{psbool}, V_{bool}) generate the same pseudo-Boolean function iff they are congruent modulo the theory P B, that is ŝ = t̂ iff s ≡_{P B} t.

Proof: We prove only the second part of the theorem. The first part is completely analogous.

“⟸”: If s ≡_{P B} t, then by the well-known theorem of Birkhoff [HO80] the equation s ≐ t holds in all models of the set of equations P B, in particular in the algebra ({0, 1}, Z). This means that for any variable assignment σ : V_{bool} → {0, 1} the terms s and t have the same value. This is equivalent to say that the pseudo-Boolean functions generated by s and t are the same.

“⟹”: Using the equations in P B we may transform the pseudo-Boolean terms s, t to pseudo-Boolean terms s↓ ≡_{P B} s and t↓ ≡_{P B} t such that s↓ and t↓ are of the form (2). From “⟸” we deduce that ŝ = ŝ↓ and t̂= t̂↓. From the preceding proposition and the assumption ŝ = t̂ we know that s↓ and t↓ are the same up to associativity and commutativity of +, ∗. This implies s↓ ≡_{P B} t↓ and consequently s ≡_{P B} t. □

Boolean functions can be described by both Boolean and pseudo-Boolean terms. A canonical transformation between the two representations is given in the next definition.

Definition 7 The pseudo-Boolean form t^{P} ∈ T (F_{psbool}, V_{bool}) of a term t ∈ T (F_{bool} ∪ F_{psbool}, V_{bool}) is obtained by normalizing t using the canonical term rewrite system

P = {X ⊕ Y → X + Y − (X ∗ Y + X ∗ Y),
X ∧ Y → X ∗ Y,
\overline{X} → 1 − X,
X ∨ Y → X + Y − X ∗ Y }

Lemma 8 For any Boolean term t ∈ T (F_{bool}, V_{bool}) the functions generated by t and t^{P} agree, that is t̂= t̂^{P}.

Proof: The equations X ⊕ Y ≐ X + Y − (X ∗ Y + X ∗ Y), X ∧ Y ≐ X ∗ Y, \overline{X} ≐ 1 − X, X ∨ Y ≐ X + Y − X ∗ Y hold in the algebra ({0, 1}, Z). This implies ({0, 1}, Z) ⊧ t ≐ t^{P} and we get t̂= t̂^{P}. □ Lemma 9 Let s, t ∈ T (F_{bool}, V_{bool}) be two Boolean terms. Then s ≡_{B} t iff s^{P} ≡_{P B} t^{P}.

Proof: By proposition 6 we have s ≡_{B} t iff ŝ = t̂. By the preceding lemma ŝ = ŝ^{P} and t̂ = t̂^{P}. Again by proposition 6, s^{P} ≡_{P B} t^{P} iff ŝ^{P} = t̂^{P}. Altogether this yields s ≡_{B} t iff ŝ = t̂ iff ŝ^{P} = t̂^{P} iff s^{P} ≡_{P B} t^{P}. □

We close this section by an easy lemma that we will need several times in the sequel.

Lemma 10 Suppose f, g : {0, 1}^{n} → Z are pseudo-Boolean functions and u : {0, 1}^{n} → {0, 1} is a Boolean function. Then f ∗ u + g ∗ \overline{u} = 0 implies f ∗ u = g ∗ \overline{u} = 0 and f ∗ g = 0.

Proof: Assume f ∗ u + g ∗ \overline{u} = 0. Multiplying this equation with u yields 0 = f ∗ u ∗ u + g ∗ \overline{u} ∗ u = f ∗ u. In the same way, multiplication with \overline{u} yields 0 = f ∗ u ∗ \overline{u} + g ∗ \overline{u} ∗ \overline{u} = g ∗ \overline{u}. Finally, f ∗ g = f ∗ g ∗ (u + \overline{u}) = f ∗ g ∗ u + f ∗ g ∗ \overline{u} = 0 + 0 = 0. □

3 Logic Programming with Pseudo-Boolean Constraints

We now introduce a constraint logic programming language CLP(PB) over an algebraic structure P B that allows us to handle equations and inequalities between pseudo-Boolean functions. The language is an instance of the constraint logic programming language scheme CLP(X) of [JL86, JL87].

The algebraic structure in question is the order-sorted algebra P B over the signature Σ = (S, F, P) with

S = {bool ⊆ integer ⊆ tree}
F = F_{bool} ∪ F_{psbool} ∪ {f_{i} : tree^{n_{i}} → tree | i = 1, …, k, k ≥ 0, n_{i} ≥ 0}
P = {≐: tree × tree → tree, ≤, <, ≥, >: integer × integer → integer}

where the interpretation of the sort, function and predicate symbols is the usual one.

V = V_{bool} ∪ V_{integer} ∪ V_{tree} denotes a collection of countably infinite sets of variables of the different sorts.

An atomic pseudo-Boolean constraint is of the form

s ≐ t, u ≤ v, u < v, u ≥ v, or u > v

with terms s, t ∈ T (F, V) and pseudo-Boolean terms u, v ∈ T (F_{psbool}, V_{bool}). A pseudo-Boolean constraint is a possibly empty finite set of atomic constraints.

An atom is of the form p(t_{1}, …, t_{n}) where p is a predicate symbol distinct from ≐, ≤, <, ≥, > and t_{i} ∈ T (F, V), i = 1, …, n, n ≥ 0, are terms.

A CLP(PB) constraint logic program is defined over a signature Σ^{⋆} = (S, F, P^{⋆}) where P^{⋆} ∩P = Ø. It consists of a finite set of constraint rules each being of the form

H :- c ∥ B_{1}, …, B_{n}

where c is a possibly empty pseudo-Boolean constraint and H, B_{i}, i = 1,…,n, n ≥ 0, are atoms over Σ^{⋆}.

A CLP(PB) goal is of the form

? − c ∥ B_{1}, …, B_{n}

where again c is a possibly empty pseudo-Boolean constraint and B_{i}, i = 1,…,n, n ≥ 0, are atoms over Σ^{⋆}.

The structure P B is solution compact because it has no limit elements. From the general results of [JL86, JL87] we can derive for the language CLP(PB):

• the existence of a canonical domain of computation

• the existence of a least and greatest model semantics

• the existence of a least and greatest fixpoint semantics

• soundness and completeness results for successful derivations of the underlying implementation model

• soundness and completeness results for finitely failed derivations of the underlying implementation model

• soundness and completeness results for negation as failure

4 Solving Pseudo-Boolean Constraints

In this section we describe how we may solve arbitrary pseudo-Boolean constraints. A detailed account of this subject is beyond the scope of this paper. We will restrict ourselves mainly to the case of equality constraints. In addition, we show how arbitrary pseudo-Boolean constraints can be reduced to pseudo-Boolean equations. However, such a reduction is mainly of theoretical interest. In practice, it will be more efficient to handle non-equality constraints by a specific solving procedure.

4.1 A Variable Elimination Algorithm for Pseudo-Boolean Unification

Definition 11 A pseudo-Boolean unification problem is a system of equations

S : s_{1} ≐ t_{1}, …, s_{n} ≐ t_{n}

with pseudo-Boolean terms s_{i}, t_{i} ∈ T (F_{psbool}, V_{bool}), i = 1, …, n. A pseudo-Boolean unifier of S is a substitution τ : V_{bool} → T (F_{bool}, V_{bool}) such that

τ(s_{i})^{P} ≡_{P B} τ(t_{i})^{P} , for all i = 1, …, n.

A most general pseudo-Boolean unifier of S is a substitution σ : V_{bool} → T (F_{bool}, V_{bool}) such that for all pseudo-Boolean unifiers τ of S there is a substitution λ : V_{bool} → T (F_{bool}, V_{bool}) with

λ(σ(X)) ≡_{B} τ(X), for all X ∈ V_{bool}.

Now we want to give a constructive proof that, similar to syntactic unification in classical logic programming, any two unifiable pseudo-Boolean terms have a most general pseudo-Boolean unifier. In the terminology of unification theory this means that pseudo-Boolean terms form a unitary theory. The next theorem is a generalization of the well-known Boolean unification method of [BS87] to the pseudo-Boolean case. For the proof we use previous results by P. Hammer [Ham64a].

Theorem 12 Pseudo-Boolean unification is unitary, that is any two pseudo-Boolean terms are either not unifiable modulo P B or they have a most general pseudo-Boolean unifier.

Proof: It is sufficient to consider the pseudo-Boolean unification problem u ≐ 0, with a pseudo-Boolean term u ∈ T (F_{psbool}, V_{bool}). Let V ar(u) = {X_{1}, …, X_{n_{u}}} be the set of variables occurring in u. The proof uses induction on n_{u} and provides a decision procedure for the unifiability of u and 0 as well as an algorithm for computing a most general unifier.

To simplify our notation we will identify throughout the proof a Boolean or pseudo-Boolean term t with the corresponding function t̂. In particular, we will write s = t instead of ŝ = t̂. This is justified by the considerations in Section 2.

First let n_{u} = 0. If u = 0 then the empty substitution is a most general pseudo-Boolean unifier. and if u ≠ 0 then the equation is unsolvable.

Suppose now that the theorem is true for pseudo-Boolean terms which contain at most n variables, n ≥ 0, and let u be a pseudo-Boolean term with n + 1 variables. Select a variable X_{n+1} in u and write u in the form

u = v ∗ X_{n+1} + w ∗ \overline{X_{n+1}}

where {X_{1}, …, X_{n}}, n ≥ 0, are the only variables occurring in the pseudo-Boolean terms v, w. Let τ : V_{bool} → T (F_{bool}, V_{bool}) be a pseudo-Boolean unifier of u and 0. Then we have

τ(v) ∗ τ(X_{n+1}) + τ(w) ∗ \overline{τ(X_{n+1})} = 0.

From Lemma 10 we deduce that τ(v) ∗ τ(w) = τ(v ∗ w) = 0 or that τ is a pseudo-Boolean unifier of v ∗ w and 0.

Conversely, if ρ : V_{bool} → T (F_{bool}, V_{bool}) is a unifier of v ∗ w and 0, then

σ(X_{i}) =^{def} ρ(X_{i}), for i = 1, …, n
σ(X_{n+1}) =^{def} \overline{ρ(v^{≠})} ∧ Y ⊕ ρ(w^{≠}) ∧ \overline{Y} = \overline{ρ(v^{≠})} ∗ Y + ρ(w^{≠}) ∗ \overline{Y} ,

with a new variable Y ∈ V_{bool}, defines a pseudo-Boolean unifier of u and 0. In fact, we have

σ(u) = σ(v) ∗ σ(X_{n+1}) + σ(w) ∗ \overline{σ(X_{n+1})}
= ρ(v) ∗ (\overline{ρ(v^{≠})} ∗ Y + ρ(w^{≠}) ∗ \overline{Y}) + ρ(w) ∗ \overline{(\overline{ρ(v^{≠})} ∗ Y + ρ(w^{≠}) ∗ \overline{Y})}
= ρ(v) ∗ \overline{ρ(v^{≠})} ∗ Y + ρ(v) ∗ ρ(w^{≠}) ∗ \overline{Y} + ρ(w) ∗ (1 − \overline{ρ(v^{≠})} ∗ Y − ρ(w^{≠}) ∗ \overline{Y})
= 0 + 0 + ρ(w) − ρ(w) ∗ \overline{ρ(v^{≠})} ∗ Y − ρ(w) ∗ ρ(w^{≠}) ∗ \overline{Y}
= ρ(w) − ρ(w) ∗ (1 − ρ(v^{≠})) ∗ Y − ρ(w) ∗ (1 − Y)
= ρ(w) − ρ(w) ∗ Y + ρ(w) ∗ ρ(v^{≠}) ∗ Y − ρ(w) + ρ(w) ∗ Y = 0

Here, we have used the identities ρ(v) ∗ \overline{ρ(v^{≠})} = 0, 0 = ρ(v) ∗ ρ(w) = ρ(v^{≠}) ∗ ρ(w) = ρ(v) ∗ ρ(w^{≠}) = ρ(v^{≠}) ∗ ρ(w^{≠}), and ρ(w) ∗ ρ(w^{≠}) = ρ(w).

Solved  \frac{\{u ≐ 0\}}{true}

if u ≡_{P B} 0

Unsolvable  \frac{\{u ≐ 0\}}{fail}

if u ≢_{P B} 0 and V ar(u) = ∅

Variable Elimination \frac{\{u ≐ 0\}}{\{v ∗ w ≐ 0\} ∪ \{X ≐ \overline{v^{≠}} ∗ Y + w^{≠} ∗ \overline{Y} \}}

if u ≢_{P B} 0,

u ≡_{P B} v ∗ X + w ∗ \overline{X},

X ∉ V ar(v, w),

and Y is a new variable

Figure 1: Variable Elimination for Pseudo-Boolean Unification

It remains to show that if ρ is a most general pseudo-Boolean unifier of v ∗ w ≐ 0, then σ is a most general pseudo-Boolean unifier of u ≐ 0. Let τ be an arbitrary unifier of u and 0. The restriction τ′ of τ to the variables {X_{1}, …, X_{n}} unifies v ∗ w and 0. Consequently, there exists a substitution λ′ such that

τ′(X_{i}) = λ′(ρ(X_{i})), for all i = 1, …, n.

We define a substitution λ by

λ(X) =^{def} λ′(X), for X ∈ ⋃_{i=1,...,n} V ar(ρ(X_{i}))
λ(Y) =^{def} τ(X_{n+1}).

Now we get

λ(σ(X_{n+1})) = \overline{λ(ρ(v^{≠}))} ∗ λ(Y) + λ(ρ(w^{≠})) ∗ \overline{λ(Y)}
= \overline{λ′(ρ(v^{≠}))} ∗ τ(X_{n+1}) + λ′(ρ(w^{≠})) ∗ \overline{τ(X_{n+1})}
= \overline{τ(v^{≠})} ∗ τ(X_{n+1}) + τ(w^{≠}) ∗ \overline{τ(X_{n+1})}
= (1 − τ(v^{≠})) ∗ τ(X_{n+1}) + τ(w^{≠}) ∗ \overline{τ(X_{n+1})}
= τ(X_{n+1}) − τ(v^{≠}) ∗ τ(X_{n+1}) + τ(w^{≠}) ∗ \overline{τ(X_{n+1})}
= τ(X_{n+1}) − 0 + 0 = τ(X_{n+1})

The last equality holds, because τ is a unifier of u and 0. This means τ(v) ∗ τ(X_{n+1}) + τ(w) ∗ \overline{τ(X_{n+1})} = 0 which by Lemma 10 implies τ(v^{≠}) ∗ τ(X_{n+1}) = τ(w^{≠}) ∗ \overline{τ(X_{n+1})} = 0. Altogether we have shown that σ is a most general pseudo-Boolean unifier of u and 0. □

From the proof of the preceding theorem we derive a variable elimination algorithm for pseudo-Boolean unification which subsumes the Boolean unification algorithm [BS87]. Given a pseudo-Boolean term u, it computes a most general pseudo-Boolean unifier of u and 0 if it exists and fails otherwise (see Figure 1).

4.2 Solving Arbitrary Pseudo-Boolean Constraints

We show in this section how arbitrary pseudo-Boolean constraints can be reduced to equality constraints.

Lemma 13 The problem of solving a pseudo-Boolean inequality is reducible to that of solving a pseudo-Boolean equation.

Proof: It is enough to consider a pseudo-Boolean inequality of the form

g(X_{1}, …, X_{n}) ≤ 0.  (3)

The following proof was first given in [Ham64b]. Let g(X_{1}, …, X_{n}) = ∑_{I∈Ω} c_{I} ∏_{i∈I} X_{i} be a polynomial representation of g and let A =^{def} ∑_{c_{I}<0} c_{I}. Then A is a lower bound of the pseudo-Boolean function g. Let −A = a_{0}2^{0} + ⋯ + a_{k}2^{k}, k ≥ 0, be the binary representation of −A ≥ 0. The inequality (3) is equivalent to the equation

g(X_{1}, …, X_{n}) + y ≐ 0  (4)

with the additional restriction y ≥ 0. Therefore we may write y = Y_{0}2^{0} + ⋯ + Y_{l}2^{l}, l ≥ 0, and since y = −g(X_{1}, …, X_{n}) ≤ −A we get l ≤ k. It follows that (3) and (4) are equivalent to the pseudo-Boolean equation

g(X_{1}, …, X_{n}) + Y_{0}2^{0} + ⋯ + Y_{k}2^{k} ≐ 0  (5)

where in the case k > l we have Y_{l+1} = … = Y_{k} = 0. □

Lemma 14 The problem of solving a system of pseudo-Boolean equations is reducible to that of solving a single pseudo-Boolean equation.

Proof: The system s_{1} ≐ t_{1}, …, s_{n} ≐ t_{n}, n ≥ 1, is equivalent to the equation ∑_{i=1}^{n}(s_{i} − t_{i})^{2} ≐ 0. □

The two lemmas together yield

Proposition 15 The problem of solving an arbitrary pseudo-Boolean constraint is reducible to that of solving a single pseudo-Boolean equation.

5 Pseudo-Boolean Optimization

In the last section we have sketched a solution procedure for pseudo-Boolean constraints. In practical applications, one is often not interested in all solutions of a pseudo-Boolean constraint but only in those solutions which are optimal with respect to some objective function, which itself is a pseudo-Boolean function.

This leads to the problem of pseudo-Boolean optimization also known as nonlinear 0-1 programming.

Maximize the pseudo-Boolean function g(X_{1}, …, X_{n}) subject to the pseudo-Boolean constraint f(X_{1}, …, X_{n}) ≐ 0.

A constrained pseudo-Boolean optimization problem can be transformed to an unconstrained pseudo-Boolean optimization problem by first computing a most general solution

X_{1} = t_{1}(Y_{1}, …, Y_{m}), …, X_{n} = t_{n}(Y_{1}, …, Y_{m})

of the constraint f(X_{1}, …, X_{n}) ≐ 0 and then maximizing the pseudo-Boolean function

h(Y_{1}, …, Y_{m}) =^{def} g(t_{1}(Y_{1}, …, Y_{m}), …, t_{n}(Y_{1}, …, Y_{m})).

The unconstrained quadratic pseudo-Boolean maximization problem z ≐ max(g) with a quadratic pseudo-Boolean function g : {0, 1}^{n} → Z is NP-complete. As a matter of fact, most of the well-known NP-complete problems (for example the minimum cut problem, balancing a signed graph, maximum 2-satisfiability) can be very naturally formulated as unconstrained quadratic pseudo-Boolean optimization problems. The same is true for broad classes of constrained pseudo-Boolean optimization problems, such as the maximization of a linear function subject to a quadratic Boolean equation or the maximization of a quadratic function subject to a system of linear equations [HS86].

5.1 The Basic Algorithm for Pseudo-Boolean Optimization

There is an extensive literature on the solution of pseudo-Boolean optimization problems (see the survey [HS86]) that we cannot cover in this paper. Because of its close relationship to the variable elimination method for Boolean unification we present here a variant of the so-called Basic Algorithm for pseudo-Boolean optimization. This algorithm was originally proposed in [HRR63a, HRR63b] and allows to maximize an arbitrary nonlinear pseudo-Boolean function f : {0, 1}^{n} → Z.

First we define the notion of a most-general maximizer of a pseudo-Boolean function f.

Definition 16 Let f : {0, 1}^{n} → Z be a pseudo-Boolean function with the maximum value z ∈ Z. Let t_{f} ∈ T (F_{psbool}, V_{bool}) be a pseudo-Boolean term representing f. A (most general) maximizer of f (resp. t_{f}) is a (most general) pseudo-Boolean unifier of the pseudo-Boolean equation t ≐ z.

From Theorem 12 we can conclude that any pseudo-Boolean function f : {0, 1}^{n} → Z has a most general maximizer σ_{f} which subsumes any other maximizer τ of f. However, we cannot compute σ_{f} by the variable elimination algorithm for pseudo-Boolean unification, because we do not know a priori the maximum value of f. The Basic Algorithm for pseudo-Boolean optimization is a variable elimination method which computes simultaneously the maximum value z of f and a most general pseudo-Boolean unifier of the equation f ≐ z.

In order to formulate the algorithm we need the following definitions.

Definition 17 Let g : {0, 1}^{n} → Z be a pseudo-Boolean function. The pseudo-Boolean function g^{+} : {0, 1}^{n} → Z is defined by

g^{+}(X_{1}, …, X_{n}) =^{def} \{ \begin{matrix}g(X_{1}, …, X_{n}), & if g(X_{1}, …, X_{n}) > 0 \\ 0, & if g(X_{1}, …, X_{n}) ≤ 0. \end{matrix}

Constant  \frac{z ≐ max(u)}{z ≐ c}

if u ≡_{P B} c = constant

Variable Elimination \frac{z ≐ max(u)}{\{z ≐ max(v^{+} + w)\} ∪ \{X ≐ v^{=} ∗ X′ + v^{>}\}}

if u ≡_{P B} v ∗ X + w, X ∉ V ar(v, w), v ≢_{P B} 0, and X′ is a new variable

Figure 2: The Basic Algorithm for Pseudo-Boolean Optimization

Definition 18 Let g : {0, 1}^{n} → Z be a pseudo-Boolean function. The Boolean functions g^{=}, g^{>} : {0, 1}^{n} → {0, 1} are defined by

g^{=}(X_{1}, …, X_{n}) =^{def} \{ \begin{matrix}1, & if g(X_{1}, …, X_{n}) = 0 \\ 0, & if g(X_{1}, …, X_{n}) ≠ 0 \end{matrix}

and

g^{>}(X_{1}, …, X_{n}) =^{def} \{ \begin{matrix}1, & if g(X_{1}, …, X_{n}) > 0 \\ 0, & if g(X_{1}, …, X_{n}) ≤ 0 \end{matrix}

Now we can describe the Basic Algorithm by a set of inference rules (see Figure 2).

The correctness proof of the Basic Algorithm depends on the following two lemmas that relate a most general maximizer of a pseudo-Boolean function f = g ∗ X + h to a most general maximizer of g^{+} + h.

Lemma 19 Let f : {0, 1}^{n+1} → Z be a pseudo-Boolean function.

Suppose

f(X_{1}, …, X_{n+1}) = X_{n+1} ∗ g(X_{1}, …, X_{n}) + h(X_{1}, …, X_{n})

with pseudo-Boolean functions g, h : {0, 1}^{n} → Z. Then

max(f) = max(g^{+} + h).

If τ : {X_{1}, …, X_{n+1}} → T (F_{bool}, V_{bool}) is a maximizer of f then the restriction of τ to {X_{1}, …, X_{n}} is a maximizer of g^{+} + h.

Moreover, τ satisfies the condition τ(X_{n+1}) = τ(g^{=}) ∗ τ(X_{n+1}) + τ(g^{>}).

Proof: As before, we will not distinguish a pseudo-Boolean function f and the corresponding term t_{f}.

From f = X_{n+1}∗g+h ≤ X_{n+1}∗g^{+}+h ≤ g^{+}+h we get max(f) ≤ max(g^{+}+h). Let z ∈ Z denote the maximum value of g^{+} +h. Then there exist a_{1}, …, a_{n} ∈ {0, 1} such that (g^{+} +h)(a_{1}, …, a_{n}) =

z. Let a_{n+1} =^{def} g^{>}(a_{1}, …, a_{n}). Then f(a_{1}, …, a_{n+1}) = a_{n+1} ∗ g(a_{1}, …, a_{n}) + h(a_{1}, …, a_{n}) =

g^{+}(a_{1}, …, a_{n}) + h(a_{1}, …, a_{n}) = z. This implies max(f) ≥ max(g^{+} + h) and altogether we get max(f) = max(g^{+} + h) = z.

Now let τ : {X_{1}, …, X_{n+1}} → T (F_{bool}, V_{bool}) be a maximizer of f.

First we show that τ(X_{n+1}) = τ(g^{=}) ∗ τ(X_{n+1}) + τ(g^{>}). Otherwise there would exist a ground substitution γ : V_{bool} → {0, 1} such that (γ ∘ τ)(X_{n+1}) ≠ (γ ∘ τ)(g^{=}) ∗ (γ ∘ τ)(X_{n+1}) + (γ ∘ τ)(g^{>}). Since

(γ ∘ τ)(g^{=}) ∗ (γ ∘ τ)(X_{n+1}) + (γ ∘ τ)(g^{>}) = \{ \begin{matrix}1, & if (γ ∘ τ)(g) > 0 \\ (γ ∘ τ)(X_{n+1}), & if (γ ∘ τ)(g) = 0 \\ 0, & if (γ ∘ τ)(g) < 0 \end{matrix} ,

we get a contradiction in the case (γ ∘ τ)(g) = 0. In the two remaining cases we can derive

(γ ∘ τ)(X_{n+1}) = \{ \begin{matrix}0, & if (γ ∘ τ)(g) > 0 \\ 1, & if (γ ∘ τ)(g) < 0 \end{matrix} .

This is an obvious contradiction to the maximality of τ as we show now.

Define the substitution \overline{τ} : \{X_{1}, …, X_{n+1}\} → T (F_{bool}, V_{bool}) by

\overline{τ}(X_{i}) =^{def} (γ ∘ τ)(X_{i}), for i = 1, …, n
\overline{τ}(X_{n+1}) =^{def} \{ \begin{matrix}1, & if (γ ∘ τ)(g) > 0 \\ 0, & if (γ ∘ τ)(g) < 0 \end{matrix} .

Then \overline{τ}(f) = \overline{τ}(g ∗ X_{n+1} + h) = \overline{τ}(g) ∗ \overline{τ}(X_{n+1}) + \overline{τ}(h) = (γ ∘ τ)(g) ∗ \overline{τ}(X_{n+1}) + (γ ∘ τ)(g) > (γ ∘ τ)(g) ∗ (γ ∘ τ)(X_{n+1}) + (γ ∘ τ)(h) = (γ ∘ τ)(f) = γ(z) = z, in contradiction to the maximality of z. This allows us to conclude that τ(X_{n+1}) = τ(g^{=}) ∗ τ(X_{n+1}) + τ(g^{>}).

In order to show that the restriction of τ to {X_{1}, …, X_{n}} is maximizer of g^{+} + h, we must prove that τ(g^{+} + h) = z. Since we know that τ(f) = τ(X_{n+1}) ∗ τ(g) + τ(h) = z, it is enough to show that τ(X_{n+1}) ∗ τ(g) = τ(g^{+}). But, τ(X_{n+1}) ∗ τ(g) = (τ(g^{=}) ∗ τ(X_{n+1}) + τ(g^{>})) ∗ τ(g) = τ(g^{=}) ∗ τ(g) ∗ τ(X_{n+1}) + τ(g^{>}) ∗ τ(g) = 0 + τ(g^{+}) = τ(g^{+}), and the lemma is proved.

□

Lemma 20 Let f : {0, 1}^{n+1} → Z be a pseudo-Boolean function. Suppose

f(X_{1}, …, X_{n+1}) = X_{n+1} ∗ g(X_{1}, …, X_{n}) + h(X_{1}, …, X_{n})

with pseudo-Boolean functions g, h : {0, 1}^{n} → Z. Let ρ : V_{bool} → T (F_{bool}, V_{bool}) be a most general maximizer of the pseudo-Boolean function g^{+} + h. Then the substitution σ : V_{bool} → T (F_{bool}, V_{bool}),

σ(X_{i}) =^{def} ρ(X_{i}), for i = 1, …, n
σ(X_{n+1}) =^{def} ρ(g^{=}) ∧ Y ⊕ ρ(g^{>}) = ρ(g^{=}) ∗ Y + ρ(g^{>}),

with a new variable Y ∈ V_{bool}, defines a most general maximizer of f.

Proof: Again we do not distinguish a pseudo-Boolean function f and the corresponding term t_{f}. Let z ∈ Z be the maximum value of f. By Lemma 19, z is also the maximum value of g^{+} + h. This means that the substitution ρ is a most general pseudo-Boolean unifier of the equation g^{+} + h ≐ z. In particular, we get ρ(g^{+}) + ρ(h) = z. It follows that

σ(f) = σ(X_{n+1}) ∗ σ(g) + σ(h)
= (ρ(g^{=}) ∗ Y + ρ(g^{>})) ∗ ρ(g) + ρ(h)
= ρ(g^{=}) ∗ ρ(g) ∗ Y + ρ(g^{>}) ∗ ρ(g) + ρ(h)
= ρ(g^{=} ∗ g) ∗ Y + ρ(g^{>} ∗ g) + ρ(h)
= ρ(0) ∗ Y + ρ(g^{+}) + ρ(h)
= 0 + z = z.

Here we have used the identities g^{=} ∗ g = 0 and g^{>} ∗ g = g^{+}. This shows, that σ is a maximizer of f.

Let τ : V_{bool} → T (F_{bool}, V_{bool}) be an arbitrary maximizer of f, that is z = τ(f) = τ(X_{n+1}) ∗ τ(g)+τ(h). By Lemma 19, τ is also a maximizer of g^{+}+h. It follows that there exists a substitution λ′ : V_{bool} → T (F_{bool}, V_{bool}) such that λ′(ρ(X_{i})) = τ(X_{i}), for all i = 1, …, n.

We define a substitution λ by

λ(X) =^{def} λ′(X), for X ∈ ⋃_{i=1,...,n} V ar(ρ(X_{i}))
λ(Y) =^{def} τ(X_{n+1}).

Then we get λ(σ(X_{n+1})) = λ(ρ(g^{=})∗Y +ρ(g^{>})) = λ(ρ(g^{=}))∗λ(Y)+λ(ρ(g^{>})) = τ(g^{=})∗τ(X_{n+1})+ τ(g^{>}) = τ(X_{n+1}). The last equality holds because of Lemma 19.

By definition, λ(σ(X_{i})) = λ′(ρ(X_{i})) = τ(X_{i}), for all i = 1, …, n. This shows that σ is even a most general maximizer of f. □

Now we are able to prove the correctness of our algorithm.

Theorem 21 Let f : {0, 1}^{n} → Z be a pseudo-Boolean function represented by the pseudo-Boolean term u ∈ T (F_{psbool}, V_{bool}).

Starting with the problem z ≐ max(u) and applying the rules of the Basic Algorithm at most n + 1 times one obtains a solved form

{z ≐ c, X_{1} ≐ t_{n}, …, X_{n} ≐ t_{n}},

with c ∈ Z, t_{i} ∈ T (F_{psbool}, V_{bool}), such that c is the maximum value and {X_{1} ← t_{1}}∘…∘{X_{n} ← t_{n}} is a most general maximizer of f.

Proof: Let V ar(u) = {X_{1}, …, X_{n_{u}}} denote the set of variables occurring in the pseudo-Boolean term u. The proof is by induction on n_{u}.

First consider the case n_{u} = 0. If u contains no variables, the function f is equivalent to a constant function c :→ Z, the rule Constant applies, and we get max(f) = z = c.

Now suppose n_{u} = n + 1, n ≥ 0. We may assume that u is not congruent to a constant. Then we can choose a variable X_{n+1} in u and write u in the form

u = v ∗ X_{n+1} + w,

Constant  \frac{z ≐ max(u)}{z ≐ c}

if u ≡_{P B} c = constant
Variable Elimination \frac{z ≐ max(u)}{\{z ≐ max(v^{+} + w)\} ∪ \{X ≐ v^{>}\}}

if u ≡_{P B} v ∗ X + w,
X ∉ V ar(v, w),
v ≢_{P B} 0

Figure 3: The Basic Algorithm for Pseudo-Boolean Optimization (Special Version)

where {X_{1}, …, X_{n}} are the only variables occurring in the terms v, w and v ≠ 0. We apply the variable elimination rule and obtain the new problem

{z ≐ max(v^{+} + w)} ∪ {X_{n+1} ≐ v^{=} ∗ X′ + v^{>}},

with a new variable X′.

Applying the induction hypothesis to z ≐ max(v^{+} +w) then yields in at most n steps the solved form

{z ≐ c, X_{1} ≐ t_{n}, …, X_{n} ≐ t_{n}},

with c ∈ Z, t_{i} ∈ T (F_{psbool}, V_{bool}), where c is the maximum value and {X_{1} ← v} ∘ … ∘ {X_{n} ← t_{n}} is a most general maximizer of v^{+} + w.

Using Lemma 19 and Lemma 20 we may conclude that c is also the maximum value of f and that {X_{1} ← v} ∘ … ∘ {X_{n} ← t_{n}} ∘ {X_{n+1} ≐ v^{=} ∗ X′ + v^{>}} defines a most general maximizer of f. □

5.2 The Special Version of the Basic Algorithm

Sometimes one is interested only in one special maximizer of a given pseudo-Boolean function and not in the most general maximizer. In this case, one can use a special version of the Basic Algorithm (see Figure 3).

For the special version of the Basic Algorithm an interesting complexity result was recently proved in [CHJ90]. In this paper it is shown that for some special class of pseudo-Boolean functions, namely the pseudo-Boolean functions of bounded tree-width, the special version of the Basic Algorithm runs in linear time.

Definition 22 Let f(X_{1}, …, X_{n}) be a pseudo-Boolean function in polynomial form. The cooccurrence graph G(f) has vertex-set V = {X_{1}, …, X_{n}} and an edge between X_{i} and X_{j}, i ≠ j, iff these variables occur simultaneously in at least one monomial of f. The tree-width of f is the tree-width of the co-occurrence graph G(f).

The definition of the tree-width of a graph is rather technical and can be found in the appendix (see also [Arn85]).

Theorem 23 ([CHJ90]) The Basic Algorithm has linear-time complexity when applied to pseudo-Boolean functions with bounded tree width.

More precisely: For every fixed k ≥ 0, the Basic Algorithm can be implemented to run in O(n) time on those pseudo-Boolean functions f(X_{1}, …, X_{n}), expressed in polynomial form, for which (X_{1}, …, X_{n}) is a k-scheme of G(f).

If g : {0, 1}^{n} → {0, 1} is a Boolean function, then the equation g(X_{1}, …, X_{n}) ≐ 1 has a solution iff max(g(X_{1}, …, X_{n})) = 1. This means that Boolean unification can be regarded as a special pseudo-Boolean optimization problem. In this case, the Basic Algorithm can be used to compute a special solution of the equation g(X_{1}, …, X_{n}) ≐ 1.

Moreover, for Boolean functions the Basic Algorithm specializes to a variant of Büttner-Simonis’ Boolean unification algorithm [BS87]. Therefore we get the following complexity result for Boolean unification.

Corollary 24 For every fixed k ≥ 0, Büttner/Simonis’ Boolean unification algorithm can be implemented to compute in O(n) time a special solution of those Boolean unification problems f(X_{1}, …, X_{n}) ≐ 1, for which the Boolean function f(X_{1}, …, X_{n}) has tree-width at most k.

Because of the close relationship between the two algorithms, experiences that have been gained in the implementation of one of them have immediate consequences for the other one. For example,

[CHJ90] compare two variable elimination orderings, which are related to the co-occurrence graph of the pseudo-Boolean function. The determination of a good elimination ordering is one of the main problems in the implementation of Büttner-Simonis’ algorithm. It has a great influence on the size of the most general unifiers that are computed. In this context, the orderings proposed in [CHJ90] may be very interesting. On the other hand, there exist rather sophisticated implementations of Büttner-Simonis’ algorithm. It is clear that the ideas which have been developed in this context should be used also in the pseudo-Boolean case.

6 Example

In this section we present a typical application of pseudo-Boolean constraints [HR68] that is simple enough to be considered here.

The problem is to assemble a radio set under the following conditions:

• Any one of the three types T1, T2, T3 of tubes may be utilized, but only one.

• The box may be either of wood W, or of plastic material P. When using P, dimensionality requirements impose the choice of T2, and as there is no place for a transformer F, a special power supply S is needed.

• T1 needs F.

• T2 and T3 need S (and not F).

The prices of the above components are

Tubes T1  28 units
Tubes T2  30 units
Tubes T3  31 units
Transformer F  25 units
Special Power Supply S 23 units
Wood Box W  9 units
Plastic Material Box P 6 units

The other necessary components of the radio set cost

27 units, if the tubes T1 are utilized
28 units, if the tubes T2 are utilized
25 units, if the tubes T3 are utilized

The price of the make is 10 units for each set in all the cases and a set is sold at 110 units when it is enclosed in a plastic material box, and at 105 units in the other case. Which model is to be constructed in order to maximize the profit? The following program solves this problem.

assemble(T1, T2, T3, F, S, W, P) :-
                 T1 + T2 + T3 = 1,
                 W + P = 1,
                 F + S = 1,
                 P ≤ T2 * S,       % P = 1 implies T2 = S = 1
                 T1 ≤ F,           % T1 = 1 implies F = 1
                 T2 ≤ S,           % T2 = 1 implies S = 1
                 T3 ≤ S.           % T3 = 1 implies S = 1
maximal-profit(T1, T2, T3, F, S, W, M) :-
        max( 110W + 105M - ( 28T1 + 30T2 + 31T3 + 25F + 23S
                             + 9W + 6P + 27T1 + 28T2 + 25T3 + 10),
        assemble(T1, T2, T3, F, S, W, M) ).

Asking the query

     ?- maximal-profit(T1, T2, T3, F, S, W, M).

yields the unique answer

     T1 = 0, T2 = 0, T3 = 1, F = 0, S = 1, W = 1, M = 0.

7 Conclusion and Further Research

In this paper we have introduced a new constraint logic programming language CLP(PB) for logic programming with pseudo-Boolean constraints. The language is an instance of the constraint logic programming language scheme CLP(X) and has therefore the usual declarative and operational semantics of constraint logic programming languages. The main emphasis of the paper was on the solution of pseudo-Boolean constraints. We showed that any pseudo-Boolean constraint has a most general solution and gave an algorithm for pseudo-Boolean unification. Then we discussed the problem of optimizing pseudo-Boolean functions. We presented the Basic Algorithm for pseudo-Boolean optimization and discussed its relationship to the variable elimination method in Boolean unification. Among others, we obtained a new complexity result for Boolean unification.

Several research directions can be outlined to continue this work. On the practical side, the most important problem is to design an efficient constraint solver for pseudo-Boolean constraints. This should be done using the techniques that have been developed for the Boolean case. The next step is to extend this constraint solver by an algorithm for pseudo-Boolean optimization. On the theoretical side, it would be interesting to find further classes of Boolean and pseudo-Boolean functions that admit polynomial unification or optimization algorithms. Various such classes are already known, however it is not clear which role they play in practical applications.

References

[Arn85] S. Arnborg. Efficient algorithms for combinatorial problems on graphs with bounded decomposability. A survey. BIT, 25:2–23, 1985.

[ASS^{+}88] A. Aiba, K. Sakai, Y. Sato, D.J. Kawley, and R. Hasegawa. Constraint logic programming language CAL. In Fifth Generation Computer Systems, Tokyo, 1988. Springer-Verlag, 1988.

[BR89a] A. Bockmayr and H.H. Rath. Algorithms for boolean unification. In Proc. FAW Workshop on Boolean Functions, Propositional Logic, and AI Systems. FAW Ulm, Germany, 1989.

[BR89b] A. Bockmayr and H.H. Rath. Extended prolog with boolean unification. Technical Report 21/89, Fakultät für Informatik, Univ. Karlsruhe, 1989.

[BS87] W. Büttner and H. Simonis. Embedding boolean expressions in logic programming. Journal of Symbolic Computation, 4(2):191–205, 1987.

[CHJ90] Y. Crama, P. Hansen, and B. Jaumard. The basic algorithm for pseudo-boolean programming revisited. Discrete Applied Mathematics, 29:171 – 185, 1990.

[Col87] A. Colmerauer. Introduction to PROLOG III. In 4th Annual ESPRIT Conference, Bruxelles. North Holland, 1987.

[DvHS^{+}88] M. Dincbas, P. van Hentenryck, H. Simonis, A. Aggoun, and T. Graf. The constraint logic programming language CHIP. In Fifth Generation Computer Systems, Tokyo, 1988. Springer-Verlag, 1988.

[FGGB66] R.J. Freeman, D.C. Gogerty, G.W. Graves, and R.B.S. Brooks. A mathematical model of supply support for space operations. Oper. Research, 14:1–15, 1966.

[Ham64a] P.L. Hammer. The method of successive eliminations for pseudo-boolean equations. Bulletin de l’Academie Polonaise des Sciences-Serie des Sciences Math., Astr. et Phys., XII(11):681–683, 1964.

[Ham64b] P.L. Hammer. Systems of pseudo-boolean equations and inequalities. Bulletin de l’Academie Polonaise des Sciences-Serie des Sciences Math., Astr. et Phys., XII(11):673–680, 1964.

[HO80] G Huet and D. C. Oppen. Equations and rewrite rules, A survey. In R. V. Book, editor, Formal Language Theory. Academic Press, 1980.

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

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

[HRR63a] P.L. Hammer, I. Rosenberg, and S. Rudeanu. Application of discrete linear programming to the minimization of boolean functions. Rev. Math. Pures Appl., 8:459–475, 1963. (in Russian).

[HRR63b] P.L. Hammer, I. Rosenberg, and S. Rudeanu. On the determination of minima of pseudo-boolean functions. Stud. Cerc. Mat., 14:359–364, 1963. (in Romanian).

[HS86] P.L. Hammer and B. Simeone. Quadratic functions of binary variables. In Combinatorial Optimization, volume 1403 of Lecture Notes in Mathematics. Springer-Verlag, 1986.

[JL86] J. Jaffar and J.-L. Lassez. Constraint logic programming. Technical Report 86/73, Department of Computer Science, Monash University, June 1986.

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

[KGV83] S. Kirkpatrick, C.D. Gelatt, and M.P. Vecchi. Optimization by simulated annealing. Science, 220:671–680, 1983.

[Rhy70] J. Rhys. A selection problem of shared fixed costs and networks. Manag. Science, 17:200–207, 1970.

A Tree-Width of a Graph

Let G be a simple and undirected graph. A vertex v is simplicial in G if the neighbors of v induce a complete subgraph of G. For k ≥ 0, a k-perfect elimination scheme of the graph G is an ordering (v_{1}, …, v_{n}) of its vertices, such that v_{j} is simplicial and has degree k in the subgraph G_{j} of G induced by {v_{j}, v_{j+1}, …, v_{n}} for j = 1, …, n − k. A graph is a k-tree if it has a k-perfect elimination ordering. A partial k-tree is any graph obtained by deleting edges from a k-tree. Any graph on n vertices is a partial n-tree. The tree-width of a graph is the smallest value of k for which the graph is a partial k-tree. For instance, trees and forests have tree-width at most 1, and series-parallel graphs have tree-width at most 2. Determining the tree-width of a graph is NP-hard. However, for every fixed k, there is a polynomial algorithm to decide if a graph has tree-width k.