# Using Symbolics to simplify Boolean algebra

Dear All,

I would like to ask, if it would be possible to use Symbolics to simplify Boolean rules. For example

``````using Symbolics
x =  SymbolicUtils.Sym{Real}(:x)
simplify((x > 1) & (x > 2))
``````

should return `(x > 1)`?

Or am I doing something wrong?
Thanks a lot for help in advance.

1 Like

The problem is, that I do it wrongly. I need to teach Symbolics the rules

``````using Symbolics, SymbolicUtils
x =  SymbolicUtils.Sym{Real}(:x)

simplify((x > 1) & (x > 2))

INEQUALITY_RULES = [
@rule (~x > ~a) & (~x > ~b) => ~x > max(~a, ~b)
@rule (~x >= ~a) & (~x >= ~b) => ~x >= max(~a, ~b)
@rule (~x > ~a) | (~x > ~b) => ~x > min(~a, ~b)
@rule (~x >= ~a) | (~x >= ~b) => ~x >= min(~a, ~b)
@rule (~x < ~a) & (~x < ~b) => ~x < min(~a, ~b)
@rule (~x <= ~a) & (~x <= ~b) => ~x <= min(~a, ~b)
@rule (~x < ~a) | (~x < ~b) => ~x < max(~a, ~b)
@rule (~x <= ~a) | (~x <= ~b) => ~x <= max(~a, ~b)
]

inequality_simplifier() = SymbolicUtils.Chain(INEQUALITY_RULES)
``````

and with that it works like a charm

``````julia> simplify((x > 1) & (x > 2), rewriter = inequality_simplifier())
x > 2
``````
2 Likes

Still, I admit that I failing a bit. I am interested in simplifying logic rules

``````x1 =  SymbolicUtils.Sym{Real}(:x1)
x2 =  SymbolicUtils.Sym{Real}(:x2)
s = (((!(x1 >= 1.46) & !(x2 >= 1.4)) & !(x1 >= 1.42)) & !(x2 >= 1.42)) & (x2 <= -1.42)
``````

But I am totally failing.
I have extended the rules

``````INEQUALITY_RULES = [
@rule (~x > ~a) & (~x > ~b) => ~x > max(~a, ~b)
@rule (~x >= ~a) & (~x > ~b) => ~x >= max(~a, ~b)
@rule (~x > ~a) | (~x > ~b) => ~x > min(~a, ~b)
@rule (~x >= ~a) | (~x >= ~b) => ~x >= min(~a, ~b)
@rule (~x >= ~a) | (~x > ~b) => ~x >= min(~a, ~b)
@rule (~x < ~a) & (~x < ~b) => ~x < min(~a, ~b)
@rule (~x <= ~a) & (~x <= ~b) => ~x <= min(~a, ~b)
@rule (~x < ~a) | (~x < ~b) => ~x < max(~a, ~b)
@rule (~x <= ~a) | (~x <= ~b) => ~x <= max(~a, ~b)
@rule !(~x < ~a) => ~x >= ~a
@rule !(~x > ~a) => ~x <= ~a
@rule !(~x <= ~a) => ~x > ~a
@rule !(~x >= ~a) => ~x < ~a
@acrule (~x & ~y) & ~z  => ~x & (~y & ~z)
]

inequality_simplifier() = SymbolicUtils.Chain(INEQUALITY_RULES)

function extended_simplifier()
SymbolicUtils.Chain([inequality_simplifier(), SymbolicUtils.serial_expand_simplifier])
end

s = ((x1 < 1.42) & (x2 < 1.42) & (x2 <= -1.42))
simplify(s, rewriter = extended_simplifier())
``````

but this runs forever. The solution should be trivial to `x1 < 1.42 & x2 <= -1.42`. Any help is appreciated.

Open an issue. We should add these to the rule set, but you do need to make sure it’s a terminating set.

Thanks Chris,

I have created an even simpler MWE and put it to the issue

I guess in that MWE example, the e-graph should saturate.

Best wishes,
Tomas

2 Likes