Formalizing and optimizing constraints involving booleans, pairs of booleans, and integer sums 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.
Can this be reformulated as follows (careful, I am sleep-deprived with a cranky toddler in the room):

We are looking at a random graph $G$ with 6000 weighted nodes, a subgraph $G'$ induced by about 4000 edges, and 140.000 other weighted edges of positive weight but strictly smaller than the nodes they connect to.

A satisfying assignment for $C$ induces a bipartite subgraph of $G'$ (all nodes with assignment 1 plus their immediate neighbors with assignment 0). So you are looking to optimize over the set of bipartite subgraphs of $G'$?

A few random thoughts:


How structured are $G$ and $G'$? I presume a random graph model is not a very good model? What is the distribution of degrees of nodes?
Are all nodes in $G'$?


Is there a way we can bound the sum of all $w_2$-induced weights for given node? We know that the node weight $w_1(v)$ is bigger than the edge weight $w_2(v, \centerdot)$, is there something to be said for $\sum_{v_2 \in V} w_2(v, v_2)$? That could give some information about whether "switching a node on" is worth it...

If nodes have a tendency to outweigh the sum of their edges, would that hint at a bigger bipartite subgraph being always better than a smaller one, and at the problem becoming one of maximizing the size of the bipartite subgraph?