Minimize Number of Boolean Formulas that Evaluate to True

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),
ReduceFreeVariables[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!

• It works for me for Table[First@AbsoluteTiming[jossolver[genexample[100, 100]]], {20}], outputting {15.8332, 14.9384, 14.5264, 14.6845, 14.5709, 14.5643, 14.7029, 14.6103, 14.6754, 14.5772, 14.6466, 14.6076, 14.5993, 14.6325, 14.7242, 14.7133, 14.7002, 15.6228, 14.9258, 14.6775} if Method-> "SimulatedAnnealing" is replaced by Method->"DifferentialEvolution". – user64494 Feb 24 at 8:54
• Indeed, good point. Swapping out the optimizer seems to yield a speedup; I originally used SimulatedAnnealing since it didn't complain about non-convergence within the specified number of iterations. – J Bausch Feb 24 at 11:28

Replacing the NMinimize part of you code by

NMinimize[Total@(Mod[#, 2] & /@ alg),
ReduceFreeVariables[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.).