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)
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