\documentclass{article}
\input{../6825-preamble}
\begin{document}
\psetnum{1a}
\date{2005/09/29}
\lstset{language=homework}
\lstset{frame=trbl}
\lstset{basicstyle=\footnotesize}
\stepcounter{equation}
\stepcounter{equation}
\stepcounter{equation}
\stepcounter{equation}
\stepcounter{equation}
\stepcounter{equation}
\begin{pset}
  \begin{problem}
    We begin by translating the original six axioms (1-6):
    \begin{lstlisting}
(Connects(W1, W2) ^ 
 Connects(W2, W3) ^
 Connects(W3, W4) ^
 Connects(W4, W1)) ^

(~Connects(W1, W3) ^ ~Connects(W1, W4) ^ ~Connects(W2, W4) ^
 ~Connects(W2, W1) ^ ~Connects(W3, W1) ^ ~Connects(W3, W2) ^
 ~Connects(W4, W2)  ^ ~Connects(W4, W3) ^ all w ~Connects(w, w)) ^

(all s 
  (Unconflicted(s) <-> 
    (all w all a1 all a2 (On(a1,w,s) ^ On(a2,w,s)
                           -> Equals(a1,a2))))) ^

(Unconflicted(S1)) ^

(all a all w2 
  (On(a,w2, S2) -> 
    (exists w1 
      (On(a,w1,S1) ^ Connects(w1,w2) ^ Allowed(a,w1,w2))))) ^

(all a1 all w1 all w2 
   Allowed(a1,w1,w2) <-> 
      (Equals(w1, w2) v ~(exists a2 On(a2,w2,S1))))                            
    \end{lstlisting}
  \end{problem}

  \begin{problem}
    Next, we express the following:
    \begin{itemize}
    \item Every athlete is always on some workout station:
      \begin{equation}
        \label{eq:always-on-some-station}
        \forall a \; \forall s \; \exists w \; \; On(a, w, s)
      \end{equation}
      \begin{lstlisting}
(all a all s exists w
   On(a, w, s))
      \end{lstlisting}
    \item No athlete is on two stations at the same time:
      \begin{equation}
        \label{eq:no-athlete-on-two-stations}
        \forall s \; \forall a \;  \forall w_1 \; \forall w_2 \; \; \proc{On}(a, w_1, s)
        \wedge \proc{On}(a, w_2, s) \implies w_1 = w_2
      \end{equation}
      \begin{lstlisting}
(all s all a all w1 all w2
  ((On(a, w1, s) ^ On(a, w2, s)) -> Equals(w1, w2)))        
      \end{lstlisting}
    \end{itemize}
  \end{problem}

  \begin{problem}
    The Java solver found the following satisfying
    assignment\footnote{To make satisfying assignments readable, I
      created a postprocessor that parses the assignment and displays
      only the instantiations that are true, in alphabetical
      order. False instantiations are not listed. All satisfying
      assignments shown in this document are in this format.}:

    \begin{lstlisting}
Allowed_A1_W1_W1
Allowed_A1_W1_W3
Allowed_A1_W2_W1
Allowed_A1_W2_W3
Allowed_A1_W3_W1
Allowed_A1_W3_W3
Allowed_A1_W4_W1
Allowed_A1_W4_W3
Allowed_A2_W1_W1
Allowed_A2_W1_W3
Allowed_A2_W2_W1
Allowed_A2_W2_W3
Allowed_A2_W3_W1
Allowed_A2_W3_W3
Allowed_A2_W4_W1
Allowed_A2_W4_W3
Connects_W1_W2
Connects_W2_W3
Connects_W3_W4
Connects_W4_W1
On_A1_W1_S2
On_A1_W4_S1
On_A2_W2_S1
On_A2_W3_S2
Unconflicted_S1
Unconflicted_S2      
    \end{lstlisting}

    In this satisfying assignment, $A_1$ is at station $W_4$
    initially, then moves to $W_1$ in $S_2$, and $A_2$ moves from
    $W_2$ to $W_3$. Both $S_1$ and $S_2$ are unconflicted, and the
    values for $\proc{Allowed}$ are as we expect: both $A_1$ and $A_2$
    are allowed to move anywhere except for $W_2$ and $W_4$, the
    original positions of the two athletes.
  \end{problem}

  \begin{problem}
    To show that there are no possible conflicts, we add an axiom
    saying that $S_2$ is conflicted:
    \begin{lstlisting}
