@freemo Just wrote a program that presents such a problem. Due to time constraints we wrote it for 3x3 rather than 5x5 or whatever it normally is. But I wrote the clues manually, as I proved them out, and resolved the puzzle myself. I came up with 5 templated sets of rules and then we shuffle different entities and attributes through the puzzle. But I am considering expanding it to the full size puzzle at some point, and assume there should be some straight forward way to create all the "facts" relationships etc.. To come up with rule sets.

One explanation was to come up with all the possible "facts" (since they are definitely finite) then somehow determine that some number of them would be sufficient to solve it. Or something like that.

@Absinthe Well any solution that designs a valid clue set would also have to be able to solve the problem. You can only verify the clue set is valid if it produces a solution.

But it doesnt need to be random in any way.. like you dont need to generate random clues then test, you can generate the clues predictively.

But regardless any such system will be one step away from a solver at best.

@freemo well, I think there is something to generating all possible clues.

Within any given column there is a direct positive and or set of negative clues relative to every other elements in that same column.

And for any element in any column will have positive and negative relationships either "left of" "right of" "next to" or possibly "between" (which would be relative to two other column values.)

@Absinthe yea should be doable.. brute force could work but would get infeasible for any large sets obviously.

An efficient solution would be better though up to you if that is something your after, but like i said while that would still result in a solver it would need to be of a very specific nature.

But i could certainly envision this being doable with set theory and perhaps some graph theory depending on how you want to approach it.

Start simple and work up...

But to answer your question, yes its doable and it doesnt need to be brute forced with an ordinary solver.

Follow

@Absinthe a mathematical proof would produce a solver.. each rule infers the elimination of relationships, when only one path to the target exists (one relationship) then you know your rule set is valid.. just as you said.. but that is a solver, the one relationship that would remain would be the solution.

So thats my whole point, yes you can create a mathematical "proof".. but in doing so you would have created a special type of solver all the same.

@Absinthe keep in mind there are two dimensions to this... one dimension is the positional relationships.. one house being left of another, for example... thats one dimension... Then the other "dimension" (not spatial) is then the association to the various variables, like what pet they have, this dimension would likely look more like relations in a graph while the other dimension would look a bit different.

Its a fun problem im tempted to work on if i werent busy writing my mmorpg :)

@freemo well, sort of. But you still have clues that are still relative. For example

abc

def

ghi

A is left of b, c

A is also left of e, f

A is also left of h, i

So Bob is left of Charlie, but another clue is Bob is left of The person who smokes Pall Malls. Or the person who has a Zebra, and so on...

These have multi-dimentional inferences in that way. I get that. But I have to start my thought process somewhere. So reducing it to 3x3 and ABC is a good starting point, from which to build up a theory. No?

@Absinthe well your starting point is really 3x1 then.. your deealing just with the positional aspect of 3 variables.. which is fine, like you said you have to start somewhere.

So lets start with just 3x1 and work our way out... you need to start with a robust enough mathematical language to describe things right... Try to think in set theory terms, that means tuples and sets...

tuples, or adjacency lists might be useful representations..

if we start simple it might be as simple as saying "Bob is left of Alice" being represented as "p_bob < p_alice" at which point it all just become simple simultaneous equations right?

Seems to me this is the easy part of the problem if you model it that way.

@freemo let me think about it that way...

See if I can come up with something.

@freemo but maybe I can use it to have a reasonable language to start generating the fact templates.

@Absinthe the key here is finding the language to represent the problem yea.

@Absinthe Not sure why you asked me then :)

When my mind isnt deep in another problem ill be a little more clear headed to think about this. fun problem.

@freemo that's exactly why I asked you :)

La FΓ©e Verte@Absinthe@qoto.org@freemo Just thinking out loud. in a 3x3, a "left of" eliminates 1 position. 2 of them would infer that rightmost position as the one not referenced. Though there would be some other clue necessary to determine their specific location:

A is left of C

B is left of C

Infers C is rightmost. But doesn't solve AB vs BA

A is left of B

B is left of C

Infers C is rightmost

Infers A is leftmost

Infers B is in the middle

So 2 relative rules that commonly refer to a given element, infer that element, but not the relative ones. But 2 relative rules that do not share a common element will infer all 3 elements.

This is intuitive to me, but I don't know how to define that.. Or scale it.