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

edit

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.