(~(Unconflicted(S2)))
    \end{lstlisting}
    Then, performing a search for a satisfying assignment will tell us
    if there is a possible assignment such that $S_1$ is unconflicted
    and $S_2$ is conflicted: i.e. if it is possible to create a
    conflict when none existed before. The $\proc{SAT}$ solver failed
    to find a satisfying assignment, and it is complete, so we know
    that none existed. Therefore, there are no possible conflicts in
    this domain.

    It would not have been correct to use $\proc{WalkSAT}$ for this
    test, since $\proc{WalkSAT}$ is not a complete solver; it may fail
    to find a satisfying assignment even if one exists. So it cannot
    be used to prove that a set of axioms is never satisfiable.
  \end{problem}

  \begin{problem}
    We now allow athletes to stay on their current station. We begin
    by adding connections from each station to itself; this involves
    a $\forall w \;\; \proc{Connects}(w,w)$ clause to (1) and removing
    the opposite from (2):
    \begin{lstlisting}
(Connects(W1, W2) ^ 
 Connects(W2, W3) ^
 Connects(W3, W4) ^
 Connects(W4, W1) ^
 (all w Connects(w,w))) ^

(~Connects(W1, W3) ^ ~Connects(W1, W4) ^ ~Connects(W2, W4) ^
 ~Connects(W2, W1) ^ ~Connects(W3, W1) ^ ~Connects(W3, W2) ^
 ~Connects(W4, W2) ^ ~Connects(W4, W3)) ^      
    \end{lstlisting}

    But this does not suffice: the station is already occupied (by the
    same athlete), so our current definition of $\proc{Allowed}$ will
    not allow the athlete to stay in place. We must modify it to allow
    a move if the station is currently occupied by the same athlete
    trying to move there, in addition to if it is empty. This makes
    our axiom:
    \begin{equation}
      \label{eq:allowed-including-self-loops}
      \forall a_1 \; \forall w_1 \; \forall w_2 \; \proc{Allowed}(a_1,
        w_1, w_2) \iff (w_1 = w_2) \vee \left(\exists a_2 \;
          \proc{On}(a_2, w_2, S_1) \right)
    \end{equation}
    \begin{lstlisting}
(all a1 all w1 all w2 
   Allowed(a1,w1,w2) <-> 
      (Equals(w1, w2) v ~(exists a2 On(a2,w2,S1)))) ^      
    \end{lstlisting}

    To verify that this is correct, we add the following test axiom,
    which requires that some athlete stays in place:
    \begin{lstlisting}
      (exists a exists w (On(a, w, S1) ^ (On(a, w, S2))))
    \end{lstlisting}
    Running the solver gives a satisfying assignment, in which $A_1$
    stays in place in $W_2$, and $A_2$ moves from $W_3$ to $W_4$.

    The domain is still unconflicted. To verify this, we add the $\lnot
    \proc{Unconflicted}(S_2)$ axiom again, as before, and
    attempt to find a satisfying assignment. No satisfying assignment
    exists, so the domain is unconflicted.
  \end{problem}

  \begin{problem}
    Now we consider Layout 2. We replace (1) and (2) with the
    following:
    \begin{lstlisting}
(Connects(W1, W2) ^ 
 Connects(W1, W3) ^
 Connects(W2, W3) ^
 Connects(W3, W2) ^
 Connects(W2, W4) ^
 Connects(W3, W4) ^
 (all w Connects(w,w))) ^

(~Connects(W1, W4) ^ ~Connects(W2, W1) ^ ~Connects(W3, W1) ^
 ~Connects(W4, W2)  ^ ~Connects(W4, W3) ^ ~Connects(W4, W1))      
    \end{lstlisting}
    We test for conflictedness using the $\lnot
    \proc{Unconflicted}(S_2)$ axiom, which finds a conflicting
    assignment. The full set of axioms and the output of the solver
    follow:

    \begin{lstlisting}
