I want to solve a variant of the weighted XOR-SAT problem. Concretely,

Given $n$ boolean variables $x_1,\ldots,x_n$ each of which is assigned a non-negative cost $c_1,\ldots,c_n\in\mathbb{R}_{\ge 0}$ and a boolean function $f$ on these variables given in the form $$f(x_1,\ldots,x_n)=\bigwedge_{i=1}^k\bigoplus_{j=1}^{l_i}x_{r_{ij}}$$ ($\oplus$ denoting XOR) with $k\in\mathbb{Z}_{>0}$, integers $1\leq l_i\leq n$ and $1\leq r_{i1}<\cdots<r_{il_i}\leq n$ for all $i=1,\ldots,k$, $j=1,\ldots,l_i$, the problem is to find an assignment of minimum cost for $x_1,\ldots,x_n$ that satisfies $f$, if such an assignment exists. The cost of an assignment is simply given by $$\sum_{\substack{i\in\{1,\ldots,n\}\\x_i\,\text{true}}}c_i.$$

This problem is essentially XOR-SAT with a linear objective. The difference between my formulation and the one in the linked question above is that $c_i$ can take values in $\mathbb{R}_{\ge 0}$ instead of $\mathbb{Z}_{> 0}$.

How do I solve it with an off-the-shelf solver, like OR-Tools or Gurobi? By "solve it", I mean finding a solution that is good enough in a reasonable amount of time, not finding the optimal solution exactly. This problem is NP-complete after all.


1 Answer 1


Introduce a nonnegative integer variable $y_i$ and minimize $\sum_j c_j x_j$ subject to $Ax=2y+1$, where $Ax=1$ is the system of equality constraints defined in the linked question. The role of $y$ is to convert an equality in $\mathbb{F}_2$ to an equality in $\mathbb{R}$, which is what an off-the-shelf MILP solver supports.

  • $\begingroup$ I'm missing something here. The constraint $f(x)$ true here becomes $Ax=1,$ right? Why do we need $y$ Doesn't its presence turn XOR to OR? $\endgroup$
    – prubin
    Dec 18, 2023 at 18:11
  • $\begingroup$ @prubin The $Ax=1$ is really $Ax\equiv 1\mod 2$. We want each sum to be odd. $\endgroup$
    – RobPratt
    Dec 18, 2023 at 18:14
  • $\begingroup$ My bad. I thought the multiple input version of XOR meant exactly one input must be 1, but Wikipedia agrees with you. $\endgroup$
    – prubin
    Dec 19, 2023 at 23:09
  • $\begingroup$ CP-SAT supports both xor and floating point coefficients $\endgroup$ Dec 22, 2023 at 14:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.