Hi Denis, now I have some time to continue
denis_berthier wrote:What I want to recall in the context of this thread is that any claim that the first family above is universal is clearly false. A chain cannot be considered as a mere set of CSP-variables (base set) and constraints. In such a view, something would be lost: the order of the chain. As a result, the proof of validity the chain carries with it would also be lost (and the complexity of proving validity increased).
The elementary mathematical basis for this is (symbolically) "sequence = set + order relation on this set".
Apparently, you have problems with logic.
If I say that a sequence is more than a set, it doesn't mean that a sequence is not a set.
Maybe, you didn't understand my "symbolic" writing. Let me write it more formally: Seq = {Set, <}, where < is an order relation, i.e. some subset of SxS with the relevant properties of an order. If you forget the <, there remains the Set.
Your statement as it stands is absolutely true and I never questioned this. Its just unrelated to what I said. Your braids carry an order property because they were defined using order. My universal pattern are defined without any notion of order, but can nevertheless be verified. This is not any "better" or so, only more general.
Back to where I started: If you compute all valid permutations of e.g. number plane 1+2 and find a candidate that is not member of any of these permutations. This candidate is clearly false
and you have a perfect proof. Enumerating all possible cases for a finite problem is always a trivial proof. That was already clear in the discussion we had in another thread.
If we accept a permutation enumeration as "elimination", we are finished and move on with the next one. Even if the same elimination can be validated with less objects in a "simpler" way, its pointless to prove a fact that is already proven.
So moving into that direction needs another motivation in form of a secondary goal. Possible secondary goals must be clearly defined as comparison of results related to different goals make no sense. I think we also agree that any comparison is related to a well defined size function.
The motivation for "univeral pattern" is to define "acceptable elimations". The term
elimination pattern seem self-evident but is not. The set of all permutations of one or more planes is regarded as "not acceptable". On the other hand I wanted the definition to be as general as possible. I did not mention
uniqueness in my first post, because I was aware of the history of emotional discussions. Uniqueness undermines the comparabilty of results, that why I don't like it.
denis_berthier wrote:logel wrote:I rather see an advantage to have a definition covering all. Now its possible to define size for the most general class. This is especially important for pattern derived from level-one contradiction pathes, their size is calculated from the steps.
Unfortunately, until now your "universal pattern" X can solve all the puzzles only if you use it in T&E(X). So, what does universality mean here ?
As for "deriving the size from the steps", we already talked of this in the "Pattern-based classification of (hard) puzzles" thread, but you had no idea of how to do this, even in the simplest case of a sequence of Singles.
Moreover, when you use T&E, you don't get the shortest path, so any size definition for a "pattern derived from level-one contradiction pathes", i.e. based on T&E, is totally meaningless.
Here is a key misunderstanding.
All puzzles can be solved
without T&E at the base level with universal pattern. Thats the way they are defined. This is obvious as all eliminations are a result of
some reduction of the whole set of candidates. This justifies the attribute
universal. Of course its another thing to show an "optimal" elimination sequence explicitly. I never claimed that I can do this with reasonable computing. And I never claimed to have a magic algorithm to find the simplest universal pattern for a situation.
Of course you don't get the "shortest path" on a level-one contradiction path, but that does not make the construction useless. Each elimation pattern at the base level has a corresponding contradiction sequence at level-one consisting of (smaller) eliminations itself. And a well defined size function should consistently relate to the values of the elimations of the inverted logic.
Moreover any contradiction path from level-one can be reduced to a universal elimination. This requires some additional computation stripping off all redundant parts, but is manageable for all pathes. The reduction result may not be "optimal", but we can compute its size. So with T&E as auxiliary vehicle I can get a at least some solution consisting of a series of explicit universal pattern, but these solutions are far from satisfactory (optimal size).
denis_berthier wrote:Finally, I'll raise a question of methodology.
Your goals are extremely ambitious: you want to define a universal pattern (in a sense of "universal" still undefined); you want to define a rating based on the global solution path instead of the hardest step; and you want to deal with the hardest puzzles.
BUT:
- it appears that your "universal pattern" X can solve all the puzzles only if applied in T&E(X); we already know that a relatively simple pattern can do this (e.g. braids[7]); so X also should be rather simple;
- your rating is not defined for puzzles not solvable by X, i.e. it is defined only for relatively easy puzzles;
- if, based on X only, you ever define a rating for the total resolution path, it will have to deal with paths of paths of X-eliminations.
In view of my above remark about paths of Singles, this is obviously not a sustainable research program.
Why don't you forget about the hardest puzzles and T&E and why don't you merely solve a moderate level puzzle using only X ?
I can surely solve moderate puzzles as test cases, but finally it does not help. Reduced T&E is the inverted form of the direct logic.
Yes, rating for the total resolution path is a long term goal. But this was not intended to address in this thread.