(Connects(W1, W2) ^ 
 Connects(W1, W3) ^
 Connects(W2, W3) ^
 Connects(W3, W2) ^
 Connects(W2, W4) ^
 Connects(W3, W4) ^
 (all w Connects(w,w))) ^

(~Connects(W1, W4) ^ ~Connects(W2, W1) ^ ~Connects(W3, W1) ^
 ~Connects(W4, W2)  ^ ~Connects(W4, W3) ^ ~Connects(W4, W1)) ^

(all s 
  (Unconflicted(s) <-> 
    (all w all a1 all a2 (On(a1,w,s) ^ 
                          On(a2,w,s) -> Equals(a1,a2))))) ^

(Unconflicted(S1)) ^

(all a all w2 
  (On(a,w2, S2) -> 
    (exists w1 
      (On(a,w1,S1) ^ Connects(w1,w2) ^ Allowed(a,w1,w2))))) ^

(all a1 all w1 all w2 
   Allowed(a1,w1,w2) <-> 
      (Equals(w1, w2) v ~(exists a2 On(a2,w2,S1)))) ^

(all a all s exists w
   On(a, w, s)) ^

(all s all a all w1 all w2
  ((On(a, w1, s) ^ On(a, w2, s)) -> Equals(w1, w2))) ^

(~(Unconflicted(S2)))      
    \end{lstlisting}

    \begin{lstlisting}
Allowed_A2_W2_W1
Allowed_A2_W2_W2
Allowed_A2_W2_W4
Allowed_A2_W3_W1
Allowed_A2_W3_W3
Allowed_A2_W3_W4
Allowed_A2_W4_W1
Allowed_A2_W4_W4
Connects_W1_W1
Connects_W1_W2
Connects_W1_W3
Connects_W2_W2
Connects_W2_W3
Connects_W2_W4
Connects_W3_W2
Connects_W3_W3
Connects_W3_W4
Connects_W4_W4
On_A1_W2_S1
On_A1_W4_S2
On_A2_W3_S1
On_A2_W4_S2
Unconflicted_S1      
    \end{lstlisting}
    So we see that in $S_1$, $A_1$ and $A_2$ are on stations $W_2$ and
    $W_3$ respectively, but both try to move to $W_4$ in $S_2$,
    creating a conflict.
  \end{problem}

  \begin{problem}
    We change the definition of $\proc{Allowed}$ to avoid this
    situation. Now, an athlete can either stay in the same place, or
    move to a station that no other athlete can move to. (Note that
    this also forbids moving to a station that another athlete is
    already on, since the other athlete could stay in place.)
    \begin{multline}
      \label{eq:allowed-creating-deadlock}
      \forall a_1 \; \forall w_1 \; \forall w_2 \; \proc{Allowed}(a_1,
        w_1, w_2) \iff \\
        (w_1 = w_2) \vee \left(\exists a_2 \; \exists
          w_3 \;
          a_2 \neq a_1 \wedge \proc{On}(a_2, w_3, S_1) \wedge
          \proc{Connects}(w_3, w_2) \right)              
    \end{multline}
    \begin{lstlisting}
