WIP: Optimize negation (depends on stratified-aggregation) #38
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…into improved-negation
guillembartrina
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR attempts to optimize the current implementation of stratified negation in carac.
The current implementation is extremely simple but also very wasteful: it keeps the set of all constants appearing anywhere in a fact or a rule; just before performing the n-way join to solve a rule, it computes the "virtual" relation corresponding to the negated atom by constructing a relation containing all possible combinations of constants of length equal to the arity of the negated atom and subtracting the relation from it. Note that this is a source of combinatorial explosion, and often most of the combinations of constants do not even make sense, since they come from other relations.
The optimized version gets rid of the global set of constants and instead of building a relation containing all possible combinations of constants of length the arity of the negated atom, first collects the constants that can appear in each of the arguments by performing a corresponding column intersection of the other relations in the rule that share a variable (at least there is one because the variables appearing in the negated atoms must be guarded), and then builds the relation containing all possible combinations of these collected constants. In this way, it only creates the combinations that "make sense".
For the general use case, the optimization may not be extremely noticeable but it is definitely no worse than the current implementation and also makes some now intractable problems tractable.
In addition, (almost) as a consequence of the new design, this PR also solves the case where we have anonymous variables appearing in negated atoms, which was not handled until now.