# Simplify binary expressions

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

• 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). Jan 8, 2015 at 18:36
• @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! Jan 9, 2015 at 4:52
• (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. Jan 9, 2015 at 16:01
• (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. Jan 9, 2015 at 16:05

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}];

(* Out= {-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];


For example,

binarySimplify[a + 2 b a + 2 c == 2 d, {a, b, c, d}]
(* {a == 0, c == d} *)

• 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.
– user484
Jan 6, 2015 at 16:38
• @Rahul Thanks, that seems like a useful improvement. Jan 6, 2015 at 17:54
• Are you using the fact that if the variables can only take 0 and 1 values they must be idempotent when adding rels? Jan 6, 2015 at 22:40
• @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. Jan 6, 2015 at 22:54
• 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. Jan 8, 2015 at 0:07

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={}},
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}*)

• This is a neat approach, but it thinks the solution to a + b + c == 3 is {a + b + c == 1}.
– user484
Jan 6, 2015 at 6:47
• Why does it think a + b + c = 1 ? The solution should clearly be a = b = c = 1 Jan 6, 2015 at 7:28
• 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. Jan 6, 2015 at 21:19
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)*)


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

• 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. Jan 6, 2015 at 8:06

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.

• Dear Carlo, the calculation is not being done ( mod 2 ). The functions map variables in {0,1} to the set of all integers. Jan 2, 2015 at 16:53