Example Problem/Solution for HW #2
Problem
This problem is based on an ETS practice problem (see www.ets.org).
There are six professors -- Anderson, Boriello, Chambers, Diorio,
Eggers, and Fakeprof -- playing faculty one-on-one ping-pong. Each
prof plays each other prof once and only once, and each prof plays
exactly one game per week over the course of the five week regular
season. The schedule follows these constraints:
- Anderson must play Diorio first and Fakeprof second.
- Boriello must play Eggers first and Chambers third.
- Chambers must play Fakeprof first.
Which of these profs must play Boriello second?
- Anderson
- Chambers
- Diorio
- Eggers
- Fakeprof
Solution
First-order Logic
Let each prof be represented by the first letter of his, her, or its
name. Let the relation plays(x, y, z) mean that Professor
x (Xavier?) plays Professor y in week z.
Now, I axiomatize the system with the following rules:
- Forall x,z: not plays(x,x,z)
- No prof plays himself, herself, or itself.
- Forall x,y,z: plays(x,y,z) -> plays(y,x,z)
- If x plays y in week z, then y also plays x in week z.
- Forall w,x,y,z: (not eq(y,w)) -> (plays(x,y,z) -> (not plays(x,w,z)))
- Each prof plays at most once per week.
- Forall x,z: there exists a y such that: plays(x,y,z)
- Each prof plays at least once per week.
- Forall x,y: there exists a z such that: (not eq(x,y)) -> plays(x,y,z)
- Each prof plays each other prof at least once.
- Forall w,x,y,z: (not eq(z,w)) -> (plays(x,y,z) -> (not plays(x,y,w)))
- Each prof plays each other prof at most once.
To this I add statements describing the given information:
- plays(A,D,1)
- plays(A,F,2)
- plays(B,E,1)
- plays(B,C,3)
- plays(C,F,1)
Note that I don't have to fill this out to say things like
plays(D,A,1). My axioms will do this for me!
Finally, I need to determine who must play Boriello second. I can do
this a couple different ways. I can insert (not plays(?,B,2)) for each
prof and see which one makes the KB inconsistent, or I can find a
solution to the KB and see which prof plays Boriello in that solution
(since the prof must play Boriello, she'll play
Boriello in every solution).
I have two predicates: plays and eq. Technically, there are actually
two eq predicates: one eq over weeks and one eq over profs. I will
allow the eq predicates to be implicit (so this is actually FOL with
equality), but in propositional form, I can make these predicates
explicit just by spewing out things like:
- eq(A,A)
- eq(B,B)
- eq(C,C)
- eq(D,D)
- eq(E,E)
- eq(F,F)
- (not eq(A,B))
- (not eq(A,C))
- ...
Translation to CNF
You may use the
translator we provide in order to translate from FOL to CNF (note:
you do not have to translate first order logic to general
propositional and then to CNF form; you can go straight to CNF).
You should follow the instructions and example provided in fol.lsp
and sat.lsp
to perform the translation and solution of the problem.