Minimize Number of Boolean Formulas that Evaluate to True

Question

I'm interested in a MinSat variant: given a list of boolean formulas like

example1 = {a[1] ⊻ a[3] ⊻ a[4] ⊻ a[6] ⊻ a[10],  a[3] ⊻ a[4] ⊻ a[5] ⊻ a[6] ⊻ a[7],  a[3] ⊻ a[5] ⊻ a[8]}
example2 = {a[1] ⊻ a[2], a[2] ⊻ a[6] ⊻ a[10],  a[2] ⊻ a[9],  !(a[6] ⊻ a[9])}

find an assignment to the a[i] that minimizes the total number of formulas in the list that evaluate to True.

More information: The formulas all look like Xor[..., ..., ...] or Not@Xor[..., ..., ...]. The number of variables and clauses is not fixed; code to create samples of this form is

genexample[m_Integer, n_Integer] := Xor @@@ Table[
    ({True}~Join~Table[a[i], {i, 1, n}]) RandomChoice[{.8, .2} -> {0, 1}, n + 1] // Total,
    {m}
  ] // DeleteCases[_Integer|True|False]

My own crude way of solving this so far is using NMinimize, in the following fashion:

jossolver[example_]:=Module[{alg},
 (* translate to a list of algebraic expressions *)
 alg = example /. {Xor -> f, Not -> g} //. {g[sth_] :> 1 + sth, 
    f[sth__] :> Total@{sth}};
 
 (* minimize sum of terms, each taken modulo 2 *)
 NMinimize[
   Total@(Mod[#, 2] & /@ alg), 
   Reduce`FreeVariables[alg] \[Element] Integers,
   Method -> "SimulatedAnnealing"
 ] /. Rule[var_, val_] :> (var -> Mod[val, 2])
]

This is of course neither optimized, nor elegant, nor something that works well for large m and n; it might not even find the global minimum. It works reasonably ok for, say, n=m=20, but if possible I'd like to solve such instances for m=n=100 or even larger within a few seconds (or faster?).

Approximate solutions (such as mine) are not ideal, but ok.

"Fast" is of course subjective; I'm just interested in a solution that's faster than what I tried. I realize of course that this problem is NP hard, but that doesn't mean one cannot solve small instances reasonably quickly. On my machine I get

Table[First@AbsoluteTiming[jossolver[genexample[20, 20]]], {20}] // MeanAround
(* == 1.376 ± 0.013 *)

I'm grateful for any attempts!

Answer 1

Replacing the NMinimize part of you code by

NMinimize[Total@(Mod[#, 2] & /@ alg), 
Reduce`FreeVariables[alg] \[Element] Integers, Method -> "DifferentialEvolution", 
PrecisionGoal -> 2, AccuracyGoal -> 2, MaxIterations -> 200]

and executing

Table[First@AbsoluteTiming[jossolver[genexample[100, 100]]], {20}]//MeanAround

, I obtain

15.16[PlusMinus]0.13

and several warnings. It is difficult to improve your little commented code (A good code is a commented code.).