Alloy

Stumbling on Jim Propp's self-referential aptitude test reminded me that I should really get around to learning Alloy (a "simple structural modeling language based on first-order logic", according to its homepage). The examples in the Alloy tutorial work well enough, but I wanted to know whether will also solve problems not chosen by the author ;-)

My final solution came out surprisingly neatly for a first attempt, following the format of the quiz closely, although it took much experimenting to get the syntax exactly right. The only bit I'm unhappy about is the helper predicates for question 12, as I couldn't find an easy way to test for primes, etc. Any Alloy experts out there want to show me a quicker way?

In case anyone is wondering what is impressive about Alloy, consider that the program below only says how to check that a given set of answers is correct. There are five possible answers to each question, all inter-related, giving 5 ** 20 possible answer sets. There is only one correct solution, so a naive approach would have to check an average of (5**20)/2 states before finding the answer. At n processor cycles to check one state, that's (1/2)n.(5**20) cycles, or about 50,000.n seconds on a 1GHz machine. If n is 100 (probably optimistic), that's an average of 55 days to find the solution. Alloy takes just a few seconds.

Now I just need to find a real use for it.

Code

For reference, here's my code:

module thomas/reftest

open util/ordering[Question]

// Every question has one answer
sig Question {
  a : one Answer
}

// Each answer can be used for any number of questions
abstract sig Answer {
  qs : set Question
}

// The five possible answers to each question
one sig A, B, C, D, E extends Answer {
}

// These are inverse relationships (if X is the
// answer to Y, then Y is answered by X)
fact {
  qs = ~a
}

// The next question with the same answer as qa is qb
pred next_with_same(qa, qb : Question) {
  qa.a = qb.a
  no q : Question {
    q.a = qa.a
    q in nexts(qa) - nexts(qb) - qb
  }
}

pred odd(e : set univ) {
  #e = 1 ||
  #e = 3 ||
  #e = 5 ||
  #e = 7 ||
  #e = 9 ||
  #e = 11 ||
  #e = 13 ||
  #e = 15 ||
  #e = 17 ||
  #e = 19
}

pred perfect_square(e : set univ) {
  #e = 0 ||
  #e = 1 ||
  #e = 4 ||
  #e = 9 ||
  #e = 16
}

pred prime(e : set univ) {
  #e = 2 ||
  #e = 3 ||
  #e = 5 ||
  #e = 7 ||
  #e = 11 ||
  #e = 13 ||
  #e = 17 ||
  #e = 19
}

pred divisible_by_5(e : set univ) {
  #e = 0 ||
  #e = 5 ||
  #e = 10 ||
  #e = 15 ||
  #e = 20
}

