18  Finding an Equivalent Binary Inequality

NoteSource and adaptation

Based on Optimising a constraint, Section 12.18 of Williams (2013). Uses the source eight-variable inequality. Adds explicit integer coefficient magnitudes of 1–40 and minimizes the absolute right-hand side. The results below solve the stated instance and are not presented as the numerical answer to an unmodified textbook problem.

18.1 Problem Statement

The original binary inequality is 9x1+13x2−14x3+17x4+13x5−19x6+23x7+21x8 ≤ 37. Every x is zero or one. Find an equivalent inequality with the same strict coefficient signs, integer coefficient magnitudes from 1 to 40, and integer right-hand side. Equivalent means accepting exactly the same binary assignments. Minimize the absolute right-hand side. There may be multiple equally simple answers. The coefficient bound is a teaching restriction, not a theorem about the unrestricted source problem.

18.1.1 Original inequality

Term Coefficient
x1 9
x2 13
x3 -14
x4 17
x5 13
x6 -19
x7 23
x8 21
RHS 37

18.2 Model Formulation

Enumerate the 256 binary vectors. Partition them into \(F\) (originally feasible) and \(N\) (originally infeasible). Unknown signed integer coefficients \(a_j\) have their prescribed signs and magnitudes 1–40. Let integer \(b\) be the right-hand side and \(B\ge0\).

\[\sum_j a_jx_j\le b\ (x\in F),\qquad \sum_j a_jx_j\ge b+1\ (x\in N),\] \[B\ge b,\quad B\ge-b,\qquad\min B.\]

The unit separation for infeasible points is exact because coefficients, binary inputs, and \(b\) are integer. Here the truth-table assignments are data; the decision variables are coefficients of a new constraint.

All decision variables and units refer to the problem statement above. Continuous variables are nonnegative unless explicitly stated otherwise; binary and integer domains are specified in the equations and code.

18.3 Pyomo Implementation

The following Python implementation uses Pyomo and HiGHS. Run from the workbook root so that the models package and shared helpers are importable. The shared solver and audit functions check optimal termination before loading values, then verify every active constraint, variable bound, and integer domain. Any imported earlier-chapter model supplies the data and balances already explained there.

The full source is problem18.py. To solve and print this problem independently:

~/.venvs/optim/bin/python -m models.common 18
import itertools
import pyomo.environ as pyo
from models.common import frame

ORIGINAL = [9, 13, -14, 17, 13, -19, 23, 21]
POINTS = list(itertools.product([0, 1], repeat=8))


def build():
    m = pyo.ConcreteModel()
    m.a = pyo.Var(
        range(8),
        domain=pyo.Integers,
        bounds=lambda m, j: (1, 40) if ORIGINAL[j] > 0 else (-40, -1),
    )
    m.b = pyo.Var(domain=pyo.Integers)
    m.B = pyo.Var(domain=pyo.NonNegativeReals)
    m.c = pyo.ConstraintList()
    for x in POINTS:
        lhs = sum(m.a[j] * x[j] for j in range(8))
        m.c.add(
            lhs <= m.b
            if sum(ORIGINAL[j] * x[j] for j in range(8)) <= 37
            else lhs >= m.b + 1
        )
    m.c.add(m.B >= m.b)
    m.c.add(m.B >= -m.b)
    m.obj = pyo.Objective(expr=m.B)
    return m


def check(m):
    a = [round(pyo.value(m.a[j])) for j in range(8)]
    b = round(pyo.value(m.b))
    assert all(
        (sum(ORIGINAL[j] * x[j] for j in range(8)) <= 37)
        == (sum(a[j] * x[j] for j in range(8)) <= b)
        for x in POINTS
    )


def tables(m):
    return {
        "coefficients": frame(
            [[f"x{j + 1}", ORIGINAL[j], pyo.value(m.a[j])] for j in range(8)]
            + [["RHS", 37, pyo.value(m.b)]],
            ["Term", "Original", "Equivalent"],
        )
    }


def plot(m):
    return (
        [f"x{j + 1}" for j in range(8)],
        [pyo.value(m.a[j]) for j in range(8)],
        "Equivalent signed coefficient",
    )

# Solve, audit constraints, and run domain-specific checks.
from models.common import solve, audit
model = solve(build())
audit(model)
check(model)
for name, result_table in tables(model).items():
    print(name)
    print(result_table.to_string(index=False))

18.4 Optimal Solution

The solver reports optimal termination. The objective is 25 absolute right-hand side (minimize). The largest violation across active constraints, variable bounds, and integer domains is 0.00e+00 in the corresponding model units. The problem-specific checks also pass. These checks establish numerical consistency with the stated model, not the validity of its assumptions for a real facility.

18.4.1 Coefficients

Term Original Equivalent
x1 9 6
x2 13 9
x3 -14 -10
x4 17 12
x5 13 9
x6 -19 -13
x7 23 16
x8 21 14
RHS 37 25
Figure 18.1: Selected quantities from the verified optimal solution. Units are stated on the axis.

Tables round numerical values for reading; feasibility checks use the original solver values. Multiple optimal decisions may exist. Machine-readable result records the solver status and package versions. Figure-generation code is in figures/workbook.py.

18.5 Brief Discussion

The minimum absolute right-hand side is 25, compared with 37 originally. All 256 binary assignments have the same feasibility status under the displayed replacement inequality.

Scaling an inequality by a positive constant preserves feasibility but need not give the simplest integer representation. Exact truth-table matching protects both feasible and infeasible assignments. The result is optimal within the stated coefficient bounds. Experiment: change the objective to the sum of coefficient magnitudes and compare the resulting inequality.