arrays - Reducing complex filter rules to a comparable form

Question

I want to determine whether or not an input array of integers "matches" a set of rules.

The Matcher

The Matcher is built from a set of helper methods to describe rules for input data. These rules are essentially logic gates on arrays of integers:

AND(1, 2) // Requires both 1 AND 2 be present in the input array.
OR(3, 4, 5) // Requires that 3 OR 4 OR 5 be present in the input array.
NOR(6, 7) // Requires that neither 6 NOR 7 be present in the input array.
XOR(8, 9) // Requires that either 8 (X)OR 9 be present in the input array, but not both.

Thus, I could say that, given the input array:

[0, 1, 2, 3]

I could build a Matcher like:

AND(OR(0, 1), AND(1, 2) NOR(4))

Which would match the input, because the input satisfies:

OR(0, 1) // 0 or 1 is present
AND(1, 2) // Both 1 and 2 are present
NOR(4) // 4 is not present

And each of those cumulatively satisfies the overarching AND rule.

The Problem

I need to reduce matchers to the simplest and most basic form that still describes the rules. For example, given the above matcher, a sample reduction could be:

rules = {
  or: [1, 2],
  xor: [], // No XORs
  nor: [4]
}

Each rule has three arrays of sub-rules, comprised of integers or rules.

Notice that the ORs are empty, because 1 is required anyways, which means OR(0, 1) => [0, 1] is redundant because it must be satisfied.

Since Matchers need to be comparable (I need to be able to determine an equivalence between the underlying rules), it becomes a bit more complicated when I get to:

input = [1, 2, 5, 9, 11, 12, 13, 14, 17]

XOR(OR(AND(1, 2), NOR(3, 4), XOR(3 11), AND(11, 14)), AND(1, 5, 17))

Now, a large amount of that is redundant and/or contradictory, so what I was thinking I could do was first place it into a tree-like structure, and then recurse it and reduce unnecessary entries. Any ideas for a better way to do this?

I'm specifically looking for something deterministic (any set of input rules that mean the same thing yield the same final reduced form). If there is a better way to express this problem, I'm interested, and if rules are contradictory it's fine for the reducer to break and throw an exception. This is intended for occasional use in the program, so performance is not much of an issue.

Answer 1

What you are actually dealing with here is propositional logic. Consider the integer your propositions being either false or true depending on whether they are present in the input array.

Your constraints (XOR, AND, etc.) then form a logical formula that is either satisfiable or not. It is in fact hard to figure out for any given formula whether it is satisfiable. However, at first sight this shouldn't concern you because you only have to check whether a given input satisfies the formula.

Unfortunately what you are actually asking is how you can determine whether two propositional formulas are equivalent. It turns out this is equally hard: https://math.stackexchange.com/questions/1050127/how-to-efficiently-determine-if-any-two-propositional-formulas-are-equivalent