{'fraction_non_alphanumeric': 0.037275927866913916, 'fraction_numerical': 0.006530678061759252, 'mean_word_length': 4.243799323562571, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Terse Integer Linear Programs for Boolean Optimization

We present a new polyhedral approach to nonlinear Boolean optimization. Compared to other methods, it produces much smaller integer programming models, making it more efficient from a practical point of view. We mainly obtain this by two different ideas: first, we do not require the objective function to be in any normal form. The transformation into a normal form usually leads to the introduction of many additional variables or constraints. Second, we reduce the problem to the degree-two case in a very efficient way, by slightly extending the dimension of the original variable space. The resulting model turns out to be closely related to the maximum cut problem; we show that the corresponding polytope is a face of a suitable cut polytope in most cases. In particular, our separation problem reduces to the one for the maximum cut problem. In practice, the approach appears to be very competitive for unconstrained Boolean optimization problems. First experimental results, which have been obtained for some particularly hard instances of the Max-SAT Evaluation 2007, show that our very general implementation can outperform even special-purpose Max-SAT solvers. The software is accessible online under “we.logoptimize.it”.


Introduction
Nonlinear zero-one optimization problems are often solved by transforming the objective function into an appropriate normal form, e.g., into conjunctive normal form (CNF) or into a polynomial. The problem can then be addressed by a general solver for maximum satisfiability, polynomial zero-one optimization or some other standard problem. However, the transformation often increases the problem size significantly, since new variables or constraints have to be added. Depending on the normal form, an exponential blow-up might be unavoidable, e.g., if negations in a polynomial have to be resolved. But even if the increase is tractable from a theoretical point of view, in practice it might lead to a problem instance that is too large to be solved.
In this paper, we present a novel approach to nonlinear zero-one optimization that avoids the transformation into any normal form, by directly modeling arbitrarily constructed Boolean functions into an integer linear program (ILP). The strength of our approach lies in the fact that, nevertheless, a tight polyhedral description for the resulting model can be obtained. This description is based on a reduction of the general problem to the special case of unconstrained quadratic zero-one optimization, which is known to be equivalent to the maximum cut problem [8]. Our approach is mainly designed for unconstrained problems. Under general linear or nonlinear constraints, our polyhedral results do not hold anymore, however, our construction still gives rise to much tighter linear relaxations. Furthermore, certain classes of constraints do not harm our polyhedral results, as discussed below.
We first deal with the quadratic case, i.e., the case where all objective function terms contain at most one binary operator. We show that in this case the polytope corresponding to our formulation is isomorphic to a cut polytope, no matter which operators are considered. This is a generalization of a result of [6], where all operators are multiplications.
The situation is more complicated in the general case where we allow arbitrary Boolean functions defined recursively by binary operators. Again, our aim is to avoid introducing too many new variables or constraints, as done by other approaches such as lift-and-project. In [4], we developed a new approach for polynomial zero-one optimization problems that uses an efficient reduction to the quadratic case. The reduction can be applied after a slight extension of the variable space; the resulting polytope then turns out to be a face of a polytope corresponding to a quadratic instance of basically the same type. This allows to derive a polyhedral description for a general instance from the polyhedral description of an appropriate quadratic problem.
In the following, we generalize these results. In place of multiplications, we allow arbitrary binary operators. For problem instances not containing any exclusive disjunctions or equivalences, we show that the general polytope is still a face of an appropriate cut polytope, defined on roughly four times as many variables as in the original model. If exclusive disjunctions or equivalences are present, they can be replaced by at most three other operators each.
Our problem is closely related to the pseudo-boolean optimization problem, which has been investigated intensively in the literature. See [3] for a survey of applications and results. In pseudo-boolean optimization methods, polyhedral techniques are often used in order to derive stronger dual bounds on the optimal solutions, leading to smaller enumeration trees in general. In this spirit, Manquinho and Marques-Silva [11,12] propose the use of cutting planes in SAT-based algorithms. Similarly, Joy et al. [10] devise classes of cutting planes for the basic integer programming model of Max-SAT. Cutting planes are also used in a hybrid approach presented by Sheini and Sakallah [14].
Our polyhedral approach presented in the following is different from these approaches, in that it does not aim at the identification of single classes of cutting planes that can be used to tighten dual bounds, but at a full integer programming model of the problem, for which strong polyhedral results can be derived in a more general way.
We also give experimental evidence of the practical potential of our new approach. We present the results obtained by an implementation of this approach, on all instances of the Max-SAT Evaluation 2007 [1]. It turns out that our approach is very competitive and can even outperform special-purpose Max-SAT solvers on particularly hard instances.

The Problem
We consider an unconstrained Boolean optimization problem in the following form: a set of Boolean variables x i ∈ {0, 1} for i ∈ I is given, where I is a finite index set. We set n = |I|. Moreover, we have a pseudo-boolean objective function In the following, our aim is to address problem (1) by an approach that is based on modeling each such Boolean function independently.
Example 2.1. All CNF and DNF clauses are Boolean functions. In particular, the maximum satisfiability problem is a special case of (1).
Example 2.2. Binary monomials are Boolean functions, since multiplication of binary variables can be considered a binary operator on Boolean variables. In particular, a special case of (1) is binary polynomial optimization.
3. If f is any Boolean function as defined above, then checking satisfiability of f amounts to checking whether max(f ) = 1. Checking whether f is a tautology amounts to checking whether min(f ) = 1. In particular, we can check equivalency of f and any other logical formula g by minimizing the Boolean function f ⇔ g.
A list of all possible 16 binary operators is given in Table 1. For ease of exposition, we assume throughout that all operators appearing in the functions are proper binary operators, i.e., we do not consider unary or constant operators. This situation can always be obtained as follows: constant operators can be resolved easily. The only non-trivial unary operator is negation. In the objective function, negations can be resolved by replacing ¬f k by 1 − f k . Elsewhere, negations can be merged into binary operators, e.g., we can consider a ∨(¬b) a binary operator in a and b. In Table 2, we list the corresponding replacements explicitly. In summary, out of the 16 operators in Table 1, we only have to consider the first ten.
In theory, problem (1) can model the minimization of any function f : {0, 1} n → R, as E.g., we could write a ∨ b as (a ∧ b) + (a ∧ ¬b) + (¬a ∧ b). Unfortunately, this representation of f is useless, as it leads to a trivial problem: the optimal solution is readily obtained with a simple linear time algorithm that produces the solution right after reading the input to the problem. However, if a much more compact representation of f than (2) is provided, then the problem may become much more difficult to solve and the approach presented in the following may become very efficient. Actually, the efficiency mainly depends on the total number of operators in all functions f k , k ∈ K. Clearly, the number of functions {0, 1} n → {0, 1} that can be modeled with a fixed number of arbitrary binary operators, as explained above, is much bigger than, e.g., the number of CNF formulae produced using the same number of operators.
In this context, we point out that some effort in compactifying the representation of f can be worthwhile. Even if the original instance is given in some normal form such as CNF, it might well pay off to give up the normal form if this leads to a smaller number of operators. In general, the more the flexibility of our approach is exploited, the more it can be expected to outperform methods designed for instances with a specific structure.

Branch-and-Cut and the Maximum Cut Problem
In this section, we review the basic ideas of branch-and-cut algorithms, with a view towards the maximum cut problem. Branch-and-cut is an extension of branch-and-bound, in which the bounds in all enumeration nodes are computed by solving LP-relaxations of the problem [13].
In order to start a branch-and-cut approach, the problem must first be modeled as an integer linear program (ILP), i.e., a linear program with additional integrality constraints on all or some of the variables. In the following, all variable required to be integer will be binary, i.e., will take only the values 0 or 1. Therefore, we will only consider the branchand-cut approach for the binary case. The branching step usually consists in creating two subproblems that replace the original one; each of the two subproblems is obtained by fixing an integer variable to one of its two possible values. The first LP-relaxation arises from ignoring all integrality requirements. The optimal solution of this LP-relaxation then yields a dual bound for the original problem (a lower or an upper bound depending on whether we minimize or maximize, respectively).
If the optimal LP-solution is fractional, i.e., if it does not meet all integrality constraints, then a branch-and-cut algorithm tries to improve the relaxation by adding further linear inequalities that are valid for all feasible solutions of the ILP but violated by the given fractional LP-solution. Such inequalities are called cutting planes. An algorithm trying to find such cutting planes is called a separation algorithm. Usually, a separation algorithm is designed to find cutting planes from within a specific class of candidate inequalities.
The separation problem leads to the mathematical task of understanding the polyhedral structure of the problem. More precisely, it is necessary to characterize classes of valid inequalities for the polytope defined as the convex hull of all feasible solutions of the ILP. The separation algorithm must then decide whether a certain fractional point can be separated from this polytope by some hyperplane from the known classes.
For an NP-hard problem, there is no hope of finding a complete characterization of the system of linear inequalities describing the polytope. However, in practice, the performance of a cutting plane algorithm generally increases even with a (very) limited knowledge of such a system. Moreover, for the polytope associated with these difficult problems the separation for several classes of valid inequalities is also NP-hard. Therefore, typically one has to resort to heuristic separation algorithms. When such an algorithm returns a cutting plane from a specific class, the answer is correct. However, if it terminates with the status "no separating hyperplanes found", this does not necessarily mean that indeed no such hyperplanes exist.
Due to the incomplete knowledge of the linear system, and due to the heuristic nature of some separation algorithms, the cutting-plane phase may terminate with an optimal LP-solution that still has some fractional components. The branch-and-cut algorithm then proceeds with a branching phase. Cutting-plane and branching phases are recursively applied to all generated subproblems.
Branch-and-cut algorithms turned out to be very successful in practice for solving many hard optimization problems. One of these problems concerns cuts in graphs. In a graph G = (V, E), with every subset S ⊆ V we associate the set of all edges having exactly one end-node in S. Such an edge set is called the cut of G defined by S and is denoted by δ(S). Note that the sets S and V \ S define the same cut of G and that S can be empty (or can coincide with V ), in which case the cut δ(S) is the empty set. Given a graph G = (V, E) with edge weights w e ∈ R, the maximum cut problem (max-cut) is to find a cut in G of maximum total weight. In the standard ILP formulation of this problem, we have a binary variable x e ∈ {0, 1} for each edge e ∈ E, such that x e = 1 if and only if e belongs to the cut being modeled. Such a binary vector associated with a cut δ(S) is called its incidence vector and is denoted by χ S ∈ R E . The cut polytope C(G) ⊂ R E of G is the convex hull of all incidence vectors of cuts in G.
Many classes of cutting planes as well as other structural properties of cut polytopes have been discovered; see [7] for a broad overview. In our implementation, we currently only use the most important class of cutting planes called cycle inequalities. These inequalities model the fact that every cut of G must have an even intersection with every cycle in G, i.e., for every cycle C in G and every odd subset F ⊆ C, we have that the inequality e∈F x e − e∈C\F x e ≤ |F | − 1 is satisfied by the incidence vectors of all cuts of G, thus it is as a valid inequality for the cut polytope C(G). In general, there are exponentially many cycle inequalities for a given graph; nevertheless, the corresponding separation problem can be solved in polynomial time [2].
Though polynomial, the exact separation algorithm for cycle inequalities is often too slow in practice. Therefore, the separation is often done heuristically. In our implementation, we use a heuristic based on maximum weight spanning trees, see Section 5 below.

New Formulation and Reduction to Maximum Cut
In the following, we develop our new model for Boolean optimization problems. This approach has two main advantages over other methods: the number of variables is kept small, even if the objective function does not conform to any normal form. The second advantage is that the corresponding polytope turns out to be a face of an appropriate cut polytope, if the model is slightly extended and no exclusive disjunctions or equivalences appear in the objective function. This allows us to address the general problem by a cutting plane method that is entirely based on separation algorithms for the maximum cut problem. An example illustrating the construction will be given in Section 4.3 below.

The Model
In order to develop a linear model for problem (1), we have to introduce further binary variables. First, we need to linearize the objective function by adding a variable x k ∈ {0, 1} representing f k , for every k ∈ K. The objective then translates to min c ⊤ x K , and it remains to model the connection between the basic variables x I and the objective variables x K . More precisely, we have to make sure that In order to bridge the gap between basic and objective variables, we additionally introduce connection variables x j ∈ {0, 1}, j ∈ J. Every such variable corresponds to an intermediate function in the recursive definition of the Boolean functions f k .
More formally, we determine the set of connection variables recursively as follows: we start with J = ∅. Let j ∈ J ∪ K with f j = g • j h, for appropriate Boolean functions g and h and for a proper binary operator • j . If g = f s for some s ∈ I ∪ J ∪ K, we define l(j) = s, otherwise we add a new index l(j) to J, introduce a new variable x l(j) representing g, and define f l(j) = g. Analogously, if h = f s for some s ∈ I ∪ J ∪ K, we define r(j) = s, otherwise we add a new index r(j) to J, introduce a variable x r(s) representing h, and define f r(j) = h. We continue in this way until every We have thus constructed a set of variables {x s | s ∈ I ∪ J ∪ K} and a corresponding set of Boolean functions F = {f s | s ∈ I ∪ J ∪ K} defined on the domain {0, 1} I∪J . In the following, the unit vector corresponding to x s will be denoted by e s . Every non-basic function in F is the result of applying some binary operator to an appropriate pair of other functions in F . Notice that the total number of connection and objective variables |J ∪ K| is at most the total number m of operators in the objective function, so the total number of variables in our model is at most n + m. In practice, it is often possible to save a lot of these variables by intelligent decomposition of the objective function.
Every feasible solution in our model is uniquely determined by a truth assignment for all basic variables x i , i.e., by a function t : I → {0, 1}. The corresponding characteristic vector χ t ∈ {0, 1} I∪J∪K is defined in the obvious way-every component (χ t ) s takes the value of f s under t, denoted by t(f s ) in the following. Now we define Equivalently, we have We can thus restate problem (1) as min c ⊤ x K s.t. x ∈ P .
In order to solve this problem, it is necessary to find tight linear relaxations of the polytope P . The standard techniques for linearizing polynomial terms in binary programs could be adapted to our model, however, the resulting relaxations for P are weak in general. Instead, we aim at generalizing the results we obtained for binary polynomial optimization, presented in [4], to the more general situation considered here. In the remainder of this section, we will show that P is a face of an appropriate cut polytope of small dimension if the objective function does not contain exclusive disjunctions or equivalences.
The proof is done in two steps: first the result is shown in the quadratic case, i.e., when all objective terms f k contain at most one operator. In fact, P is isomorphic to a cut polytope in this case. This is a generalization of a result given in [6], that states that binary quadric polytopes are isomorphic to cut polytopes. We obtain this result without restricting the set of allowed operators.
Second, we show that in the case of objective functions of arbitrary degree, the polytope P is a face of a polytope P * defined by a quadratic instance of our problem, if the objective function does not contain exclusive disjunctions or equivalences. In other words, under this assumption, the case of arbitrary degree can be reduced to the quadratic case.

Quadratic Case
In the quadratic case, the polytope P is always isomorphic to an appropriate cut polytope defined on the same number of variables.
Lemma 4.1. Let f k contain at most one operator for all k ∈ K. Then the polytope P is isomorphic to a cut polytope. The corresponding graph has n + 1 nodes and n + m edges.
Proof: In this case, we have J = ∅ and l(k), r(k) ∈ I for all k ∈ K. We can thus define a graph G = (V, E) by In the following, let e (v,w) denote the unit vector in R E associated with an edge (v, w) ∈ E.
We define a linear map ψ ′ : R E → R I∪K by fixing the images of all unit vectors of R E : As ψ ′ is bijective, the map ψ : R E → R I∪K given by x → ψ ′ (x) + k∈K (0 • k 0)e k is an affine isomorphism. Hence it suffices to show that ψ induces a bijection between the vertices of the cut polytope C(G) of G and the vertices of P . So consider the incidence vector χ S ∈ C(G) of any cut δ(S), S ⊆ V , where we may assume, without loss of generality, that z ∈ S. Define a truth assignment t : I → {0, 1} by setting t(i) = 1 if and only if v i ∈ S. We claim that ψ(χ S ) = χ t . Indeed, = t(l(k)) • k t(r(k)) = (χ t ) k . operator Conversely, for given t : This construction is obviously inverse to the one above, so the proof is complete. 2 The main ingredient in the proof of Lemma 4.1 is the reformulation of an arbitrary binary operator as an affine combination of exclusive disjunction and basic variables, using (3). For the ten operators to be considered, the corresponding formulae are listed in Table 3.

General Case
In this section, we do not require a quadratic objective function any more. Moreover, we do not assume any normal form, all operators may be mixed arbitrarily. Nevertheless, we can show the following result.
Theorem 4.1. Assume that no operator in the objective function is an exclusive disjunction or an equivalence. Then the polytope P is isomorphic to a face of a cut polytope. The corresponding graph has at most n + 4m edges.
Proof: By the previous lemma, it suffices to show that P is a face of some polytope P * that corresponds to a quadratic instance of our problem with at most n + m basic variables and at most 3m operators in total. In order to construct this quadratic instance, define the set of basic variables to be {x 0 s | s ∈ I ∪ J} and set I * = I ∪ J. Moreover, define a new set of quadratic objective terms over these variables as Let K * be an index set for these 3|J| + |K| objective terms. Denote the corresponding polytope in R I * ∪K * by P * . We will show that P is a face of P * . For the following, we denote the unit vector in R I * ∪K * associated with the variable x i s by e i s , for s ∈ I * ∪K * and i = 0, 1, 2, 3. Moreover, we define c s = 1• s 1+0• s 0−1• s 0−0• s 1. Observe that c s = 0 for all proper binary operators. We first claim that where X is the linear subspace of R I * ∪K * given by the equations for all s ∈ J. The isomorphism is induced by the linear map ϕ : R I * ∪K * ∩ X → R I∪J∪K that is uniquely defined by ϕ(e 0 s ) = e s for s ∈ I * and ϕ(e 1 s ) = e s for s ∈ K. The images of all other unit vectors of R I * ∪K * under ϕ are determined by the equations (5) to (7).
To show (4), consider a vertex χ t of P corresponding to an assignment t : I → {0, 1}. Extend it to t * : I * → {0, 1} in the natural way, setting t * (s) = t(f s ) for all s ∈ J. Now by construction we have χ t = ϕ(χ * t * ), where χ * t * denotes the characteristic vector of t * in P * . To see this, one can verify, by checking all possible operators • s and all possible truth assignments to the variables x l(s) , x r(s) , and x s , that Conversely, any point in P * ∩ {0, 1} I * ∪K * is a vertex χ * t * of P * corresponding to a truth assignment t * : I * → {0, 1}. Let t = t * | I . By (5), all vectors in X satisfy so that we can inductively show that x 0 s = t(f s ) for s ∈ I * , supposed that the same holds for s ∈ I. In other words, t * is the extension of t described above, hence we have χ t = ϕ(χ * t * ) again.
For each of these operators, we claim that the equations (6) and (7) hold as inequalities for P * , the direction depending on the operator. Indeed, the right hand side of (6) reads In the first two cases, this right hand side is greater or equal to x 0 l(s) ∧ x 0 s = x 2 s for every integer point in P * . In the other two cases, this right hand side is less or equal to x 0 l(s) ∧ x 0 s = x 2 s for every integer point in P * . Thus (6) induces a face of P * . For (7), the same result follows by symmetry.
So let F be the face of P * induced by the two equations (6) and (7). It remains to show that (5) induces a face of F . From (6) we derive This completes the proof. 2 Example 4.1. To illustrate the construction of Theorem 4.1, consider the case of a single CNF-clause x 1 ∨ x 2 ∨ x 3 containing three non-negated variables, which is the smallest nontrivial example. Then the polytope P corresponding to the problem is defined over five binary variables x 1 , . . . , x 5 , where the first three are basic variables and can thus be chosen freely, while the other two variables are determined by the basic variables according to By (4), the polytope ϕ(P ) is spanned by a subset of the vertices of P * , determined by the equations (5) to (7). As • 4 = ⊕ and c 4 = −2, these equations read Since P * is symmetric with respect to all hyperplanes defined by these equations, it follows that the barycenters of ϕ(P ) and P * agree, i.e., that ϕ(P ) cuts through the center of P * . The same holds with ⇔ in place of ⊕.
Corollary 4.1. The polytope P is isomorphic to a projection of a face of a cut polytope. The corresponding graph has at most n + 12m edges.
Proof: After replacing all exclusive disjunctions and equivalences using the identities we get a new instance of our problem with at most 3m binary operators. Let P ′ denote the polytope defined by this instance. Then, by Theorem 4.1, P ′ is isomorphic to a face of a cut polytope on at most n + 12m edges. On the other hand, it is clear by definition that P is an orthogonal projection of P ′ . 2

Constraints
So far we have discussed unconstrained Boolean optimization problems, where all Boolean functions in the problem formulation appear in the objective function. However, it is clear that the same approach works if we have constraints of the form f k = 0 or f k = 1, where f k is any Boolean function. In this case, we model f k exactly as we model the objective terms. If we consider the corresponding polytope P and intersect it with the hyperplane x k = 0 or x k = 1, then we obviously get a face of P . If we consider linear constraints instead of Boolean ones, the situation is more complicated. In general, we cannot rescue our polyhedral results in this case. However, in some special cases, the situation is again favorable. To give an example, consider the constraint s∈L f s ≤ 1 (8) for an arbitrary subset L ⊆ I ∪ J ∪ K. This constraint states that at most one of the functions f s with s ∈ L may evaluate to one. In order to model (8) without harming our polytope P , we introduce a zero-weight objective term f L = s∈L f s . Moreover, we have to add up to |L| − 1 connection variables. Then we can rephrase (8) as The latter formulation is preferable since s∈L f s ≥ f L is a valid constraint for P , so that (9) induces a face of P . In the same way, we can deal with an equation stating that exactly one of the functions f s with s ∈ L evaluates to one. Additionally to (9) we have to set f L = 1 here, which again induces a face.

Experiments
Experimental results obtained with a straightforward implementation of our approach show that the increased modeling power leads to fast running times in practice. In this section, in order to demonstrate this by some examples, we shortly discuss two classes of instances taken from the Max-SAT Evaluation 2007 [1,9]. The evaluation [1] was based on several classes of instances. We chose those classes where the percentage of instances solved by the best participating algorithm was particularly small, namely the logic-synthesis and the SPOT5 instances. Both classes belong to the partial Max-SAT category, i.e., some of the clauses have to be satisfied by every solution, while others have positive integer weights in the objective function.
In our implementation, we first apply some very simple preprocessing techniques. Their main objective is to reduce the number of variables in our model. Currently, we only do this in a very restricted way: we use the equivalent replacement where each f i can be an arbitrary Boolean function. Notice that SAT solvers can only handle the former group of constraints, while in our approach we can also deal with the latter constraint, as explained in Section 4.4. This reduces the number of operators from |I| 2 to |I|−1. To detect such sets of constraints, we apply a simple algorithm for finding maximal cliques in the conflict graph defined as follows: the graph contains a vertex for every Boolean function f i appearing in the instance. Two vertices corresponding to Boolean functions f i and f j are adjacent if and only if the instance contains a subformula f i ∨ f j .
In principle, we could apply much more sophisticated reformulation techniques in order to decrease the number of operators in our objective function, exploiting the fact that the result is not requested to be in CNF. However, developing such techniques was not the focus of our work. Moreover, in our opinion, the flexibility of our approach is best exploited if the user takes advantage of this flexibility already in the modeling phase.
It is also possible to save variables without decreasing the number of operators. For this, note that the variables corresponding to expressions f i • 1 f j and f i • 2 f j , containing the same operands f i and f j , determine each other: by (3), the variables for f i , f j , f i • 1 f j , and f i • 2 f j satisfy an affine equation. In other words, we only need one variable for modeling both expressions f i • 1 f j and f i • 2 f j .
Generally speaking, it is thus desirable to have a large number of expressions with the same pair of operands. In our implementation, we try to increase this number by exploiting associativity and commutativity of ∧ and ∨: for all subformulae of the objective function containing only conjunctions or only disjunctions, we can group the operands in an arbitrary way, e.g., we can write leads to different sets of variables in our model. Considering such expressions at different positions in the objective function simultaneously, one can possibly save many variables by choosing a nesting that leads to a large number of equivalent variables.
In our preprocessing phase, we determine the nesting in a greedy way: we always choose a pair of operands (f i , f j ) that jointly appears in a maximal number of such expressions, and introduce a variable for f i • f j . In other words, we consider (f i • f j ) as a single operand in the following, and proceed like this until all conjunctions and disjunctions are defined on exactly two operands. For example, having two formulae After preprocessing, an initial ILP formulation of the reduced instance is handed over to the CPLEX 11.1 MIP solver [5], which tries to optimize it using a classical branchand-cut algorithm, see Section 3. Our only (but crucial) extension of the standard solver concerns the separation phase, where we make use of our results presented in Section 4: we first create the graph corresponding to the cut polytope constructed in the proof of Lemma 4.1, after transforming the original problem to a quadratic one as described in the proof of Theorem 4.1. Whenever CPLEX tries to separate a fractional LP-solution, we first transform this solution to the variable space of the corresponding cut polytope. Then we can apply any separation algorithm for max-cut on this graph, with the transformed fractional point as input.
In our current implementation, we only separate cycle inequalities. We do this heuristically in the following way: we first compute a maximum weight spanning tree with respect to the current fractional LP-values. Then we consider all fundamental cycles defined by this tree, the number of which is linear in the number of edges of the graph. We only add inequalities defined on cycles not exceeding a given length (in our current implementation, the limit is |V |/50). Any resulting cutting plane can easily be transformed back to the original variable space. Note that this heuristic approach is much faster than the exact separation algorithm, but it may fail to find a violated cycle inequality even if there is one. Moreover, it does not necessarily find the most violated cycle inequalities, like the exact separation algorithm does.
An important advantage of our approach is the fact that all other components of the branch-and-cut algorithm can be applied to the original set of variables, since all cutting planes generated by our max-cut based separation algorithm are expressed in these variables. In particular, the solution of LP-relaxations as well as the branching can be performed on the original set of variables. The transformation to a max-cut problem defined in a higherdimensional space is only necessary within the separation phase.
All experimental results reported in the following were obtained on an Intel Xeon processor with 2.33 GHz running Linux, i.e., on a machine that is slightly faster than the one used for the Max-SAT Evaluation 2007. As it was done with the codes evaluated in this contest, we set the cpu time limit of 30 minutes for all instances. We first report our results for two classes of particularly hard instances.
Instances in the class logic-synthesis are unweighted. The running times obtained with our approach described above turn out to be more than competitive: In 30 cpu minutes, we could solve to optimality 15 out of the 17 instances in this class. On the contrary, half of the 10 participants of the Max-SAT Evaluation could not solve a single of these instances, while the others could solve between 1 and 4 of them. More detailed results are displayed in Table 4. We state the number of solved instance and the average values of the running time in cpu seconds, the running time without preprocessing (i.e., the running time for the branch-and-cut algorithm), the number of subproblems in the enumeration tree, the number of nodes and edges in the auxiliary max-cut graph, and the number of cycle inequalities generated. We noticed in our experiments that generating a relatively small number of cycle inequalities can already lead to a significant reduction of the number of subproblems in the enumeration tree. Adding more cycle inequalities can reduce the number of subproblems even further, but at the expense of a longer separation time, which only pays off for larger instances. Notice that preprocessing uses a large portion of running time for the logic-synthesis problems, which however pays off as it shrinks these instances by up to 90 %. Here we would like to point out again that all preprocessing techniques we apply are very straightforward and are not adjusted to the given type of instances.
The second example class consists of the weighted SPOT5 instances. Our results are again very positive: as shown in Table 4, we could solve 17 instances in the subclass DIR and 15 in LOG. In the Max-SAT Evaluation, the best participant could solve only 6 instances in each class. So it seems that our method is consistently superior to other approaches when applied to very hard Max-SAT instances, in spite of the fact that it is designed for much more general problems. The presented running times, in particular those for logic-synthesis, suggest that a lot of work is done in the preprocessing. As discussed above, the preprocessing aims at a more compact reformulation of the problem. Indeed, when running the same instances without preprocessing, running times are significantly longer and less instances can be solved, as shown in Table 5 (where the running time for the branch-and-cut algorithm now coincides with the total time). This is mainly due to the larger size of the auxiliary graphs used in the max-cut separation. Nevertheless, our algorithm still outperforms all participants of the Max-SAT Evaluation on these instances.
The instances discussed so far turned out to be the hardest instances for all solvers in the Max-SAT Evaluation 2007. On these instances, our approach performs particularly well. However, it is also competitive on most of the other instances; see Table 6 for a complete overview of our experimental results. The results show that our approach "prefers" sparse instances, i.e., instances with a small ratio between the number of operators and the number of basic variables. This could be expected, as it is well-known that integer programming approaches to max-cut perform much better on sparse instances. For dense instances, we plan to develop other methods in the future, e.g., using approaches based on semidefinite programming. Moreover, as our method mainly addresses the dual side of the optimization, while not containing any nontrivial primal heuristics, it is not surprising that traditional Max-SAT solvers perform better on instances where all clauses can be satisfied simultaneously. On such instances, the optimization aspect takes a back seat, and dual bounds are necessarily trivial. However, it is clearly plausible that our algorithm can be improved by combining it with any primal heuristic for SAT or Max-SAT.

Conclusion
We presented a novel integer programming approach to nonlinear Boolean optimization problems. Unlike other approaches, it avoids adding many artificial variables to the model, at the same time allowing to derive tight linear relaxations of the corresponding polytope. In the special case of binary polynomial optimization, which has been investigated in [4], our approach proved to be very successful in practical experiments. Computational results for hard Max-SAT instances reported in this paper seem to confirm the good performance of our approach also for other nonlinear optimization problems.
The software described in the paper is accessible online at the web site we.logoptimize.it