My scenario has various flavors of SAT, constrained quadratic pseudo-Boolean, and integer programming. My attempts to formalize and solve the problem with Z3's QF_LIA
optimizer have fallen flat, which leads me to wonder if perhaps there is an alternative formulation of the problem, and a solver that might have better performance characteristics. Any advice is appreciated.
I have:
- A set $V$ of Boolean variables: $V = \{v_i\}$. For a "large" instance, $|V| \approx 6,000$.
- A set $P \subseteq V \times V$. For the same "large" instance, $|P| \approx 140,000$.
- A set of constraints $C \subseteq V \times V$: if $(x,y) \in C$, then $x \wedge y \neq 1$. For the same "large" instance, $|C| \approx 4,000$.
- A weight function $w_1 : V \mapsto \mathbb{N}$ (i.e., a total function on $V$).
- A weight function $w_2 : P \mapsto \mathbb{N}$, which is mostly unrelated to $w_1$, except that $\forall v_i,v_j. w_2(v_i,v_j) \leq min(w_1(v_i),w_1(v_j))$. $w_2$ can be thought of as either:
- A total function on $P$
- A partial function on $V \times V$
- A total function on $V \times V$, where $w_2(x,y) = 0$ if $(x,y) \notin P$.
I want: an assignment $Asg : V \mapsto \mathbb{B}$ such that:
- Satisfies all constraints: $\forall (v_i,v_j) \in C$, $Asg(v_i) \wedge Asg(v_j) \neq 1$.
- Maximizes $\sum_{v_i \in V} Asg(v_i)*w_1(v_i) + \sum_{(v_i,v_j) \in P} Asg(v_i)*Asg(v_j)*w_2(v_i,v_j)$
- I.e., maximizes $w_1$ on $V$ and $w_2$ on $P$ simultaneously.