Extending LINQ-based Specification Pattern to implement subsumption

Question

There are a lot of LINQ-based implementations of the Composite Specification Pattern. I have not seen one that used Subsumption.

Are there any such examples that have been documented (blogs, etc.) or published as open source? I have an idea and proof of concept for how this could work by having an ExpressionVisitor translate every specification into a canonical logical form (CNF/DNF), but I am concerned that this is overly complicated. Is there a better way?

Answer 1

I am concerned that this is overly complicated. Is there a better way?

The short answer is "No, there isn't" ¹

The long answer: The "overly complicated" captures the essence of the problem: it is NP-hard. Here is a short informal proof relying upon the fact that the satisfiability problem is NP-complete:

• Suppose that you have two Boolean formulas, A and B
• You need to test if A implies B, or equivalently ¬A | B for all assignments of variables upon which A and B depend. In other words, you need a proof that F = ¬A | B is a tautology.
• Suppose that the tautology test can be performed in polynomial time
• Consider ¬F, the inverse of F. F is satisfiable if and only if ¬F is not a tautology
• Use the hypothetical polynomial algorithm to test ¬F for being a tautology
• The answer to "is F satisfiable" is the inverse of the answer to "is ¬F a tautology"
• Therefore, an existence of a polynomial tautology checker would imply that the satisfiability problem is in P, and that P=NP.

Of course the fact that the problem is NP-hard does not mean that there would be no solutions for practical cases: in fact, your approach with the conversion to a canonical form may produce OK results in many real-world situations. However, an absence of a known "good" algorithm often discourages active development of practical solutions².

---

¹ With the obligatory "unless P=NP" disclaimer.

² Unless a "reasonably good" solution would do, which may very well be the case for your problem, if you allow for "false negatives".