// Passing all the questions as arguments gives them
// sensible labels in the final graph
pred solve(
	q1, q2, q3, q4, q5,
	q6, q7, q8, q9, q10,
	q11, q12, q13, q14, q15,
	q16, q17, q18, q19, q20
	: Question) {

    // Ensure that our argument numbering matches the actual ordering

    q1 = first()
    q2 = next(q1)
    q3 = next(q2)
    q4 = next(q3)
    q5 = next(q4)
    q6 = next(q5)
    q7 = next(q6)
    q8 = next(q7)
    q9 = next(q8)
    q10 = next(q9)
    q11 = next(q10)
    q12 = next(q11)
    q13 = next(q12)
    q14 = next(q13)
    q15 = next(q14)
    q16 = next(q15)
    q17 = next(q16)
    q18 = next(q17)
    q19 = next(q18)
    q20 = next(q19)

    // rules for each question follow (consult quiz for English explanation)

    q1.a = A => min(B.qs) = q1
    q1.a = B => min(B.qs) = q2
    q1.a = C => min(B.qs) = q3
    q1.a = D => min(B.qs) = q4
    q1.a = E => min(B.qs) = q5

    one s1 : Question {
	    s1.a = next(s1).a
    }

    q2.a = A => q6.a = q7.a
    q2.a = B => q7.a = q8.a
    q2.a = C => q8.a = q9.a
    q2.a = D => q9.a = q10.a
    q2.a = E => q10.a = q11.a

    q3.a = A => #(E.qs) = 0
    q3.a = B => #(E.qs) = 1
    q3.a = C => #(E.qs) = 2
    q3.a = D => #(E.qs) = 3
    q3.a = E => #(E.qs) = 4

    q4.a = A => #(A.qs) = 4
    q4.a = B => #(A.qs) = 5
    q4.a = C => #(A.qs) = 6
    q4.a = D => #(A.qs) = 7
    q4.a = E => #(A.qs) = 8

    q5.a = A => q5.a = q1.a
    q5.a = B => q5.a = q2.a
    q5.a = C => q5.a = q3.a
    q5.a = D => q5.a = q4.a
    q5.a = E => q5.a = q5.a

    q6.a = A => q17.a = C
    q6.a = B => q17.a = D
    q6.a = C => q17.a = E
    q6.a = D => q17.a in (A + B)
    q6.a != E

    q7.a = A => q8.a = E
    q7.a = B => q8.a = E
    q7.a = C => q8.a in (A + E)
    q7.a = D => q8.a in (C + E)
    q7.a = E => q8.a = E

    q8.a = A => #(A.qs + E.qs) = 4
    q8.a = B => #(A.qs + E.qs) = 5
    q8.a = C => #(A.qs + E.qs) = 6
    q8.a = D => #(A.qs + E.qs) = 7
    q8.a = E => #(A.qs + E.qs) = 8

    q9.a = A => next_with_same(q9, q10)
    q9.a = B => next_with_same(q9, q11)
    q9.a = C => next_with_same(q9, q12)
    q9.a = D => next_with_same(q9, q13)
    q9.a = E => next_with_same(q9, q14)

    q10.a = A => q16.a = D
    q10.a = B => q16.a = A
    q10.a = C => q16.a = E
    q10.a = D => q16.a = B
    q10.a = E => q16.a = C

    q11.a = A => #(B.qs - nexts(q10)) = 0
    q11.a = B => #(B.qs - nexts(q10)) = 1
    q11.a = C => #(B.qs - nexts(q10)) = 2
    q11.a = D => #(B.qs - nexts(q10)) = 3
    q11.a = E => #(B.qs - nexts(q10)) = 4

    let consonant_answers = B.qs + C.qs + D.qs {
      q12.a = A => not odd(consonant_answers)
      q12.a = B => odd(consonant_answers)
      q12.a = C => perfect_square(consonant_answers)
      q12.a = D => prime(consonant_answers)
      q12.a = E => divisible_by_5(consonant_answers)
    }

    one q : (q1 + q3 + q5 + q7 + q9 +
	     q11 + q13 + q15 + q17 + q19) | q.a = A

    q13.a = A => q9.a = A
    q13.a = B => q11.a = A
    q13.a = C => q13.a = A
    q13.a = D => q15.a = A
    q13.a = E => q17.a = A

    q14.a = A => #(D.qs) = 6
    q14.a = B => #(D.qs) = 7
    q14.a = C => #(D.qs) = 8
    q14.a = D => #(D.qs) = 9
    q14.a = E => #(D.qs) = 10

    q15.a = q12.a

    q16.a = A => q10.a = D
    q16.a = B => q10.a = C
    q16.a = C => q10.a = B
    q16.a = D => q10.a = A
    q16.a = E => q10.a = E

    q17.a = A => q6.a = C
    q17.a = B => q6.a = D
    q17.a = C => q6.a = E
    q17.a = D => q6.a in (A + B)
    q17.a != E

    q18.a = A => #(A.qs) = #(B.qs)
    q18.a = B => #(A.qs) = #(C.qs)
    q18.a = C => #(A.qs) = #(D.qs)
    q18.a = D => #(A.qs) = #(E.qs)
    q18.a = E => {
      #(A.qs) != #(B.qs)
      #(A.qs) != #(C.qs)
      #(A.qs) != #(D.qs)
      #(A.qs) != #(E.qs)
    }

    q20.a = E
}

run solve for 20 Question