# 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). – Daniel Lichtblau Jan 8 '15 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! – user1271772 Jan 9 '15 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. – Daniel Lichtblau Jan 9 '15 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. – Daniel Lichtblau Jan 9 '15 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. – Rahul Jan 6 '15 at 16:38
• @Rahul Thanks, that seems like a useful improvement. – Daniel Lichtblau Jan 6 '15 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? – Carlo Jan 6 '15 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. – Daniel Lichtblau Jan 6 '15 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. – Daniel Lichtblau Jan 8 '15 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}. – Rahul Jan 6 '15 at 6:47
• Why does it think a + b + c = 1 ? The solution should clearly be a = b = c = 1 – user1271772 Jan 6 '15 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. – Daniel Lichtblau Jan 6 '15 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. – user1271772 Jan 6 '15 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. – user1271772 Jan 2 '15 at 16:53