(all a1 all w1 all w2 
   Allowed(a1,w1,w2) <-> 
      (Equals(w1, w2) v
       ~(exists a2 exists w3
          (~Equals(a2, a1) ^ On(a2, w3, S1) ^ Connects(w3, w2)))))
    \end{lstlisting}

    To verify the sanity of this approach, we search for a satisfying
    assignment. We obtain the following:

    \begin{center}
      \begin{tabular}{|c|c|c|}
        \hline
        \textbf{Athlete} & $S_1$ & $S_2$ \\
        \hline
        $A_1$ & $W_1$ & $W_1$ \\
        $A_2$ & $W_3$ & $W_4$ \\
        \hline
      \end{tabular}
    \end{center}

    $A_1$ is unable to move from $W_1$ because it can only move to
    $W_2$ or $W_3$, and $A_2$ could either stay in $W_3$ or move to
    $W_2$.

    We can already see that this will cause deadlock. If we constrain
    $A_1$ to be on $W_2$ and $A_2$ to be on $W_3$ in $S_1$, neither
    can move:

    \begin{center}
      \begin{tabular}{|c|c|c|}
        \hline
        \textbf{Athlete} & $S_1$ & $S_2$ \\
        \hline
        $A_1$ & $W_2$ & $W_2$ \\
        $A_2$ & $W_3$ & $W_3$ \\
        \hline
      \end{tabular}
    \end{center}

    But the situation can never become conflicted. Adding the $\lnot
    \proc{Unconflicted}(S_2)$ axiom, the solver fails to find a
    satisfying assignment, meaning that the domain can never become
    conflicted.
  \end{problem}

  \begin{problem}
    We formalize the notion of deadlock as follows: $S_1$ is
    deadlocked if every athlete cannot move (and can only stay at the
    same station). That is, for every athlete, the only station
    $\proc{Connect}$ed to its current situation that it is
    $\proc{Allowed}$ to move to can only be its current station.

    In FOL:
    \begin{multline}
      \label{eq:deadlock}
      \proc{Deadlocked}(S_1) \iff \\
      \forall a \; \exists w_1 \; \proc{On}(a, w_1, S_1) \:\wedge\:
      \left[ \forall w_2 \; (\proc{Connects}(w_1, w_2) \,\wedge\,
        \proc{Allowed}(a, w_1, w_2)) \implies w_1 = w_2 \right]
    \end{multline}
    
    \begin{lstlisting}
(Deadlocked(S1) <->
  (all a exists w1
    (On(a, w1, S1) ^
     (all w2 ((Connects(w1, w2) ^
              Allowed(a, w1, w2)) -> Equals(w1, w2)))))) ^      
    \end{lstlisting}

    Using the \proc{Connects} definitions for Layout 1, and the
    definition of \proc{Allowed} given in
    \eqref{eq:allowed-creating-deadlock}, there can be no deadlock. We
    test this by adding the axiom $\proc{Deadlocked}(S_1)$ and
    searching for a satisfying assignment. The solver fails to find
    such an assignment, so deadlock is not possible.
  \end{problem}

  \begin{problem}
    Now we return to the \proc{Connects} definitions for Layout 2. We
    show that it is conflicted by requiring $\proc{Deadlocked}(S_1)$
    and finding a satisfying assignment. The solver finds the
    following deadlocked assignment:

    \begin{center}
      \begin{tabular}{|c|c|c|}
        \hline
        \textbf{Athlete} & $S_1$ & $S_2$ \\
        \hline
        $A_1$ & $W_2$ & $W_2$ \\
        $A_2$ & $W_3$ & $W_3$ \\
        \hline
      \end{tabular}
    \end{center}

    $A_1$ cannot move from $W_2$ because the only adjacent stations
    are $W_3$, which is occupied by $A_2$, and $W_4$, which $A_2$
    could also move to. $A_2$ cannot move from $W_3$ for an equivalent
    reason.

    The assignment follows:
    \begin{lstlisting}
Allowed_A2_W2_W1
Allowed_A2_W2_W2
Allowed_A2_W3_W1
Allowed_A2_W3_W3
Allowed_A2_W4_W1
Allowed_A2_W4_W4
Connects_W1_W1
Connects_W1_W2
Connects_W1_W3
Connects_W2_W2
Connects_W2_W3
Connects_W2_W4
Connects_W3_W2
Connects_W3_W3
Connects_W3_W4
Connects_W4_W4
Deadlocked_S1
On_A1_W2_S1
On_A1_W2_S2
On_A2_W3_S1
On_A2_W3_S2
Unconflicted_S1
Unconflicted_S2      
    \end{lstlisting}
  \end{problem}

  \begin{problem}
    We break symmetry by introducing a notion of \emph{priority}
    between athletes. An athlete is now allowed to move to a new
    station if there exists no other athlete \emph{of lower priority}
    that could move there.

    We arbitrarily assign priorities, with $A_1$ having higher
    priority than $A_2$. Note that this axiom defines a relation
    between individual athletes, but could be easily extended if there
    were more than two athletes.

    \begin{lstlisting}
      (Priority(A1, A2) ^ ~Priority(A2, A1) ^ (all a ~Priority(a, a))) ^
    \end{lstlisting}

    We define a utility predicate \proc{Blocked}. An athlete $a$ is
    blocked from moving to a station $w$ if there exists some other
    athlete with higher priority on a station that connects to $w$.

    \begin{lstlisting}
