Algorithmically generate a Zebra/Einstein puzzle

Here's a simple algorithm making use of your solver:

1. Generate a random puzzle instance.

2. Build a set C of all possible clues that pertain to this puzzle instance. (There are a finite and in fact quite small number of possible clues: for example if there are 5 houses, there are 5 possible clues of the form "Person A lives in house B", 8 possible clues of the form "Person A lives next to house B", and so on.)

3. Pick a random permutation c₁, c₂, ..., c_n of the clues in C.

4. Set i = 1.

5. If i > n, we are done. The set C of clues is minimal.

6. Let D = C − { c_i }. Run your solver on the set D of clues and count the number of possible solutions.

7. If there is exactly one solution, set C = D.

8. Set i = i + 1 and go back to step 5.

(You can speed this up by removing clues in batches rather than one at a time, but it makes the algorithm more complicated to describe.)

I'm not entirely confident in this solution but this is how I would approach it:

Starting from a random solution (i.e. green house holds polish that smokes LM, red house holds irish that smokes cloves etc). you may look at that solution as a graph of relations between statements. where every element (polish, red house etc) is connected to all other elements either by a "yes" edge or a "no edge" (in our case the polish is connected to the green house with a "yes" edge and to the cloves with a "no edge" (amongst many other edges, this initial graph is a full, directional graph)).

Now, if you randomly take away edges, until you are left with a minimal connected graph, you should have a graph representing a solvable puzzle. translate every yes edge to "the foo is/does bar" and every no edge to "the foo isn't/doesn't bar".

intuitively this sounds about right to me. but again, this is in no way a formal or recognized way to do this, and may be entirely wrong.