# Solving a weighted XOR-SAT problem

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 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.

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.
• 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?
• @prubin The $Ax=1$ is really $Ax\equiv 1\mod 2$. We want each sum to be odd. Dec 18, 2023 at 18:14