Difficulty: Easy · Puzzle 2 of 6 · Topic: Constraint Solving Order Puzzles
For this class, what is P(x==0)? Why is the solver not 'choosing x first, then computing y' procedurally?
class sum_pair;
rand int unsigned x;
rand int unsigned y;
constraint c_dom {
x inside {[0:10]};
y inside {[0:10]};
}
constraint c_eq { x + y == 10; }
endclassEach x value determines exactly one y value in the domain.
1) For each x in 0..10, y is fixed to 10-x and remains in 0..10.
2) That gives exactly 11 legal tuples.
3) Exactly one tuple has x==0, so P(x==0)=1/11.
4) The equality is bidirectional relation solving, not assignment sequencing.Answer: P(x==0)=1/11 (~9.09%), and x/y are solved as a joint relation rather than left-to-right execution.
Checked by running a model of the rule in a Python model. Exact enumeration of the constraint set per the LRM (the LRM defines the distribution; simulator solvers need not be uniform). x + y == 10 is a relation: 11 tuples, symmetric in x and y, and solve x before y changes nothing.
Saying 'y depends on x only' is wrong here: x + y == 10 pins x just as much as it pins y (y==10 forces x==0). The 11 tuples are symmetric, so x and y are each uniform over 0..10 and either could be 'decided first'.
What is P(x is even), and does adding solve x before y change the legal set? Model answer: x even means x in {0,2,4,6,8,10}, 6 of the 11 tuples, so P=6/11. Adding `solve x before y` does not change the legal set, and here it does not change the probabilities either: each x has exactly one y, so choosing x uniformly over its 11 feasible values gives the same 1/11 per tuple.
There are eleven legal pairs, one for each x from zero to ten, so the probability that x is zero is one in eleven. The solver treats x plus y equals ten as a joint relation, not as pick x and then compute y, so x and y are each uniform over zero to ten. The trap is saying y depends only on x; y equal to ten forces x to zero just as much. Next I would confirm that solve x before y changes nothing here, since each x has exactly one y.