Issue878

Title Output information about equivalent variable-value pairs in full encoding
Priority wish Status chatting
Superseder Nosy List cedric, florian, gabi, jendrik, malte, silvan
Assigned To Keywords translator
Optional summary

Created on 2018-12-12.15:38:21 by florian, last changed by silvan.

Messages
msg8267 (view) Author: malte Date: 2018-12-12.15:57:43
To be clear, the problem in issue771 is that we could get a *quadratic* number
of mutexes, not an exponential one. With N ground facts, there can never be more
than N^2 mutexes.

An algorithm that would "multiply out" multiple representations of atoms in a
mutex group would be exponential, but that just means that this would be an
unreasonable way to represent these mutexes. The problem here is that O(N^2) is
already too large.
msg8261 (view) Author: florian Date: 2018-12-12.15:38:21
In the full encoding, an atom can be represented by more than one variable-value
pair. If this happens, there can be exponentially many mutex groups, so we do
not generate them (see issue771). However, we could generate information of the
type "var1=val4 is equivalent to var3=val0" which might be useful for some
heuristics.
History
Date User Action Args
2018-12-12 16:02:51silvansetnosy: + silvan
2018-12-12 15:57:43maltesetstatus: unread -> chatting
messages: + msg8267
2018-12-12 15:39:32cedricsetnosy: + cedric
2018-12-12 15:38:21floriancreate