I have 8192 bits, denoted $b_0, b_1, ..., b_{8191}$. The bits are subject to some XOR constraints (e.g. $b_0 \oplus b_3 \oplus b_{42} \oplus \cdots \oplus b_{8191} = 1$). The objective function to be minimized looks like $\sum_{i=0}^{2047} f_i(b_{4i}, b_{4i+1}, b_{4i+2}, b_{4i+3})$, that is, it is the sum of $2048$ functions defined on $\mathbb{F}^4 \to \mathbb{R}$. The constraint is a classic SAT problem (guaranteed feasible), but how do I formulate the objective?
One idea is to solve the problem approximately by linearizing the objective, i.e. define something like
\begin{equation} g_0(b) = \begin{cases} \frac{1}{8}\sum_{(b_1, b_2, b_3) \in \mathbb{F}^3} f_0(0, b_1, b_2, b_3), &b = 0 \\ \frac{1}{8}\sum_{(b_1, b_2, b_3) \in \mathbb{F}^3} f_0(1, b_1, b_2, b_3), &b = 1 \\ \end{cases} \end{equation}
We then pretend that the objective is linear, i.e. $\sum_{j=0}^{8191} g_i(b_i)$. However, I still don't know how to impose a linear objective on an SAT problem.
One approach is to use binary search on the value of the objective function. In other words, pick a constant $\alpha$, and add a constraint that the objective is $\ge \alpha$. Test feasibility of the resulting system, with a SAT solver. Repeat, doing binary search to find the largest $\alpha$ such that the resulting system is feasible.
You can formulate this constraint by building a circuit that adds up all of the terms in the sum and compares to $\alpha$, then apply the Tseitin transform to this circuit. Or, some SAT solvers have built-in support for pseudo-boolean constraints of this sort.
Given the number of XOR constraints, in practice, you might find CryptoMiniSAT useful.
Alternatively, you can formulate this as an instance of integer linear programming and use an off-the-shelf ILP solver. This lets you natively express the sum of these terms and maximize the sum, but you have to convert all the boolean functions to ILP. See https://cs.stackexchange.com/q/12102/755 for how to do that conversion.