Using Symbolics to simplify Boolean algebra

Specific Domains Modelling & Simulations
1

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
2

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
3

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.

4

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

5

Thanks Chris,

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

Best wishes,
Tomas

2 Likes