From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 24 Dec 2015 11:57:18 +0000 (+0100)
Subject: pretty solution'
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=38f217985470b538cc305c130413e724ac7f6e00;p=ar1516.git

pretty solution'
---

diff --git a/a2/4.tex b/a2/4.tex
index 9694310..9eb06c0 100644
--- a/a2/4.tex
+++ b/a2/4.tex
@@ -77,11 +77,7 @@ To represent each position, as in Listing~\ref{lst:coord}, we assign per
 iteration $i$ for $i\in I$ where $I=\{0..32\}$ a variable $i_ix_xy_y$ per
 position where $(x,y)\in P$ where $P=\{(x,y) | (x,y)\text{ position on the
 board}\}$. So for example for the topmost row we have for $i=0$ the variables
-$\{i_0x_2y_0, i_0x_2y_1, i_0x_3y_0, i_0x_3y_1, i_0x_4y_0, i_0x_4y_1\}$.  In
-this way we can describe the start position, where $i=0$, by the following
-formula meaning that all the positions are occupied except for the middle
-position with coordinate $(3,3)$:
-$$\neg i_0x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}i_0x_xy_y$$
+$\{i_0x_2y_0, i_0x_2y_1, i_0x_3y_0, i_0x_3y_1, i_0x_4y_0, i_0x_4y_1\}$. 
 
 To iterate over all moves we have to distinguish start and end positions from
 the middle position. All positions from $P$ are legal start or end positions
@@ -90,12 +86,17 @@ all positions in $P$ except for the corners are legal middle positions and
 therefore we define $P'$ that only contains legal middle positions and
 therefore $P'=P\setminus\{(2,0), (4,0), (0,2), (0,4), (6,2), (6,4), (2,6),
 (4,6)\}$
-All iterations following that can be described as the following formula:
 
 \begin{align}
-\bigwedge^{I}_{i=1}
+	\neg i_0x_3y_3\wedge\bigwedge_{(x,y)\in
+P\setminus\{(3,3)\}}\left(i_0x_xy_y\right)\wedge\\
+	\bigwedge^{I}_{i=1}
 	\bigvee_{(sx, sy)\in P}\bigvee_{(mx, my)\in P'}
-	\bigvee_{(ex, ey)\in P}\Bigl(
+	\bigvee_{(ex, ey)\in P}\Bigl( 
+	& \bigl((sy=my\wedge my=ey\wedge sx=mx+1\wedge mx=ex+1)\vee\\
+        & \quad(sy=my\wedge my=ey\wedge sx=mx-1\wedge mx=ex-1)\vee\\
+        & \quad(sx=mx\wedge mx=ex\wedge sy=my+1\wedge my=ey+1)\vee\\
+        & \quad(sx=mx\wedge mx=ex\wedge sy=my-1\wedge my=ey-1)\bigr)\wedge\\
 	& i_{i-1}x_{sx}y_{sy}\wedge
 		i_{i-1}x_{mx}y_{my}\wedge
 		\neg i_{i-1}x_{ex}y_{ey}\wedge\\
@@ -103,12 +104,9 @@ All iterations following that can be described as the following formula:
 		\neg i_{i}x_{mx}y_{my}\wedge
 		i_{i}x_{ex}y_{ey}\wedge\\
 	& \bigwedge_{(ox,oy)\in P\setminus\{(ex,ey),(mx,my),(sx,sy)\}}\left(
-	i_ix_{ox}y_{oy}=i_{i-1}x_{ox}y_{oy}\right)\Bigr)
+	i_ix_{ox}y_{oy}=i_{i-1}x_{ox}y_{oy}\right)\Bigr)\wedge\\
+	i_{31}x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}\neg i_{31}x_xy_y
 \end{align}
 
-To get a trace for a winning game we negate the final condition and add it to
-the formula:
-$$i_{31}x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}\neg i_{31}x_xy_y$$
-
 \lstinputlisting[caption={Solution for peg solitaire},label={lst:sol}]
 	{./src/4/a4.tex}