3
$\begingroup$

Is it possible for Mathematica to do simplifications for expressions where the variables are binary, such as:

a + b = 1 + 2*c => a + b = 1

Here c must be 0 because if it is 1, the RHS is 3 but the LHS can be at most 2.

a + 2*b*a + 2*c = 2*d => c=d

Here the LHS is: a(1+2*b) + 2*c. The RHS must be even, so the LHS must be even. But (1 + 2*b) can never be even, so 'a' must be 0.

I looked at Simplify[ ] and FullSimplify[ ] using assumptions, and various other stackexchange questions, but to my surprise this doesn't seem possible in Mathematica.

Edit:

I want to comment on the answer by Algohi, but can't seem to add an image to the comment. What Algohi is doing solves the binary equations, but what I need is the simplified equations (a + b = 1, and c=d). I would have to convert the boolean expressions in that answer to equations:

boolean expression / binary equation equivalence

However I can't find a way to do this in Mathematica. If I could convert back & forth easily, I would have converted the equations to a boolean expression and then used BooleanMinimize[ ] to simplify.

Improve this question
$\endgroup$
4
  • $\begingroup$ You mention in a comment (to my response) that you might have in the thousands of variables. Do you also have a large number of equations? I bring this up because if there are but few, the approach with GroebnerBasis might still be viable (whether it would give a useful simplification in general is another matter though). $\endgroup$
    – Daniel Lichtblau
    Jan 8, 2015 at 18:36
  • $\begingroup$ @DanielLichtblau In my paper link we simplified Eqs 1-6 into Eqs. 7-9 (14 variables -> 4 variables). For factoring RSA-100 we have 330 equations (we reduced ~2500 variables to 2165). For RSA-220 we have 729 equations (we reduced ~5000 variables to ~4500). All variables were reduced using an "in-house" Python program we wrote from scratch. Being commercial software with professional developers, we thought FullSimplify should surely do better. Each variable becomes a qubit, so we want to remove as many as possible! $\endgroup$
    – user1271772
    Jan 9, 2015 at 4:52
  • $\begingroup$ (1) FullSimplify has as its charter, approximately, to reduce leaf count. It might or might not be able to do this is an equational setting but it would need appropriate "side relations" (e.g. x^2==x for all variables x). It is far more reliable to work with functionality dedicated to such a task. $\endgroup$
    – Daniel Lichtblau
    Jan 9, 2015 at 16:01
  • $\begingroup$ (2) I have tried integer factorization via the 0-1 linear reformulation of quadratic programming. It has been an altogether unsuccessful experiment, one that I buried several years ago. In a multiple qubit world it might be a different matter of course. $\endgroup$
    – Daniel Lichtblau
    Jan 9, 2015 at 16:05

4 Answers 4

Reset to default
4
$\begingroup$

Could use GroebnerBasis as below.

rels = {a^2 - a, b^2 - b, c^2 - c};
gb = GroebnerBasis[Join[{a + b - (1 + 2 c)}, rels], {a, b, c}];
Thread[Complement[gb, rels] == 0]

(* Out[337]= {-1 + a + b == 0, c == 0} *)

Here it is packaged into a function:

