 Home More Samples
```/////////////////////////////////////////////////////////////////////////////////////////
//
// Title: Pro and Con
// Author: Monica Tenniel
// Publication: Dell Logic Puzzles
// Issue: April, 1998
// Page: 12
// Stars: 2
//
// At the last meeting of the local city council, each member (Mr. Akerman, Ms. Baird,
// Mr. Chatham, Ms. Duval, and Mr. Etting) had to vote on five motions, number 1 to 5
// in the clues below. Can you discover how each one voted on each motion?
//
// Note: a motion may have received zero or one yes vote, even though in real
// life it's unlikely that both the maker and seconder of the motion would
// change their minds before the motion came up for a vote. Each member voted
// either yes or no on each motion; no one abstained from voting on any motion.
//
// Voting Chart
//
//                1     2     3     4     5
// Mr. Akerman
// Ms. Baird
// Mr. Chatham
// Ms. Duval
// Mr. Etting
//
// 1. Each motion got a different number of yes votes.
// 2. In all, the five motions got three more yes votes than no votes.
// 3. No two council members voted the same way on all five motions.
// 4. The two women disagreed in their voting more often than they agreed.
// 5. Mr. Chatham never made two yes votes on consecutive motions.
// 6. Mr. Akerman and Ms. Baird both voted in favor of motion 4.
// 7. Motion 1 received two more yes votes than motion 2 did.
// 8. Motion 3 received twice as many yes votes as motion 4 did.
//
// Determine: fill in the chart (Yes/No) for each motion
//
/////////////////////////////////////////////////////////////////////////////////////////
//
// Query:
//          all ProAndCon(x)
//
/////////////////////////////////////////////////////////////////////////////////////////
//
// Result:
//
// x = [ {Akerman} [ {M1} 1, {M2} 1, {M3} 1, {M4} 1, {M5} 0],
//       {Baird}   [ {M1} 1, {M2} 0, {M3} 1, {M4} 1, {M5} 0],
//       {Chatham} [ {M1} 1, {M2} 0, {M3} 1, {M4} 0, {M5} 0],
//       {Duval}   [ {M1} 1, {M2} 1, {M3} 0, {M4} 0, {M5} 0],
//       {Etting}  [ {M1} 1, {M2} 1, {M3} 1, {M4} 0, {M5} 0]]
//
/////////////////////////////////////////////////////////////////////////////////////////
//
// Notes:
//      We use the number 1 for a "yes" vote, 0 for a "no" vote.
//      Although the number corresponding to a vote can only have one of these
//      two values, it was declared as "L" (large integer) as opposed to
//      "I" (integer). The constraints as specified in the code below are more
//      efficiently evaluated this way. In other words: in spite of using "L" instead
//      of "I" the puzzle is solved faster.
//
/////////////////////////////////////////////////////////////////////////////////////////

Name = Akerman | Baird | Chatham | Duval | Etting
Motion = M1 | M2 | M3 | M4 | M5
Motions = Name->>Motion->L[0..1]    {injection: Each member voted differently}

pred ProAndCon(m::Motions) iff
// 1. Each motion got a different number of yes votes.

sums::Motion->>L[0..5] & {each different}

sums(M1) = m(Akerman,M1) + m(Baird,M1) + m(Chatham,M1) + m(Duval,M1) + m(Etting,M1) &
sums(M2) = m(Akerman,M2) + m(Baird,M2) + m(Chatham,M2) + m(Duval,M2) + m(Etting,M2) &
sums(M3) = m(Akerman,M3) + m(Baird,M3) + m(Chatham,M3) + m(Duval,M3) + m(Etting,M3) &
sums(M4) = m(Akerman,M4) + m(Baird,M4) + m(Chatham,M4) + m(Duval,M4) + m(Etting,M4) &
sums(M5) = m(Akerman,M5) + m(Baird,M5) + m(Chatham,M5) + m(Duval,M5) + m(Etting,M5) &

// 2. In all, the five motions got three more yes votes than no votes.
yes_votes + no_votes = 25 & {25 votes total: 5 members * 5 votes each}
sums(M1) + sums(M2) + sums(M3) + sums(M4) + sums(M5) = yes_votes &

// 3. No two council members voted the same way on all five motions.
{this is guaranteed by the type declaration of "Motions"}

// 4. The two women disagreed in their voting more often than they agreed.
DisagreedMore(m(Baird),m(Duval)) &

// 5. Mr. Chatham never made two yes votes on consecutive motions.
NoTwoConsecutiveYes(m(Chatham)) &

// 6. Mr. Akerman and Ms. Baird both voted in favor of motion 4.
m(Akerman,M4) = 1 & m(Baird,M4) = 1 &

// 7. Motion 1 received two more yes votes than motion 2 did.
sums(M1) = sums(M2) + 2 &

// 8. Motion 3 received twice as many yes votes as motion 4 did.
sums(M3) = 2*sums(M4)

local pred DisagreedMore(m1::Motion->L[0..1],m2::Motion->L[0..1]) iff
(diff1 = 1 & m1(M1) <> m2(M1) | diff1 = 0) &
(diff2 = 1 & m1(M2) <> m2(M2) | diff2 = 0) &
(diff3 = 1 & m1(M3) <> m2(M3) | diff3 = 0) &
(diff4 = 1 & m1(M4) <> m2(M4) | diff4 = 0) &
(diff5 = 1 & m1(M5) <> m2(M5) | diff5 = 0) &
diff1 + diff2 + diff3 + diff4 + diff5 >= 3

local pred NoTwoConsecutiveYes(m::Motion->L[0..1]) iff
m(M1) + m(M2) < 2 &
m(M2) + m(M3) < 2 &
m(M3) + m(M4) < 2 &
m(M4) + m(M5) < 2

```