Search code examples
linear-programminginteger-programmingconstraint-satisfaction

How to determine fixed and non-fixed variables in solutions to a integer satisfiability instance?

I have a (satisfiable) (linear) integer satisfiability problem. The problem contains, among others, a bunch of boolean-valued variables, call them x1...xn, with one of the constraints being that sum(x1...xn) = C. I wish to determine which of these variables are fixed, and the fixed values of said variables (as in: which of these variables take a specific value (0 or 1, as these are again boolean valued) in all possible solutions).

I have a working solution, it's just slow (to put it mildly):

  1. Add a constraint that x1 == 0
  2. Check if the problem is solvable
  3. Remove the constraint added in step 1.
  4. Add a constraint that x1 == 1
  5. Check if the problem is solvable
  6. Remove the constraint added in step 4
  7. Assert that at least one of 2 and 5 succeeded.
  8. If both succeeded, the variable is not fixed. Otherwise, the variable is fixed to whichever constraint the problem was still satisfiable under.
  9. Repeat 1...8 for x2...xn

The problem with this is that it's slow. In particular, it requires solving the problem O(n), or rather 2*n, times. (I'm passing in the previous solution to warm-start the solver, but just starting the solver is taking almost all the time.)

Is there a faster method? In particular, one that requires calling the solver less times?

Something I was thinking of, that unfortunately doesn't work as-is, is to turn it into a ILP problem and solve it twice, once with the objective of maximizing sum(x1...xn), one with the objective of minimizing the same, and checking which variables change. Unfortunately, this doesn't work in general. For (counter)example: boolean variables x and y, where x+y=1. Maximizing and minimizing can yield the same thing even though neither variable is fixed.

Solution

  • It would appear as though I have a solution to my own question. It's not ideal, and as such I'd accept other answers, but here goes:

    1. Turn the ILSAT into a ILP.
    2. For each variable to check, set seenTrue and seenFalse for that variable to False
    3. Set the objective function to maximize the sum of variables that have been seen to be False but not True, minus the sum of variables that have been seen to be True but not False.
    4. Solve the ILP.
    5. If none of the values that are not known to be unknown have changed since last iteration, break to 8.
    6. For each variable in the solution, set seenTrue or seenFalse to True, depending on if the variable is True or False.
    7. Goto 2
    8. For each variable, if it was only seen to be one of True or False, the variable is fixed to that value. Otherwise (it has been seen to be both) it is not fixed.

    Effectively what I'm doing is always trying to maximize the number of variables set to values that they haven't already been set to.