binarySimplify[eq_, vars_] :=
 Module[{rels, gb},
  rels = (#^2 - # &) /@ vars;
  gb = GroebnerBasis[Join[{eq /. Equal -> Subtract}, rels], vars];
  Simplify@Thread[Complement[gb, rels] == 0]]

For example,

binarySimplify[a + 2 b a + 2 c == 2 d, {a, b, c, d}]
(* {a == 0, c == d} *)
Improve this answer
$\endgroup$
10
  • 1
    $\begingroup$ Nice solution! I wanted to try it on other examples, so I took the liberty of packaging it into an easier-to-use function and adding it to your answer. I hope you don't mind; feel free to roll back the edit if you don't want it. $\endgroup$
    – user484
    Jan 6, 2015 at 16:38
  • 1
    $\begingroup$ @Rahul Thanks, that seems like a useful improvement. $\endgroup$
    – Daniel Lichtblau
    Jan 6, 2015 at 17:54
  • $\begingroup$ Are you using the fact that if the variables can only take 0 and 1 values they must be idempotent when adding rels? $\endgroup$
    – Carlo
    Jan 6, 2015 at 22:40
  • $\begingroup$ @Carlo I'm not sure what you are asking. The relations rels that I use enforce that the variables can only be 0 or 1. $\endgroup$
    – Daniel Lichtblau
    Jan 6, 2015 at 22:54
  • 1
    $\begingroup$ As for removing Groebner bases, yeah, you could perhaps work with Reduce and omit the Integers domain specification. But then you might need to do some variation on branch-and-prune to get back to integer-land. Or maybe reverse that, do an HermiteDecomposition (enforces integrality) and follow up with the inequalities. $\endgroup$
    – Daniel Lichtblau
    Jan 8, 2015 at 0:07
1
$\begingroup$

The following should do what you want

eqnToBool={Times->And,Plus->Xor,i_Integer:>OddQ[i]};
boolToEqn={And->Times,Xor->Plus,True->1,False->0};
eqToRules={Equal->Rule};
reduceBool[eq_]:=Resolve[Exists[{},eq/.eqnToBool],Booleans]


simplifyBool[eq_]:=Module[{newEqns={}},
  FixedPoint[Simplify[#/.(If[Head@#=!=Symbol,AppendTo[newEqns,#/.boolToEqn]/.eqToRules,{}]&)[reduceBool[#]]]&,eq];
  newEqns
]

It uses Resolve to infer the properties of some of the variables. It then simplifies the equation based on these inferences and repeats until the equation can no longer be simplified.

simplifyBool[a + b == 1 + 2*c]
(*{a + b == 1, c == 0}*)

simplifyBool[a + 2*b*a + 2*c == 2*d]
(*{a == 0, c == d}*)
Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ This is a neat approach, but it thinks the solution to a + b + c == 3 is {a + b + c == 1}. $\endgroup$
    – user484
    Jan 6, 2015 at 6:47
  • $\begingroup$ Why does it think a + b + c = 1 ? The solution should clearly be a = b = c = 1 $\endgroup$
    – user1271772
    Jan 6, 2015 at 7:28
  • $\begingroup$ The issue is that the transformation to boolean is imposing (in effect) that we are working mod 2. That is not actually what is called for, in this case. $\endgroup$
    – Daniel Lichtblau
    Jan 6, 2015 at 21:19
1
$\begingroup$ 
Reduce[Join[{a + b == 1 + 2 c, {a, b, c} \[Element] Integers}, 
  0 <= # <= 1 & /@ {a, b, c}]]

(*(a == 0 && b == 1 && c == 0) || (a == 1 && b == 0 && c == 0)*)

Reduce[Join[{a + 2 b a + 2 c == 2 d, {a, b, c, d} \[Element] 
    Integers}, 0 <= # <= 1 & /@ {a, b, c, d}]]

(*(a == 0 && b == 0 && c == 0 && d == 0) || (a == 0 && b == 0 && 
   c == 1 && d == 1) || (a == 0 && b == 1 && c == 0 && 
   d == 0) || (a == 0 && b == 1 && c == 1 && d == 1)*)

For your update:

rule[exp_, vari_List] := 
 Cases[#, {x_, Max[#[[;; , 2]]]} :> x] &@
  Tally[Cases[
    Reduce[Join[{exp, vari \[Element] Integers}, 
      0 <= # <= 1 & /@ vari]], Equal[x_, 0] :> Rule[x, 0], -1]]

Now:

Simplify[# /. rule[#, {a, b, c}] &@(a + b == 1 + 2 c)]

(*a + b == 1*)

Simplify[# /. rule[#, {a, b, c, d}] &@(a + 2 b a + 2 c == 2 d)]

(*c == d*)
Improve this answer
$\endgroup$
1
  • $\begingroup$ Your solution does not do what my question asked (reduce the equations to a + b = 1, and c=d respectively). I have further clarified this in my edit above. $\endgroup$
    – user1271772
    Jan 6, 2015 at 8:06
1
$\begingroup$

Have you tried these substitution?

ReplaceAll[
    ReplaceAll[
        a + b == 1 + 2*c,
        {Times -> And, Plus -> Xor, i_Integer :> OddQ[i]}
    ],
    {And -> Times, Xor -> Plus, True -> 1, False -> 0}
]

Or something along these lines?

I also think your second example is wrong, because when you're performing a computation mod 2, anything you multiply by 2 is multiplied by 0. So your second equation would become a == 0.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Dear Carlo, the calculation is not being done ( mod 2 ). The functions map variables in {0,1} to the set of all integers. $\endgroup$
    – user1271772
    Jan 2, 2015 at 16:53

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.