How to solve a combined problem of IP, Boolean Satisfiability and Maximization?

ThemePark
11 ●1 ●3

I have a problem in mind that I want to solve, and after doing some research I believe it is a maximization problem that uses both Integer Programming and Boolean Satisfiability.

Now, it's easy enough for me to declare the variables, and assign them a range. But I simply don't know how to go on from there with Sage. So I was hoping that if I explain a thought up example of what I need to do, someone could point me in the right direction.

So I have some sum equations with a lot of variables, and all of the variables are positive integers, including zero. For example, one such equation could be like this:

(A or B) + (C or D or E)=10

This means, that at LEAST one combination of the variables in those two groups must sum up to 10. It could for example be A+C, B+D, A+E, but A+B doesn't matter. And there could be more than one combination thereof that sums up to 10, that also doesn't matter, just whether there's at least one that does.

Now I combine the sum equations I have, into groups, which is where the Boolean part comes in. Any such group can either be true or false. True, if all the sum equations can be solved, i.e. at least one combination in the equation sums up to the desired number. False, if even one of the equations cannot be solved.

So one such group could consist of two equations:

(A or B) + (C or D or E)=10

(A or D) + (B or E)=10

Because I have a lot of different variables, and a lot of equations, I doubt all the groups I will need to make, can all be solved, i.e. all are true. And that is where the Maximization problem comes in. The problem I actually need to solve, is to make as many as the aforementioned groups of equations True. Once I know this, and which groups and thus equations can be solved, I have my solution. And if there are more than one way to achieve the maximum number of solved groups, all those count and are of interest to me.

So this is where I'm at, with a problem I want to solve, and no idea on how to go about solving it with Sage.

add a comment

answered 4 years ago

Max Alekseyev

7061 ●9 ●54 ●166

updated 4 years ago

For technical details on solving MILP in Sage and examples, you can refer to the documentation.

As for your specific problem, let us enumerate all clauses appearing in the equations in arbitrary order. For each variable $Q$ present in clause number $i$ , let's introduce a binary indicator variable $s_{Q,i}$ telling whether variable $Q$ is taken from this clause. Also, let $t_{Q,i}$ be an integer variable with the value $Q\cdot s_{Q,i}$ , which is enforced by the constraints: $\begin{cases} t_{Q,i} \geq Q - L(1-s_{Q,i}), \\ t_{Q,i} \leq Q + L(1-s_{Q,i}), \\ t_{Q,i} \geq - L s_{Q,i}, \\ t_{Q,i} \leq L s_{Q,i}, \\ \end{cases}$ where $L$ is a large positive constant (larger than the maximum possible value for $|Q|$ ).

Now, without loss of generality, suppose that the clauses (A or B) and (C or D or E) in the equation (A or B) + (C or D or E)=10 have numbers 1 and 2, respectively. Then in addition to the above 4 inequalities for each pair $(Q,i)\in \{ (A,1), (B,1), (C,2), (D,2), (E,2)\}$ , we introduce the following constraints: $\begin{cases} s_{A,1} + s_{B,1} = 1, \\ s_{C,2} + s_{D,2} + s_{E,2} = 1, \\ t_{A,1} + t_{B,1} + t_{C,2} + t_{D,2} + t_{E,2} = 10.\qquad (\star) \end{cases}$ Here the first two constraints enforce that only one variable is taken from each clause, while the constraint $(\star)$ represents the equation itself.

Finally, to deal with the groups of equations, let's enumerate them, and for a group number $j$ let's introduce a binary indicator variable $p_j$ telling whether the group is satisfied. Suppose that the group formed by equations (A or B) + (C or D or E)=10 and (A or D) + (B or E)=10 has number $1$ . Then we replace the equation labeled $(\star)$ above, which corresponds to the first equation, with $\begin{cases} t_{A,1} + t_{B,1} + t_{C,2} + t_{D,2} + t_{E,2} \geq 10 - M(1-p_1), \\ t_{A,1} + t_{B,1} + t_{C,2} + t_{D,2} + t_{E,2} \leq 10 + M(1-p_1) \end{cases}$ and similarly for the second equation in the group, where $M$ is a large positive constant (larger than the maximum absolute value of the l.h.s. of the equations).

The objective function to maximize is $\sum_j p_j$ , which gives the number of satisfied groups of equations.

link

Comments

Alright, so before I posted this question, I had a look around the forum, and I noticed that a lot of commenters posted code as answers. So it threw me back that you decided to post math instead, and I've had to use some time to digest it all, as it's been a long time since I've had to deal with that notation.

I understand that the constants L and M are either zero, or their value, because you substract binary variables from 1. But I don't understand how choosing two large constants help enforce the constraints in those equations.

Also, since the s variable is binary, what happens if SC,2 and SE,2 are both 1? Because as I said, I need at least one combination to equal the sum, but not exactly one, there CAN be more.

Finally, I'm not sure how ...(more)

ThemePark ( 4 years ago )

Math is needed to solve the problem. My answer explains how to approach your problem. If you concern about actual Sage code, you'd need to give a particular example of the problem for illustration.

Constants $L$ and $M$ are not zero -- they must be large positive constants. Perhaps, you meant them multiplied by a coefficients, which may be 0 or 1. The idea is that whenever these constants come in the inequality with coefficient 1, the corresponding inequality becomes silent (i.e., automatically satisfied).

Both $s_{C,2}$ and $s_{E,2}$ cannot be 1 at the same time, because they must satisfy the constraint $s_{C,2}+s_{D,2}+s_{E,2} = 1$ . But there may exist one solution, say, with $s_{C,2}=1$ and $s_{D,2}=s_{E,2}=0$ , and another solution with $s_{E,2}=1$ and $s_{C,2}=s_{D,2}=0$ .

Max Alekseyev ( 4 years ago )

Overall, your question makes an impression that you have trouble with formalizing/posing your problem as MILP (which is quite irrelevant to Sage), and this is what my answer explains how to do. As soon as your problem is formalized as MILP, it can be solved with Sage or any other solver (e.g., CPLEX, Gurobi, etc.).

If you have troubles with Sage specifically within the context of your problem, please let me know what they are.

Max Alekseyev ( 4 years ago )

add a comment

How to solve a combined problem of IP, Boolean Satisfiability and Maximization?

1 Answer

Comments

Your Answer

Question Tools

Stats

How to solve a combined problem of IP, Boolean Satisfiability and Maximization? savecancel

1 Answer

Comments

Your Answer

Question Tools

Stats

How to solve a combined problem of IP, Boolean Satisfiability and Maximization?