The Zebra Puzzle is a classic logic puzzle, first published by Life International in 1962. Older versions of it exist and it is also sometimes called Einstein's puzzle. According to "Of Camels and Committees" by Tom Fitzpatrick and Dave Rich, it was used in the early days of constrained random verification (CRV) to show off EDA tools at marketing events.
“^” is not officially a logical operator, it’s a binary bitwise operator. I’ve tried it out just now and it works in constraints, but what we have to be careful with here is the operator precedence. “^” has a higher precedence than either “&&” or “||”.
As an example, let’s assume A, B and C are expressions and that we have the following constraint: A && B || A && C. This is equivalent to (A && B) || (A && C).
If however we want to swap out the “||” for “^” and we rewrite the constraint as A && B ^ A && C, then this will be equivalent to A && (B ^ A) && C, due to the higher precedence of the “^” operator. This would have to be rewritten as: (A && B) ^ (A && C) to force the order of operations that we want.
Nice example. I did the similar exercise, using SystemVerilog, but in order to have it solved by formal verification (model checking).
The code is more concise since we don’t care about the pitfalls you mentioned.
A commercial model checker is able to find the solution immediately, AND TO PROVE IT IS UNIQUE.
I think this shows the superiority of formal methods.
What’s the running time for the constrained random approach? How would it extend if the number of houses gets bigger? Probably very badly.
Each constraint should ideally just reduce the state space every time. From what I know, constraint solvers are also at their core built from SAT solvers, the same as formal tools. I wouldn’t think that a constraint solver gets less mileage than a formal tool if the number of houses gets bigger. The reason why I could guess a formal tool would be faster in this respect is because it has a better optimized prover (as this is the main thing it does), whereas for a logic simulator there are for sure other things that also need to be optimized (the simulation engine for example) and they won’t invest so much time in developing their constraint solver (as long as it’s not incredibly slow).
Take what I’ said with a grain of salt, as I don’t really know the internal implementations of EDA tools.
HI VERY NICE EXPLONATION. BUT THE SAME CODE, I CODED IN VCS. I RANDOMIZE 20 TIMES AND PRINTING EVERY HOUSE RESULT. IDEALLY, WE SHOULD GET THE SAME RESULT. BUT IT IS GIVING DIFFERENT RESULTS, IN WHICH CORRECT RESULT IS ONE OR TWO INSTANCES. WHAT WOULD BE THE PROBLEM. Can you help me DAVE?