(all a1 all w1
  Blocked(a1, w1) <->
   (exists a2 exists w2
          (~Equals(a2, a1) ^ Priority(a2, a1) ^
           On(a2, w2, S1) ^ Connects(w2, w1)))) ^
    \end{lstlisting}

    Now we redefine \proc{Allowed}. An athlete $a$ is now allowed to
    move from $w_1$ to $w_2$ if it is not blocked from moving to
    $w_2$. Moreover, it is not allowed to stay at the same station
    unless every adjacent station is blocked. This keeps the athletes
    moving if possible.
    \begin{lstlisting} 
(all a1 all w1 all w2 
   Allowed(a1,w1,w2) <-> 
      ((Equals(w1, w2)  ^ (all w3 (Connects(w1, w3) -> Blocked(a1, w3)))) v
       (~Equals(w1, w2) ^ ~(Blocked(a1, w2))))) ^
    \end{lstlisting}

    The result is that, if we constrain
    $A_1$ to begin on $W_2$ and $A_2$ to begin on $W_3$ in $S_1$,
    $A_1$ is able to move to $W_4$.

    \begin{center}
      \begin{tabular}{|c|c|c|}
        \hline
        \textbf{Athlete} & $S_1$ & $S_2$ \\
        \hline
        $A_1$ & $W_2$ & $W_4$ \\
        $A_2$ & $W_3$ & $W_3$ \\
        \hline
      \end{tabular}
    \end{center}

    Furthermore, by adding a $\proc{Deadlocked}(S_1)$ axiom, we can
    test whether deadlock is ever possible. There are no satisfying
    assignments, so deadlock is avoided.
  \end{problem}

  \begin{problem}
    This implication should not be a biconditional. If it were, then
    for all $w_2$, if there exists a $w_1$ such that $a$ is on $w_1$
    in $S_1$,
    $w_1$ connects to $w_2$, and $a$ is allowed to move from $w_1$ to
    $w_2$, then $a$ would be on $w_2$ in $S_1$. This is certainly true
    for \emph{some} $w_2$, but not for \emph{all} $w_2$. It's possible
    to have multiple choices for where $a$ would move, and the
    biconditional would mean that $a$ would then make all possible
    moves, which wouldn't make sense (and would be prevented by the
    axiom that asserts that each athlete is always on one station.)
  \end{problem}

  \begin{problem}
    A better definition of liveness that incorporates fairness might
    require that every athlete gets to move on \emph{some} step, i.e.
    \begin{equation}
      \label{eq:liveness-fairness}
      \forall a \; \exists s \; \exists w_1 \; \exists w_2 \;\;
      \proc{On}(a,w_1,s) \: \wedge \: \proc{Connects}(w_1, w_2) \:
      \wedge\: \proc{Allowed}(a, w_1, w_2)
    \end{equation}

    But we could not try to prove or disprove this condition using the
    finite-domain method. This would require us to consider many
    states, since we are only ensuring that every athlete gets to move
    on some step. Our finite universe with only two states would not
    suffice, since it only considers one starting position. In fact,
    any finite number $n$ of states would not suffice, since there
    might be some athlete that does not get to move until state
    $n+1$. So we would need to use some other method for first-order
    logic theorem proving.
  \end{problem}

  \vspace{1in} Just for completeness, note that the full set of axioms
  used in this project are available from
  \url{http://drkp.net/svn/classes/6.825/proj1/}.
\end{pset}

\end{document}

