# Using Symbolics to simplify Boolean algebra

**URL:** <https://discourse.julialang.org/t/using-symbolics-to-simplify-boolean-algebra/68473>\
**Category:** Modelling & Simulations\
**Tags:** symbolics\
**Created:** [September 20, 2021, 3:27pm UTC](https://discourse.julialang.org/t/using-symbolics-to-simplify-boolean-algebra/68473 "2021-09-20T15:27:59Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![Tomas\_Pevny](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tomas_pevny/32/25466_2.png) [@Tomas\_Pevny](https://discourse.julialang.org/u/Tomas_Pevny)\
**Post date:** [September 20, 2021, 3:27pm UTC](https://discourse.julialang.org/t/using-symbolics-to-simplify-boolean-algebra/68473/1 "2021-09-20T15:27:59Z")

</div>

Dear All,

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

```julia
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.

---

<div class="post-metadata">

**Author:** ![Tomas\_Pevny](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tomas_pevny/32/25466_2.png) [@Tomas\_Pevny](https://discourse.julialang.org/u/Tomas_Pevny)\
**Post date:** [September 20, 2021, 5:37pm UTC](https://discourse.julialang.org/t/using-symbolics-to-simplify-boolean-algebra/68473/2 "2021-09-20T17:37:43Z")

</div>

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

```julia
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
julia> simplify((x > 1) & (x > 2), rewriter = inequality_simplifier())
x > 2

```

---

<div class="post-metadata">

**Author:** ![Tomas\_Pevny](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tomas_pevny/32/25466_2.png) [@Tomas\_Pevny](https://discourse.julialang.org/u/Tomas_Pevny)\
**Post date:** [September 20, 2021, 6:18pm UTC](https://discourse.julialang.org/t/using-symbolics-to-simplify-boolean-algebra/68473/3 "2021-09-20T18:18:44Z")

</div>

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

```julia
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

```julia
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.

---

<div class="post-metadata">

**Author:** ![ChrisRackauckas](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/chrisrackauckas/32/77_2.png) [@ChrisRackauckas](https://discourse.julialang.org/u/ChrisRackauckas)\
**Post date:** [September 20, 2021, 7:22pm UTC](https://discourse.julialang.org/t/using-symbolics-to-simplify-boolean-algebra/68473/4 "2021-09-20T19:22:45Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Tomas\_Pevny](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tomas_pevny/32/25466_2.png) [@Tomas\_Pevny](https://discourse.julialang.org/u/Tomas_Pevny)\
**Post date:** [September 20, 2021, 7:31pm UTC](https://discourse.julialang.org/t/using-symbolics-to-simplify-boolean-algebra/68473/5 "2021-09-20T19:31:58Z")

</div>

Thanks Chris,

I have created an even simpler MWE and put it to the issue  
[https://github.com/JuliaSymbolics/SymbolicUtils.jl/issues/371](https://github.com/JuliaSymbolics/SymbolicUtils.jl/issues/371)  
I guess in that MWE example, the e-graph should saturate.

Best wishes,  
Tomas