Compilation to Integer Linear Programming

• Motivations

  • Ability to handle numeric quantities, and do optimization
  • Heuristic value of the LP relaxation of ILP problems

• Conversion

  • Convert a SAT/CSP encoding to ILP inequalities
    • E.g. X v ~Y v Z => x + (1 - y) + z >= 1
  • Explicitly set up tighter ILP inequalities
    • If X,Y,Z are pairwise mutex, we can write x+y+z <= 1
      (instead of x+y <=1 ; y+z <=1 ; z +x <= 1)

[ Walser & Kautz;

Vossen et. al;

Bockmayr & Dimopolous]

ILP: Given a set of real valued variables, a linear objective function on the variables,

a set of linear inequalities on the variables, and a set of integrality restrictions on the variables, Find the values of the feasible variables for which the objective function attains the maximum value

-- 0/1 integer programming corresponds closely to SAT problem

Previous slide

Next slide

Back to first slide

View graphic version