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!
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}
ifMethod-> "SimulatedAnnealing"
is replaced byMethod->"DifferentialEvolution"
. $\endgroup$SimulatedAnnealing
since it didn't complain about non-convergence within the specified number of iterations. $\endgroup$