2
$\begingroup$

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!

$\endgroup$
2
  • 2
    $\begingroup$ 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". $\endgroup$
    – user64494
    Feb 24, 2021 at 8:54
  • $\begingroup$ 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. $\endgroup$
    – J Bausch
    Feb 24, 2021 at 11:28

1 Answer 1

1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.