Higher-order set constraint elimination algorithm

[ctrekker]

Consider this scenario:

a = [1, 2]
b = [1, 2]
c = [1, 2, 3]

We cannot make any conclusions about a or b, but we can conclude that c must not be either 1 or 2, considering if it was the problem would become unsatisfiable between a and b. This problem can be taken as a special case of graph coloring, in which each color is an integer (in this case 1 2 or 3) and each variable (a b and c) is a node in a fully-connected graph. In fully reducible cases the graph coloring problem has a single solution.

This issue involves coming up with a moderately efficient (ideally O(n^2) or lower time complexity) algorithm for reducing an arbitrary scenario to its absolute simplest possible state.

See line 30 of set_equality.jl

[ctrekker]

First: reevaluate if this is even necessary after the refactor in #20 to use a "double recursive" form of the algorithm originally planned. I believe it is more stable in terms of output result now and scenarios like this could be impossible now.

[ctrekker]

First: reevaluate if this is even necessary after the refactor in #20 to use a "double recursive" form of the algorithm originally planned. I believe it is more stable in terms of output result now and scenarios like this could be impossible now.

Confirmed, this issue is still relevant. Here's an actual in-code equivalent of the mentioned scenario in the issue.

using Deductive

@symbols a b c
ES = ExtensionalSet
A = ES([ES([∅]), ES([ES([∅])]), ∅])
pattern = ES([ES([a]), ES([b]), c])

set_symbol_matches(pattern, A)

[ctrekker]

Here's a notebook outlining the algorithm: 🎈 Constrained Output Elimination.jl — Pluto.jl.pdf