From: Mart Lubbers Date: Sat, 2 Jan 2016 18:51:38 +0000 (+0100) Subject: big update, better formalization for pegsol X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=08b8ab611e95ff12bef42f9863a76b75b3ecab51;p=ar1516.git big update, better formalization for pegsol --- diff --git a/a2/1.tex b/a2/1.tex index 67a214c..11692f6 100644 --- a/a2/1.tex +++ b/a2/1.tex @@ -17,51 +17,90 @@ for $i\in I$ where $I=\{0\ldots\}$. For every iteration $i$ we make variables $a_i, b_i, c_i, t_i, l_i, d_i$ respectively for the capacity of city $A$, city $B$, city $C$, the truck, the trucks location and a help variable to record how much food is dumped in the city. The distance between two cities is -described with the function $dist(x, y)$. For all cities except $S$ a variable -is defined that states the maximum capacity. -$$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200$$ +described with the function $dist(x, y)$. For all cities except $S$ and the +truck a variable is defined that states the maximum capacity. We express all +the constant values in the formula called $const$. +$$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200\wedge t_{\max}=300$$ + Iteration $0$ depicts the initial state and can be described with a simple -conjuction: +conjunction called $initial$. $$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$ -After that all iterations can be formalized as -$$\begin{array}{lrl} - \bigwedge_{i\in I} \Bigg( - % Bent in S - & \Bigg[ & l_i=S\wedge d_i=0\wedge t_i=300\wedge\\ - & & \bigvee_{k\in\{A,B\}} - \bigg(l_{i-1}=k\wedge - \bigwedge_{s\in\{A,B,C\}} - s_i=s_{i-1}-dist(S, k)\bigg)\Bigg]\vee\\ - % Bent in A,B,C - & \bigvee_{k\in\{a,b,c\}}\Bigg[ & l_i=k\wedge\\ - & & d_i>0\wedge d_i0\wedge +d_i\leq t_{\max}\wedge +t_i\geq\wedge +t_i\leq t_{\max}\wedge +\bigwedge_{k\in\{A,B,C\}}k_i>0$$ -\begin{enumerate} - \item This part of the formula describes what happens if the truck is in - $S$. This is a special case of the generalized case dsecribed in $2$ - and $3$. The truck always gets a refill in $S$ and no food is dumped. - The truck could either have come from $A$ or $B$ and thus the food - stocks of $A,B$ and $C$ will drop accordingly. - \item -\end{enumerate} +We reason about the new iteration $i$ from the things we know about iteration +$i-1$. The crucial part is the location we were in iteration $i-1$ and we make +a disjunction over all possible cities and describe the result in the following +formula called $trans$. We introduce a function $conn(s)$ that returns the set +of all cities connected to city $s$. $(2)$ deals with the fact that the truck +can not dump any food in city $S$ and constraints the amount of food dumped in +the city. $(3)$ deals with the fact that the dumped food is added to the +current stock of the city. Subformula $(4)$ deals with the fact that if the +truck is in $S$ it is replenished and otherwise the dumped load is subtracted +from the trucks load. Finally $(5)$ deals with the other cities which will have +their stock decremented with the distance traveled. + +\begin{align} + \bigvee_{k\in\{S\}\cup V} + l_{i-1}=k\wedge + \bigvee_{k'\in conn(k)} & l_i=k'\wedge\\ + & (k'=S\wedge d_i=0)\vee(d_i\leq dist(k,k')+k'_{\max}-k'_{i-1}\wedge\\ + & (k'\neq S\rightarrow k_i=k_i-dist(k,k')+d_i))\wedge\\ + & (k'=S\wedge t_i=t_{\max})\vee t_i=t_{i-1}-d_i\wedge\\ + & \bigwedge_{k''\in V\setminus\{k\}} + k''_i=k''_{i-1}-dist(k,k') +\end{align} + +We tie all this together in one big formula that is as follows: +$$const\wedge initial\wedge +\bigwedge_{i\in I}\left(constraints\wedge trans\right)$$ \begin{enumerate}[a.] \item \emph{Show that it is impossible to deliver food packages in such a way that each of the villages consumes one food package per time unit forever.} + \item \emph{Show that this is possible if the capacity of the truck is increased to 320 food packages. (Note that a finite graph contains an infinite path starting in a node $v$ if and only if there is a path from $v$ to a node $w$ for which there is a non-empty path from $w$ to itself.)} + To show this we need to prove that there is a state in the statespace + that is exactly the same as some previous state. To do this we add the + following formula to the conjunction. + $$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left( + t_i=t_j\wedge l_i=l_j\wedge\bigwedge_{k\in V}k_i=k_j\right) + $$ + + When we incrementally increase the number of iterations we see that + when we have more then $8$ iterations we encounter a cycle. This is + shown in the following table where iteration $2$ and iteration $9$ are + equal. + \begin{table}[H] + \centering + \begin{tabular}{ccccccc} + \toprule + $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\ + \midrule + $0$ & $40$ & $30$ & $145$ & $320$ & $0$ & $0$\\ + $1$ & $19$ & $22$ & $124$ & $307$ & $2$ & $9$\\ + $2$ & $96$ & $5$ & $107$ & $213$ & $1$ & $98$\\ + $3$ & $79$ & $119$ & $90$ & $82$ & $2$ & $133$\\ + $4$ & $58$ & $98$ & $69$ & $320$ & $0$ & $0$\\ + $5$ & $108$ & $69$ & $40$ & $241$ & $1$ & $79$\\ + $6$ & $76$ & $37$ & $194$ & $55$ & $3$ & $186$\\ + $7$ & $39$ & $55$ & $157$ & $0$ & $2$ & $53$\\ + $8$ & $18$ & $34$ & $136$ & $320$ & $0$ & $0$\\ + $9$ & $96$ & $5$ & $107$ & $213$ & $1$ & $107$\\ + \bottomrule + \end{tabular} + \end{table} \item \emph{Figure out whether it is possible if the capacity of the truck is set to $318$.} \end{enumerate} diff --git a/a2/3.tex b/a2/3.tex index e69de29..a6e47e9 100644 --- a/a2/3.tex +++ b/a2/3.tex @@ -0,0 +1 @@ +\section{Problem 3} diff --git a/a2/4.model b/a2/4.model new file mode 100644 index 0000000..e69de29 diff --git a/a2/4.tex b/a2/4.tex index 9eb06c0..cfec0ab 100644 --- a/a2/4.tex +++ b/a2/4.tex @@ -1,112 +1,109 @@ \section{Solving solitaire} \subsection{Problem description} -Standard \emph{Peg solitaire} is a game played with marbles or pegs on a board -with $33$ holes as displayed in Figure~\ref{lst:pegs}. In the Figure dots -represent a peg and o's represent a empty hole. The goal is to end up with the -last peg in the middle hole and all other pegs removed from the board. -To achieve this you have make moves that capture another peg. You can capture -another peg by finding a peg bordering it in a certain direction and on the -other side there needs to be an empty spot. The four possible moves are -displayed in Figure~\ref{lst:moves}. - -Since there is no such thing as an empty move we know the game is always -finished in $31$ steps. This is because in the start position there are $32$ -pegs on the playing field, every move we remove one peg, thus requiring $31$ -moves to end up with only one peg. +Standard \emph{English Peg solitaire} is a single player game played on a board +with $33$ holes and is played with $32$ pegs. In the initial position all holes +are occupied except for the middle hole. A traditional board is shown in +Figure~\ref{fig:sol}. The goal of the game is to remove all but one peg on the +middle position. The player can remove a peg by jumping over the peg +orthogonally to a position two holes away. The middle peg is then removed from +the board. To visualize board configurations we use the symbol $\circ$ for a +position occupied by a peg and the symbol $\times$ by a position not occupied. +The initial board configuration and possible moves are shown in +Figure~\ref{fig:init}. Variations on the game exists with different board shapes such as triangles, rotated squares or bigger crosses. There is also an alternative that makes the -end condition more flexible. Instead of requiring the last peg to be in the -middle of the board, the last peg can be anywhere on the board. - -\begin{lstlisting}[caption={Standard English peg solitaire starting -position},label={lst:pegs}] - ... - ... -....... -...o... -....... - ... - ... -\end{lstlisting} +end condition more flexible by allowing the last peg anywhere on the board. +\begin{figure}[H] + \centering + \includegraphics[width=.2\linewidth]{board.jpg} + \caption{Peg solitaire board}\label{fig:sol} +\end{figure} -\begin{lstlisting}[caption={Moves in all possible directions}, -label={lst:moves}] -right left down up - . . o . -..o->oo. o..->.oo . -> o . -> o - o o . o -\end{lstlisting} +\begin{figure}[H] + $$\xymatrix@1@=1pt@M=1pt{ + & 0 & 1 & 2 & 3 & 4 & 5 & 6\\ + 0 & & & \circ & \circ & \circ & & & & & & + \circ\ar@/^/[rr] & \circ & \times & \rightarrow & + \times & \times & \circ\\ + 1 & & & \circ & \circ & \circ\\ + 2 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & & + \times & \circ & \circ\ar@/_/[ll]& \rightarrow & + \circ & \times & \times\\ + 3 & \circ & \circ & \circ & \times & \circ & \circ & \circ\\ + 4 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & & + \circ\ar@/_/[dd] & & \times & & \times & & \circ\\ + 5 & & & \circ & \circ & \circ & & & & & & + \circ & \rightarrow & \times & & \circ & \rightarrow& \times\\ + 6 & & & \circ & \circ & \circ & & & & & & + \times & & \circ & & \circ\ar@/^/[uu] & & \times\\ + }$$ + \caption{Initial board state and possible moves}\label{fig:init} +\end{figure} \subsection{Formalization} -Basically there are two possible formalization techniques we can use. -Formalization per position and formalization per peg. +Because in every move a peg is captured the game ends in exactly $31$ moves +since there are $32$ pegs and one is left with a sole peg. A position $p$ means +the $x$ and the $y$ coordinate as shown in Figure~\ref{fig:init}. Stating for a +point $p$, $p_x$ or $p_y$ it means the respective $x$ and $y$ component of the +position.\\ -Formalization per position means that we keep track of all the board positions -and model what the position would be in the next state considering all possible -moves. Every move there are only three positions on the board that are updated. -On the entire board there are only $76$ possible combinations of three -positions that can result in a move. This means that the formalization results -in a big disjunction of the $76$ different moves. +Set $\mathcal{P}$ is the set of all legal board positions and can be defined +as: +$$\mathcal{P}=\left\{p\in \{0\ldots7\}^2|\text{where }\neg( + (p_x<2\wedge p_y<2)\vee + (p_x>4\wedge p_y>4)\vee + (p_x>4\wedge p_y<2)\vee + (p_x<2\wedge p_y>4)\right\}$$ -The second method would be to formalize the game in means of the pegs. For -every peg we keep track of the location and when the peg is removed we put them -in the bin. In this way when we end up with only one peg with a valid winning -location and the rest in the bin the game is over. Expected is that this method -has a much higher branching factor. Moves always consist of two pegs. So for -every move we have to check every combination of pegs and every direction. This -means that when there are $32$ pegs in the game there are -$32\cdot31\cdot4=3968$ possible moves we should check. Ofcourse we can prune a -lot of combinations very quickly because one of the pegs might already in the -bin or the position of the pegs was not correct but it is still a very large -branching factor. Because of the high branching factor we first attempt to -solve the problem using the position based approach. +Set $\mathcal{M}$ is the set of position triples that form a legal move. $s$ +denotes the start position, $m$ denotes the middle position and $e$ the final +position. +$$\begin{array}{l} + \mathcal{M}=\{(s,m,e)\in \{0\ldots7\}^3|\text{where }\\ + \qquad\qquad(s_x=m_x\wedge m_x=e_x\wedge + (m_y=s_y+1\wedge e_y=m_y+1\vee m_y=s_y-1\wedge e_y=m_y-1)\vee\\ + \qquad\qquad(s_y=m_y\wedge m_y=e_y\wedge + (m_x=s_x+1\wedge e_x=m_x+1\vee m_x=s_x-1\wedge e_x=m_x-1)\\ +\end{array}$$ -\begin{lstlisting}[caption={Coordinate system},label={lst:coord}] - 0123456 -0 ooo -1 ooo -2ooooooo -3ooooooo -4ooooooo -5 ooo -6 ooo -\end{lstlisting} +For every iteration $i\in\{0\ldots32\}$ and for every position $p\in \mathcal{P}$ +we create a variable representing the state of occupation. We also define +$g=\langle3,3\rangle$ as being the middle position. With these definitions we +can describe the initial state $\mathcal{INIT}$ as follows: +$$\neg i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}} +i_0x_{p_x}y_{p_y}$$ -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\}$. +Every iteration with $i>0$ we define with a function called $\mathcal{ITER}(i)$ +which for every move describes the updates for the positions. Only the +positions involved in the move are updated when the rest stay the same. Part +$(1)$ of the formula describes the preconditions for a move to be valid. $(2)$ +describes the result of the move and $(3)$ expresses the invariability of the +other positions. +$$\begin{array}{llr} + \bigvee_{(s,m,e)\in M} \Biggl[& + i_{i-1}x_{s_x}y_{s_y}\wedge + i_{i-1}x_{m_x}y_{m_y}\wedge + \neg i_{i-1}x_{e_x}y_{e_y}\wedge & (1)\\ + & \neg i_{i}x_{s_x}y_{s_y}\wedge + \neg i_{i}x_{m_x}y_{m_y}\wedge + i_{i}x_{e_x}y_{e_y}\wedge & (2)\\ + & \bigwedge_{o\in \mathcal{P}\setminus\{s,m,e\}} + i_ix_{o_x}y_{o_y}=i_{i-1}x_{o_x}y_{o_y}\quad\Biggr] & (3) +\end{array} +$$ -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 -but some are excluded from being a legal middle position of a move. Basically -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)\}$ +The final state should be an inversion of the initial state. All holes should +be empty except the middle hole $g$. $\mathcal{POST}$ is defined as follows: +$$i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}} +\neg i_0x_{p_x}y_{p_y}$$ -\begin{align} - \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( - & \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\\ - & \neg i_{i}x_{sx}y_{sy}\wedge - \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)\wedge\\ - i_{31}x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}\neg i_{31}x_xy_y -\end{align} +All of this together in the following formula is satisfiable if +and only if there is a solution to English \textit{Peg solitaire}. The model +that satisfies the formula is the sequence of moves to be performed to win a +game. +$$\mathcal{INIT}\wedge\left(\bigwedge_{i=1}^{31}\mathcal{ITER}(i)\right) +\wedge\mathcal{POST}$$ -\lstinputlisting[caption={Solution for peg solitaire},label={lst:sol}] - {./src/4/a4.tex} +\subsection{Solution} +The conversion to SMT-Lib is trivial diff --git a/a2/ar.tex b/a2/ar.tex index 5dabd82..73a4629 100644 --- a/a2/ar.tex +++ b/a2/ar.tex @@ -3,12 +3,16 @@ \maketitle \tableofcontents +\newpage \input{1.tex} +\newpage \input{2.tex} +\newpage \input{3.tex} +\newpage \input{4.tex} \end{document} diff --git a/a2/board.jpg b/a2/board.jpg new file mode 100644 index 0000000..ed7505d Binary files /dev/null and b/a2/board.jpg differ diff --git a/a2/pre.tex b/a2/pre.tex index 7970698..b9325ec 100644 --- a/a2/pre.tex +++ b/a2/pre.tex @@ -7,6 +7,8 @@ \usepackage{amsmath} % For nice tables \usepackage{listings} % For nice tables \usepackage{float} % For nice tables +\usepackage{graphicx} +\usepackage{xypic} \everymath{\displaystyle} diff --git a/a2/src/1.bak b/a2/src/1.bak new file mode 100644 index 0000000..2966704 --- /dev/null +++ b/a2/src/1.bak @@ -0,0 +1,126 @@ +#!/bin/bash +YICES=~/projects/yices-2.4.2/bin/yices-smt +AI=40 +BI=30 +CI=145 +AMAX=120 +BMAX=120 +CMAX=200 + +function generate { + ITERATIONS=$1 + TMAX=$2 + cat< a$i 0) + (> b$i 0) + (> c$i 0) + (or ;-- ITERATION $i + (and ;-- SPECIAL CASE FOR STATE S(0) + (= l$i 0) + (= d$i 0) + (= t$i $TMAX) + (= a$i (- a$((i-1)) p$i)) + (= b$i (- b$((i-1)) p$i)) + (= c$i (- c$((i-1)) p$i)) + (or + (and ;-- CAME FROM A + (= l$((i-1)) 1) + (= p$i 29) + ) + (and ;-- CAME FROM B + (= l$((i-1)) 2) + (= p$i 21) + ) + ) + ) + (and ;-- CASE FOR STATE A(1) + (= l$i 1) + (>= d$i 0) (<= d$i t$((i-1))) + (<= d$i (+ p$i (- $AMAX a$((i-1))))) + (= t$i (- t$((i-1)) d$i)) + (= a$i (- (+ a$((i-1)) d$i) p$i)) + + (= b$i (- b$((i-1)) p$i)) + (= c$i (- c$((i-1)) p$i)) + (or + (and ;-- CAME FROM S(0) + (= l$((i-1)) 0) + (= p$i 29) + ) (and ;-- CAME FROM B(2) + (= p$i 17) + (= l$((i-1)) 2) + ) (and ;-- CAME FROM C(3) + (= p$i 32) + (= l$((i-1)) 3) + ) + ) + ) + (and ;-- CASE FOR STATE B(2) + (= l$i 3) + (>= d$i 0) (<= d$i t$((i-1))) + (<= d$i (+ p$i (- $BMAX b$((i-1))))) + (= t$i (- t$((i-1)) d$i)) + (= b$i (- (+ b$((i-1)) d$i) p$i)) + + (= a$i (- a$((i-1)) p$i)) + (= c$i (- c$((i-1)) p$i)) + + (or + (and ;-- CAME FROM S(0) + (= l$((i-1)) 0) + (= p$i 21) + ) (and ;-- CAME FROM A(1) + (= l$((i-1)) 1) + (= p$i 17) + ) (and ;-- CAME FROM C(3) + (= l$((i-1)) 3) + (= p$i 37) + ) + ) + ) + (and ;-- CASE FOR STATE C(3) + (= l$i 3) + (>= d$i 0) (<= d$i t$((i-1))) + (<= d$i (+ p$i (- $CMAX c$((i-1))))) + (= t$i (- t$((i-1)) d$i)) + (= c$i (- (+ c$((i-1)) d$i) p$i)) + (= a$i (- a$((i-1)) p$i)) + (= b$i (- b$((i-1)) p$i)) + (or + (and ;-- CAME FROM A(1) + (= l$((i-1)) 1) + (= p$i 32) + ) (and ;-- CAME FROM B(2) + (= l$((i-1)) 2) + (= p$i 37) + ) + ) + ) + ) +GEN + done + cat< $1 -generate diff --git a/a2/src/1a.bash b/a2/src/1a.bash new file mode 100755 index 0000000..1724514 --- /dev/null +++ b/a2/src/1a.bash @@ -0,0 +1,166 @@ +#!/bin/bash +YICES=~/projects/yices-2.4.2/bin/yices-smt +AI=40 +BI=30 +CI=145 +AMAX=120 +BMAX=120 +CMAX=200 + +function generate { + ITERATIONS=$1 + TMAX=$2 + cat< a$i 0) + (> b$i 0) + (> c$i 0) + (>= d$i 0) + (<= d$i $TMAX) + (>= t$i 0) + (<= t$i $TMAX) + (or ;-- ITERATION $i + (and ;-- WAS IN S + (= l$((i-1)) 0) + (or + (and ; now in A + (= l$i 1) + (<= d$i (+ 29 (- $AMAX a$((i-1))))) + (= a$i (+ (- a$((i-1)) 29) d$i)) + + (= b$i (- b$((i-1)) 29)) + (= c$i (- c$((i-1)) 29)) + + (= t$i (- t$((i-1)) d$i)) + ) (and ; now in B + (= l$i 2) + (<= d$i (+ 21 (- $BMAX b$((i-1))))) + (= b$i (+ (- b$((i-1)) 21) d$i)) + + (= a$i (- a$((i-1)) 21)) + (= c$i (- c$((i-1)) 21)) + + (= t$i (- t$((i-1)) d$i)) + ) + ) + ) + (and ;-- WAS IN A + (= l$((i-1)) 1) + (or + (and ; now in S + (= l$i 0) + (= d$i 0) + + (= a$i (- a$((i-1)) 29)) + (= b$i (- b$((i-1)) 29)) + (= c$i (- c$((i-1)) 29)) + + (= t$i $TMAX) + ) (and ; now in B + (= l$i 2) + (<= d$i (+ 17 (- $BMAX b$((i-1))))) + (= b$i (+ (- b$((i-1)) 17) d$i)) + + (= a$i (- a$((i-1)) 17)) + (= c$i (- c$((i-1)) 17)) + + (= t$i (- t$((i-1)) d$i)) + ) (and ; now in C + (= l$i 3) + + (<= d$i (+ 32 (- $CMAX c$((i-1))))) + (= c$i (+ (- c$((i-1)) 32) d$i)) + + (= a$i (- a$((i-1)) 32)) + (= b$i (- b$((i-1)) 32)) + + (= t$i (- t$((i-1)) d$i)) + ) + ) + ) + (and ;-- WAS IN B + (= l$((i-1)) 2) + (or + (and ; now in S + (= l$i 0) + (= d$i 0) + + (= a$i (- a$((i-1)) 21)) + (= b$i (- b$((i-1)) 21)) + (= c$i (- c$((i-1)) 21)) + + (= t$i $TMAX) + ) (and ; now in A + (= l$i 1) + (<= d$i (+ 17 (- $AMAX a$((i-1))))) + (= a$i (+ (- a$((i-1)) 17) d$i)) + + (= b$i (- b$((i-1)) 17)) + (= c$i (- c$((i-1)) 17)) + + (= t$i (- t$((i-1)) d$i)) + ) (and ; now in C + (= l$i 3) + (<= d$i (+ 37 (- $CMAX c$((i-1))))) + (= c$i (+ (- c$((i-1)) 37) d$i)) + + (= a$i (- a$((i-1)) 37)) + (= b$i (- b$((i-1)) 37)) + + (= t$i (- t$((i-1)) d$i)) + ) + ) + ) + (and ;-- WAS IN C + (= l$((i-1)) 3) + (or + (and ; now in A + (= l$i 1) + (<= d$i (+ 32 (- $AMAX a$((i-1))))) + (= a$i (+ (- a$((i-1)) 32) d$i)) + + (= b$i (- b$((i-1)) 32)) + (= c$i (- c$((i-1)) 32)) + + (= t$i (- t$((i-1)) d$i)) + ) (and ; now in B + (= l$i 2) + (<= d$i (+ 37 (- $BMAX b$((i-1))))) + (= b$i (+ (- b$((i-1)) 37) d$i)) + + (= a$i (- a$((i-1)) 37)) + (= c$i (- c$((i-1)) 37)) + + (= t$i (- t$((i-1)) d$i)) + ) + ) + ) + ) +GEN + done + echo "(or" + for i in $(seq 0 $ITERATIONS); do + for j in $(seq $((i+1)) $ITERATIONS); do + echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))" + done + done + echo ")))" +} +it=1 +while generate $it 318 | $YICES -m | pee sort "grep -q unsat" +do + echo $((it++)) +done diff --git a/a2/src/1b.bash b/a2/src/1b.bash new file mode 100755 index 0000000..17a3e78 --- /dev/null +++ b/a2/src/1b.bash @@ -0,0 +1,127 @@ +#!/bin/bash +YICES=~/projects/yices-2.4.2/bin/yices-smt +AI=40 +BI=30 +CI=145 +AMAX=120 +BMAX=120 +CMAX=200 + +function generate { + ITERATIONS=$1 + TMAX=$2 + cat< a$i 0) + (> b$i 0) + (> c$i 0) + (or ;-- ITERATION $i + (and ;-- SPECIAL CASE FOR STATE S(0) + (= l$i 0) + (= d$i 0) + (= t$i $TMAX) + (or + (and ;-- CAME FROM A + (= l$((i-1)) 1) + (= a$i (- a$((i-1)) 29)) + (= b$i (- b$((i-1)) 29)) + (= c$i (- c$((i-1)) 29)) + ) + (and ;-- CAME FROM B + (= l$((i-1)) 2) + (= a$i (- a$((i-1)) 21)) + (= b$i (- b$((i-1)) 21)) + (= c$i (- c$((i-1)) 21)) + ) + ) + ) + (and ;-- CASE FOR STATE A(1) + (= l$i 1) + (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $AMAX a$((i-1)))) + (= t$i (- t$((i-1)) d$i)) (= a$i (+ a$((i-1)) d$i)) + + (or + (and ;-- CAME FROM S(0) + (= l$((i-1)) 0) + (= b$i (- b$((i-1)) 29)) + (= c$i (- c$((i-1)) 29)) + ) (and ;-- CAME FROM B(2) + (= l$((i-1)) 2) + (= b$i (- b$((i-1)) 17)) + (= c$i (- c$((i-1)) 17)) + ) (and ;-- CAME FROM C(3) + (= l$((i-1)) 3) + (= b$i (- b$((i-1)) 32)) + (= c$i (- c$((i-1)) 32)) + ) + ) + ) + (and ;-- CASE FOR STATE B(2) + (= l$i 2) + (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $BMAX b$((i-1)))) + (= t$i (- t$((i-1)) d$i)) (= b$i (+ b$((i-1)) d$i)) + + (or + (and ;-- CAME FROM S(0) + (= l$((i-1)) 0) + (= a$i (- a$((i-1)) 21)) + (= c$i (- c$((i-1)) 21)) + ) (and ;-- CAME FROM A(1) + (= l$((i-1)) 1) + (= a$i (- a$((i-1)) 17)) + (= c$i (- c$((i-1)) 17)) + ) (and ;-- CAME FROM C(3) + (= l$((i-1)) 3) + (= a$i (- a$((i-1)) 37)) + (= c$i (- c$((i-1)) 37)) + ) + ) + ) + (and ;-- CASE FOR STATE C(3) + (= l$i 3) + (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $CMAX c$((i-1)))) + (= t$i (- t$((i-1)) d$i)) (= c$i (+ c$((i-1)) d$i)) + + (or + (and ;-- CAME FROM A(1) + (= l$((i-1)) 1) + (= a$i (- a$((i-1)) 32)) + (= b$i (- b$((i-1)) 32)) + ) (and ;-- CAME FROM B(2) + (= l$((i-1)) 2) + (= a$i (- a$((i-1)) 37)) + (= b$i (- b$((i-1)) 37)) + ) + ) + ) + ) +GEN + done + echo "(or" + for i in $(seq 0 $ITERATIONS); do + for j in $(seq $((i+1)) $ITERATIONS); do + echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))" + done + done + echo ")))" +} + +it=1 +while generate $it 320 | $YICES -m | pee sort "grep unsat" +do + it=$((it+1)) +done +echo $it diff --git a/a2/src/4/4.model b/a2/src/4/4.model index 3b52ae7..e69de29 100644 --- a/a2/src/4/4.model +++ b/a2/src/4/4.model @@ -1,1059 +0,0 @@ -sat - -(= i1x2y0 true) -(= i4x2y1 false) -(= i1x2y3 true) -(= i11x2y5 false) -(= i31x6y2 false) -(= i26x0y3 true) -(= i10x3y6 true) -(= i13x3y5 true) -(= i20x0y4 false) -(= i30x2y2 false) -(= i6x2y3 true) -(= i6x5y3 true) -(= i0x4y0 true) -(= i17x2y0 false) -(= i20x3y1 false) -(= i24x5y4 false) -(= i16x4y6 false) -(= i26x0y4 false) -(= i26x2y5 false) -(= i14x2y6 false) -(= i29x1y4 true) -(= i1x0y4 true) -(= i21x3y3 false) -(= i31x4y2 false) -(= i18x6y3 false) -(= i3x1y2 true) -(= i4x3y6 true) -(= i9x1y3 true) -(= i16x6y4 false) -(= i18x6y4 false) -(= i19x1y4 true) -(= i14x3y0 false) -(= i9x3y3 false) -(= i3x5y4 true) -(= i21x4y5 false) -(= i14x4y5 false) -(= i30x5y2 false) -(= i22x4y6 false) -(= i6x0y3 true) -(= i18x2y5 false) -(= i27x1y2 false) -(= i26x2y1 false) -(= i24x4y6 false) -(= i31x4y4 false) -(= i19x5y3 false) -(= i15x1y4 false) -(= i9x3y6 true) -(= i0x3y1 true) -(= i14x6y2 false) -(= i28x0y3 false) -(= i0x6y2 true) -(= i9x5y3 true) -(= i13x0y4 true) -(= i11x1y3 true) -(= i7x3y3 false) -(= i21x2y4 false) -(= i15x5y4 false) -(= i27x4y2 false) -(= i6x0y2 true) -(= i14x3y4 false) -(= i9x0y4 true) -(= i20x6y4 false) -(= i7x1y4 true) -(= i21x1y2 true) -(= i24x4y5 false) -(= i30x4y5 false) -(= i31x1y4 false) -(= i8x4y1 false) -(= i1x3y5 true) -(= i3x2y6 true) -(= i13x1y4 true) -(= i2x6y2 true) -(= i9x4y1 false) -(= i29x0y2 false) -(= i15x0y4 false) -(= i28x5y2 false) -(= i24x3y6 false) -(= i18x3y1 false) -(= i19x4y6 false) -(= i22x3y1 false) -(= i19x4y1 false) -(= i13x2y0 false) -(= i27x3y3 false) -(= i12x3y5 true) -(= i16x2y0 false) -(= i10x4y0 false) -(= i27x2y0 false) -(= i11x3y4 true) -(= i9x3y0 true) -(= i2x3y6 true) -(= i12x6y2 true) -(= i18x2y6 true) -(= i23x3y4 false) -(= i13x0y2 true) -(= i31x2y4 false) -(= i13x3y6 true) -(= i2x0y4 true) -(= i8x4y6 true) -(= i17x5y4 true) -(= i18x3y2 true) -(= i6x1y2 true) -(= i16x1y3 true) -(= i18x3y3 false) -(= i27x0y4 false) -(= i6x2y5 true) -(= i24x3y0 false) -(= i9x3y1 false) -(= i11x5y4 true) -(= i3x2y3 true) -(= i15x0y2 true) -(= i27x3y2 false) -(= i12x6y3 true) -(= i5x0y2 true) -(= i29x0y3 false) -(= i30x4y6 false) -(= i13x3y3 false) -(= i28x4y5 false) -(= i31x4y3 false) -(= i2x4y5 true) -(= i8x6y4 false) -(= i13x3y1 false) -(= i10x4y1 false) -(= i17x2y1 false) -(= i26x3y2 false) -(= i30x4y0 false) -(= i19x6y3 false) -(= i24x2y1 false) -(= i12x1y4 true) -(= i29x3y6 false) -(= i23x0y3 true) -(= i6x4y3 true) -(= i15x3y5 true) -(= i23x0y4 false) -(= i29x6y2 false) -(= i21x4y4 false) -(= i14x4y3 true) -(= i29x3y0 false) -(= i24x6y3 false) -(= i25x3y3 false) -(= i5x2y2 true) -(= i30x5y4 false) -(= i16x0y4 false) -(= i2x5y3 false) -(= i3x1y3 true) -(= i12x2y0 false) -(= i16x2y5 false) -(= i25x2y6 true) -(= i7x0y3 true) -(= i10x3y2 true) -(= i12x3y1 false) -(= i26x6y3 false) -(= i27x6y3 false) -(= i6x1y4 true) -(= i20x3y3 false) -(= i27x6y4 false) -(= i29x2y6 false) -(= i3x6y3 true) -(= i24x6y2 false) -(= i1x5y4 true) -(= i27x5y4 false) -(= i10x2y4 true) -(= i30x3y6 false) -(= i26x2y3 false) -(= i14x2y3 true) -(= i28x3y5 true) -(= i5x0y4 true) -(= i24x1y2 true) -(= i2x1y3 true) -(= i4x1y3 true) -(= i7x3y0 true) -(= i15x3y4 false) -(= i25x2y5 false) -(= i12x3y2 true) -(= i22x6y4 false) -(= i14x4y6 true) -(= i14x2y1 false) -(= i22x4y1 false) -(= i24x0y4 false) -(= i26x3y5 true) -(= i4x1y4 true) -(= i23x5y2 false) -(= i30x2y6 false) -(= i16x4y4 true) -(= i25x2y2 true) -(= i0x4y3 true) -(= i6x4y5 false) -(= i20x3y2 true) -(= i30x6y3 false) -(= i20x2y0 false) -(= i29x3y5 true) -(= i12x4y3 true) -(= i22x2y5 false) -(= i12x5y3 true) -(= i28x3y3 false) -(= i23x4y1 false) -(= i24x5y3 false) -(= i20x3y5 true) -(= i8x2y0 true) -(= i17x3y0 false) -(= i9x6y4 false) -(= i2x4y6 true) -(= i29x0y4 false) -(= i13x0y3 true) -(= i8x2y2 true) -(= i14x2y5 false) -(= i17x2y3 true) -(= i11x3y0 false) -(= i24x4y1 false) -(= i14x4y0 true) -(= i27x4y4 false) -(= i4x5y4 true) -(= i23x3y3 false) -(= i9x1y2 true) -(= i3x6y2 true) -(= i30x0y2 false) -(= i3x2y1 false) -(= i11x4y4 false) -(= i6x2y2 true) -(= i15x2y4 true) -(= i23x4y4 false) -(= i26x1y3 true) -(= i4x0y3 true) -(= i28x0y4 false) -(= i29x6y3 false) -(= i2x4y0 true) -(= i0x3y0 true) -(= i14x3y3 false) -(= i30x4y1 false) -(= i11x6y4 false) -(= i0x3y6 true) -(= i12x1y3 true) -(= i8x1y3 true) -(= i28x2y2 false) -(= i4x2y5 true) -(= i26x1y4 true) -(= i6x4y6 true) -(= i21x0y3 true) -(= i21x4y3 false) -(= i26x4y0 false) -(= i24x3y3 false) -(= i18x4y1 false) -(= i21x3y0 false) -(= i25x2y1 false) -(= i26x3y6 false) -(= i27x1y4 true) -(= i27x4y5 false) -(= i28x2y6 true) -(= i27x3y6 false) -(= i19x2y6 true) -(= i1x2y1 true) -(= i0x0y3 true) -(= i25x4y6 false) -(= i4x1y2 true) -(= i0x2y0 true) -(= i17x6y3 false) -(= i11x5y2 true) -(= i7x6y3 true) -(= i12x3y3 false) -(= i9x0y2 true) -(= i21x2y2 false) -(= i4x2y3 true) -(= i16x3y1 false) -(= i21x3y1 false) -(= i24x4y2 false) -(= i4x0y4 true) -(= i7x3y5 true) -(= i11x4y3 true) -(= i9x2y3 true) -(= i20x2y6 true) -(= i18x4y5 false) -(= i2x0y2 true) -(= i13x4y0 true) -(= i25x3y6 false) -(= i27x3y5 true) -(= i4x3y3 true) -(= i31x4y5 false) -(= i10x0y2 true) -(= i20x2y5 false) -(= i9x4y6 true) -(= i1x3y1 true) -(= i28x1y2 false) -(= i28x6y2 false) -(= i20x6y2 false) -(= i5x2y5 true) -(= i1x0y2 true) -(= i1x4y5 true) -(= i1x1y3 true) -(= i6x0y4 true) -(= i14x5y2 true) -(= i9x6y2 true) -(= i19x0y3 true) -(= i21x3y2 true) -(= i26x4y2 false) -(= i24x1y3 true) -(= i20x4y1 false) -(= i5x3y6 true) -(= i23x1y4 true) -(= i1x6y2 true) -(= i23x5y3 false) -(= i12x2y1 false) -(= i2x0y3 true) -(= i18x4y6 false) -(= i7x4y0 false) -(= i1x1y2 true) -(= i0x2y1 true) -(= i1x5y3 false) -(= i1x3y0 true) -(= i8x4y0 false) -(= i10x5y4 true) -(= i4x0y2 true) -(= i26x3y3 false) -(= i0x4y6 true) -(= i7x6y2 true) -(= i17x1y3 true) -(= i13x4y4 false) -(= i3x4y1 true) -(= i5x3y4 true) -(= i21x3y5 true) -(= i28x4y0 false) -(= i22x3y5 true) -(= i14x3y6 true) -(= i2x3y5 true) -(= i29x4y6 false) -(= i12x2y2 true) -(= i30x3y3 false) -(= i17x5y2 false) -(= i4x3y5 true) -(= i11x3y3 false) -(= i30x3y5 true) -(= i14x5y4 true) -(= i8x5y2 true) -(= i25x4y0 false) -(= i9x4y4 false) -(= i4x3y0 true) -(= i3x4y3 true) -(= i11x2y6 false) -(= i18x3y5 true) -(= i12x4y0 true) -(= i11x3y5 true) -(= i28x4y3 false) -(= i14x3y2 true) -(= i16x5y3 true) -(= i6x5y4 true) -(= i2x3y4 true) -(= i19x5y4 false) -(= i1x6y4 true) -(= i15x5y2 true) -(= i1x3y4 true) -(= i3x2y5 true) -(= i20x5y4 false) -(= i23x0y2 true) -(= i23x2y5 false) -(= i3x4y6 true) -(= i6x4y4 false) -(= i7x2y1 false) -(= i26x4y5 false) -(= i25x4y1 false) -(= i10x2y2 true) -(= i23x2y1 true) -(= i9x6y3 true) -(= i8x3y1 false) -(= i13x1y3 true) -(= i14x2y0 false) -(= i7x4y5 false) -(= i15x1y2 true) -(= i21x2y1 true) -(= i1x2y6 true) -(= i17x2y6 true) -(= i12x1y2 true) -(= i22x1y2 true) -(= i12x5y4 true) -(= i1x6y3 true) -(= i25x2y4 false) -(= i25x4y5 false) -(= i7x3y4 true) -(= i10x3y1 false) -(= i25x4y2 false) -(= i18x0y4 false) -(= i26x5y3 false) -(= i11x2y4 true) -(= i10x2y1 false) -(= i18x2y3 true) -(= i24x2y4 false) -(= i29x2y5 false) -(= i28x2y5 true) -(= i11x4y2 true) -(= i7x3y2 true) -(= i16x4y5 false) -(= i27x0y3 false) -(= i16x6y3 false) -(= i19x3y2 true) -(= i20x5y2 false) -(= i12x3y6 true) -(= i22x3y6 false) -(= i27x2y1 false) -(= i13x3y4 false) -(= i24x3y1 false) -(= i10x6y2 true) -(= i0x3y5 true) -(= i21x5y4 false) -(= i17x0y4 false) -(= i7x0y4 true) -(= i8x6y2 true) -(= i10x1y3 true) -(= i11x3y2 true) -(= i24x4y3 false) -(= i13x4y5 false) -(= i13x6y2 false) -(= i25x5y3 false) -(= i13x5y2 true) -(= i13x6y4 true) -(= i15x2y2 true) -(= i31x2y6 false) -(= i25x1y2 false) -(= i18x0y3 true) -(= i29x2y4 true) -(= i0x2y5 true) -(= i15x4y5 false) -(= i16x2y1 false) -(= i29x4y2 false) -(= i30x3y1 false) -(= i28x5y3 false) -(= i13x4y1 false) -(= i13x4y3 true) -(= i22x5y2 false) -(= i14x0y3 true) -(= i20x6y3 false) -(= i7x2y2 true) -(= i22x2y6 true) -(= i18x4y2 true) -(= i10x4y3 true) -(= i24x3y2 false) -(= i16x4y2 true) -(= i20x4y5 false) -(= i24x2y6 true) -(= i17x0y3 true) -(= i26x2y2 false) -(= i31x3y2 false) -(= i23x2y4 false) -(= i18x0y2 true) -(= i24x2y0 false) -(= i5x2y6 true) -(= i25x1y4 true) -(= i29x3y3 false) -(= i13x5y3 true) -(= i17x1y2 true) -(= i27x2y5 false) -(= i22x5y4 false) -(= i8x2y6 true) -(= i30x2y5 false) -(= i6x6y2 true) -(= i28x4y6 false) -(= i3x6y4 true) -(= i29x2y2 false) -(= i22x5y3 false) -(= i26x3y4 false) -(= i11x0y2 true) -(= i6x3y2 true) -(= i11x2y2 true) -(= i0x3y3 false) -(= i1x4y1 true) -(= i11x4y0 true) -(= i12x0y4 true) -(= i10x2y6 false) -(= i28x6y4 false) -(= i17x3y3 false) -(= i20x2y4 false) -(= i4x4y5 true) -(= i5x1y3 true) -(= i0x2y4 true) -(= i15x2y1 false) -(= i26x5y2 false) -(= i25x3y4 false) -(= i3x1y4 true) -(= i26x3y1 false) -(= i8x6y3 true) -(= i19x0y2 true) -(= i11x4y1 false) -(= i19x3y4 false) -(= i28x4y2 false) -(= i2x5y4 true) -(= i23x6y3 false) -(= i21x4y6 false) -(= i10x4y2 true) -(= i26x3y0 false) -(= i6x3y4 true) -(= i25x3y5 true) -(= i17x4y0 true) -(= i27x2y3 true) -(= i29x5y2 false) -(= i12x2y4 false) -(= i0x2y3 true) -(= i24x4y0 false) -(= i13x4y6 true) -(= i31x2y5 false) -(= i30x2y3 false) -(= i4x4y3 true) -(= i14x5y3 true) -(= i7x3y1 false) -(= i17x4y2 true) -(= i22x2y1 true) -(= i0x0y2 true) -(= i11x4y6 true) -(= i7x0y2 true) -(= i4x2y6 true) -(= i22x3y0 false) -(= i9x4y0 false) -(= i23x6y2 false) -(= i9x2y0 true) -(= i16x6y2 false) -(= i15x2y0 false) -(= i29x2y0 false) -(= i2x3y1 true) -(= i5x4y3 false) -(= i3x3y5 true) -(= i9x2y5 true) -(= i27x6y2 false) -(= i22x6y3 false) -(= i1x1y4 true) -(= i23x1y3 true) -(= i5x5y3 true) -(= i17x4y5 false) -(= i17x0y2 true) -(= i18x3y0 false) -(= i6x4y2 true) -(= i24x0y2 true) -(= i0x2y2 true) -(= i7x3y6 true) -(= i20x2y3 false) -(= i31x5y2 false) -(= i22x3y4 false) -(= i1x2y4 true) -(= i16x4y0 true) -(= i19x6y4 false) -(= i8x4y4 false) -(= i19x3y0 false) -(= i30x6y4 false) -(= i22x0y3 true) -(= i4x4y1 false) -(= i29x3y2 false) -(= i8x5y4 true) -(= i5x1y4 true) -(= i29x1y3 false) -(= i7x2y5 true) -(= i10x0y4 true) -(= i5x2y1 false) -(= i8x1y4 true) -(= i13x2y6 false) -(= i14x2y4 true) -(= i22x3y2 true) -(= i22x4y3 false) -(= i8x4y5 false) -(= i24x2y3 true) -(= i7x4y3 true) -(= i7x4y4 true) -(= i5x3y3 false) -(= i28x4y4 false) -(= i3x5y2 true) -(= i30x0y3 false) -(= i10x1y2 true) -(= i8x5y3 true) -(= i0x4y4 true) -(= i3x4y0 true) -(= i31x2y3 false) -(= i18x4y4 false) -(= i6x2y6 true) -(= i28x3y4 false) -(= i16x3y5 true) -(= i19x3y1 false) -(= i22x3y3 false) -(= i24x2y2 false) -(= i24x3y5 true) -(= i5x4y0 false) -(= i12x4y1 false) -(= i17x2y2 true) -(= i28x2y1 false) -(= i16x2y4 true) -(= i24x4y4 false) -(= i6x6y3 true) -(= i8x2y3 true) -(= i3x3y4 true) -(= i22x4y4 false) -(= i1x2y2 true) -(= i5x0y3 true) -(= i8x4y3 true) -(= i20x1y3 true) -(= i21x6y3 false) -(= i5x4y1 false) -(= i8x0y2 true) -(= i19x2y1 false) -(= i21x4y0 true) -(= i23x5y4 false) -(= i15x0y3 true) -(= i10x1y4 false) -(= i29x6y4 false) -(= i5x3y0 true) -(= i13x4y2 true) -(= i27x0y2 false) -(= i17x4y3 true) -(= i26x4y6 false) -(= i10x5y3 true) -(= i29x5y4 false) -(= i18x4y3 true) -(= i4x2y4 true) -(= i1x4y0 true) -(= i10x2y5 false) -(= i25x0y4 false) -(= i5x4y2 true) -(= i30x4y3 false) -(= i2x2y4 true) -(= i25x3y1 false) -(= i3x3y1 false) -(= i12x3y4 false) -(= i15x3y1 false) -(= i2x1y2 true) -(= i22x4y5 false) -(= i17x4y4 true) -(= i6x4y0 false) -(= i17x6y2 false) -(= i18x6y2 false) -(= i5x3y2 true) -(= i7x2y6 true) -(= i21x6y4 false) -(= i25x6y2 false) -(= i2x4y2 false) -(= i31x5y4 false) -(= i3x3y3 true) -(= i14x4y2 true) -(= i19x6y2 false) -(= i25x5y4 false) -(= i19x3y5 true) -(= i5x3y5 true) -(= i7x2y4 true) -(= i15x1y3 true) -(= i16x4y1 false) -(= i3x0y4 true) -(= i8x2y5 true) -(= i13x3y2 true) -(= i25x0y3 true) -(= i5x5y4 true) -(= i13x2y3 true) -(= i20x4y0 true) -(= i4x6y2 true) -(= i21x3y6 false) -(= i22x1y3 true) -(= i1x0y3 true) -(= i1x4y3 false) -(= i8x3y5 true) -(= i25x2y0 false) -(= i13x2y5 false) -(= i4x6y4 true) -(= i4x4y4 true) -(= i20x2y2 false) -(= i21x4y2 false) -(= i4x2y2 true) -(= i31x5y3 false) -(= i15x4y2 true) -(= i28x1y3 false) -(= i25x5y2 false) -(= i7x1y3 true) -(= i13x3y0 false) -(= i16x3y4 false) -(= i23x3y5 true) -(= i0x3y2 true) -(= i15x3y3 false) -(= i1x4y6 true) -(= i2x3y3 true) -(= i19x4y5 false) -(= i7x5y3 true) -(= i6x3y6 true) -(= i19x4y0 true) -(= i4x3y1 false) -(= i16x1y4 false) -(= i27x3y0 false) -(= i13x6y3 false) -(= i17x3y5 true) -(= i6x6y4 true) -(= i0x1y4 true) -(= i23x4y6 false) -(= i23x4y2 false) -(= i16x0y3 true) -(= i17x6y4 false) -(= i29x4y0 false) -(= i31x3y1 false) -(= i13x2y2 true) -(= i15x4y3 true) -(= i18x1y3 true) -(= i12x0y3 true) -(= i15x4y4 true) -(= i31x3y0 false) -(= i11x2y3 true) -(= i3x3y2 true) -(= i15x2y3 true) -(= i27x4y3 false) -(= i27x5y3 false) -(= i22x1y4 true) -(= i19x2y2 true) -(= i31x2y1 false) -(= i21x0y4 false) -(= i18x1y4 false) -(= i10x3y0 true) -(= i18x4y0 true) -(= i3x2y2 true) -(= i5x2y0 true) -(= i10x0y3 true) -(= i9x5y2 true) -(= i0x5y3 true) -(= i15x3y6 true) -(= i18x1y2 true) -(= i31x3y4 false) -(= i19x3y3 false) -(= i30x3y0 false) -(= i27x4y1 false) -(= i9x5y4 true) -(= i4x2y0 true) -(= i26x2y0 false) -(= i3x2y4 true) -(= i30x2y1 false) -(= i22x0y4 false) -(= i3x0y2 true) -(= i15x4y1 false) -(= i9x1y4 false) -(= i26x4y3 false) -(= i6x3y3 false) -(= i8x2y1 false) -(= i17x2y4 true) -(= i19x2y3 true) -(= i22x2y4 false) -(= i31x3y6 false) -(= i7x2y3 true) -(= i29x4y4 false) -(= i0x5y4 true) -(= i21x2y3 false) -(= i30x4y2 false) -(= i4x5y2 true) -(= i11x1y2 true) -(= i22x2y3 false) -(= i3x3y0 true) -(= i17x3y1 false) -(= i6x3y5 true) -(= i26x4y1 false) -(= i3x4y4 true) -(= i29x3y4 false) -(= i25x4y4 false) -(= i4x4y0 false) -(= i14x4y1 false) -(= i19x3y6 false) -(= i8x0y4 true) -(= i23x4y3 false) -(= i21x0y2 true) -(= i6x5y2 true) -(= i25x3y2 false) -(= i16x2y6 true) -(= i6x4y1 false) -(= i14x1y3 true) -(= i29x3y1 false) -(= i0x1y3 true) -(= i13x2y4 false) -(= i18x3y4 true) -(= i0x2y6 true) -(= i2x3y2 true) -(= i28x4y1 false) -(= i2x1y4 true) -(= i0x4y2 true) -(= i28x3y6 false) -(= i6x1y3 true) -(= i18x2y2 true) -(= i29x4y3 false) -(= i30x0y4 false) -(= i2x2y3 true) -(= i15x2y5 false) -(= i8x3y6 true) -(= i19x2y4 false) -(= i20x4y4 false) -(= i3x2y0 true) -(= i28x1y4 true) -(= i22x2y2 false) -(= i6x2y4 true) -(= i31x3y5 false) -(= i5x2y3 true) -(= i13x2y1 false) -(= i16x1y2 true) -(= i1x4y4 true) -(= i15x3y0 false) -(= i20x4y3 true) -(= i21x2y5 false) -(= i25x4y3 false) -(= i7x1y2 true) -(= i24x6y4 false) -(= i9x3y4 true) -(= i19x4y3 true) -(= i9x4y2 true) -(= i5x5y2 true) -(= i23x2y2 true) -(= i26x4y4 false) -(= i4x4y6 true) -(= i28x3y0 false) -(= i14x2y2 true) -(= i5x4y6 true) -(= i21x5y3 false) -(= i5x4y4 true) -(= i5x1y2 true) -(= i5x6y3 true) -(= i5x4y5 true) -(= i19x2y0 false) -(= i15x4y0 true) -(= i16x3y3 false) -(= i11x2y0 false) -(= i9x4y5 false) -(= i2x4y1 false) -(= i8x2y4 true) -(= i9x3y2 true) -(= i16x3y0 false) -(= i19x2y5 false) -(= i30x1y2 false) -(= i18x2y4 true) -(= i30x2y0 false) -(= i1x3y6 true) -(= i10x6y4 false) -(= i17x2y5 false) -(= i28x5y4 false) -(= i12x4y2 true) -(= i14x1y4 false) -(= i29x4y5 false) -(= i1x2y5 true) -(= i2x4y3 true) -(= i7x4y1 false) -(= i1x4y2 true) -(= i24x0y3 true) -(= i10x4y4 false) -(= i6x2y1 false) -(= i7x5y2 true) -(= i8x1y2 true) -(= i8x4y2 true) -(= i10x6y3 true) -(= i14x6y4 true) -(= i10x2y0 true) -(= i23x4y0 false) -(= i28x3y1 false) -(= i10x4y5 false) -(= i31x6y4 false) -(= i19x1y2 true) -(= i7x4y2 true) -(= i16x5y2 true) -(= i24x2y5 false) -(= i24x3y4 false) -(= i2x2y1 true) -(= i15x2y6 false) -(= i2x5y2 true) -(= i23x2y6 true) -(= i30x5y3 false) -(= i3x4y5 true) -(= i10x3y5 true) -(= i27x1y3 false) -(= i26x2y6 true) -(= i20x4y2 true) -(= i2x2y2 true) -(= i22x0y2 true) -(= i19x0y4 false) -(= i9x3y5 true) -(= i24x1y4 true) -(= i21x5y2 false) -(= i5x3y1 false) -(= i20x4y6 false) -(= i30x6y2 false) -(= i18x2y0 false) -(= i31x4y6 false) -(= i17x4y6 false) -(= i27x2y4 true) -(= i2x6y4 true) -(= i26x0y2 false) -(= i30x1y3 false) -(= i14x3y5 true) -(= i28x2y3 false) -(= i31x0y2 false) -(= i28x2y4 false) -(= i12x2y6 false) -(= i4x3y4 true) -(= i31x2y2 false) -(= i7x6y4 false) -(= i8x3y2 true) -(= i11x6y2 true) -(= i17x4y1 false) -(= i29x1y2 false) -(= i12x4y5 false) -(= i27x4y6 false) -(= i22x4y0 false) -(= i2x2y0 true) -(= i9x2y4 false) -(= i3x3y6 true) -(= i11x3y6 true) -(= i11x6y3 true) -(= i9x2y1 false) -(= i12x2y5 false) -(= i23x4y5 false) -(= i27x5y2 false) -(= i23x3y6 false) -(= i31x4y0 false) -(= i8x0y3 true) -(= i23x2y0 false) -(= i28x0y2 false) -(= i20x1y4 true) -(= i0x4y5 true) -(= i6x3y1 false) -(= i12x5y2 true) -(= i12x4y6 true) -(= i18x3y6 false) -(= i3x4y2 false) -(= i2x6y3 true) -(= i5x6y4 true) -(= i21x6y2 false) -(= i1x3y3 true) -(= i16x0y2 true) -(= i11x4y5 false) -(= i26x6y4 false) -(= i31x0y4 false) -(= i20x5y3 false) -(= i25x0y2 false) -(= i31x0y3 false) -(= i10x3y3 false) -(= i10x2y3 true) -(= i27x2y6 true) -(= i11x5y3 true) -(= i2x4y4 true) -(= i16x3y2 true) -(= i19x5y2 false) -(= i1x3y2 true) -(= i21x3y4 false) -(= i10x3y4 true) -(= i21x2y6 true) -(= i30x2y4 false) -(= i28x6y3 false) -(= i27x3y1 false) -(= i12x4y4 false) -(= i22x2y0 false) -(= i15x6y2 false) -(= i29x2y1 false) -(= i6x3y0 true) -(= i11x2y1 false) -(= i23x2y3 false) -(= i10x4y6 true) -(= i18x2y1 false) -(= i10x5y2 true) -(= i16x2y2 true) -(= i2x2y5 true) -(= i7x4y6 true) -(= i25x3y0 false) -(= i17x3y2 true) -(= i31x1y2 false) -(= i22x4y2 true) -(= i26x5y4 false) -(= i24x5y2 false) -(= i0x6y4 true) -(= i17x3y4 false) -(= i29x2y3 false) -(= i21x1y3 true) -(= i23x1y2 true) -(= i21x1y4 true) -(= i5x2y4 true) -(= i25x6y3 false) -(= i11x1y4 false) -(= i20x0y3 true) -(= i16x5y4 false) -(= i28x2y0 false) -(= i5x6y2 true) -(= i15x5y3 true) -(= i31x6y3 false) -(= i1x5y2 true) -(= i17x3y6 false) -(= i18x5y4 false) -(= i13x5y4 true) -(= i16x4y3 true) -(= i6x2y0 true) -(= i25x2y3 true) -(= i19x4y4 false) -(= i3x0y3 true) -(= i30x3y4 true) -(= i4x4y2 true) -(= i18x5y2 false) -(= i21x2y0 false) -(= i29x5y3 false) -(= i11x0y4 true) -(= i31x3y3 true) -(= i7x2y0 true) -(= i20x2y1 true) -(= i0x5y2 true) -(= i14x0y2 true) -(= i19x1y3 true) -(= i11x0y3 true) -(= i20x1y2 true) -(= i25x1y3 true) -(= i30x3y2 false) -(= i16x3y6 false) -(= i4x6y3 true) -(= i8x3y4 false) -(= i31x2y0 false) -(= i20x3y0 false) -(= i29x4y1 false) -(= i0x4y1 true) -(= i14x4y4 false) -(= i0x1y2 true) -(= i2x2y6 true) -(= i26x2y4 true) -(= i23x3y0 false) -(= i14x6y3 false) -(= i16x2y3 true) -(= i19x4y2 true) -(= i31x4y1 false) -(= i20x3y4 false) -(= i31x1y3 false) -(= i22x6y2 false) -(= i25x6y4 false) -(= i17x1y4 false) -(= i30x4y4 false) -(= i9x0y3 true) -(= i0x3y4 true) -(= i20x0y2 true) -(= i23x3y1 false) -(= i3x5y3 false) -(= i26x1y2 false) -(= i11x3y1 false) -(= i9x2y6 true) -(= i14x0y4 false) -(= i14x1y2 true) -(= i20x3y6 false) -(= i14x3y1 false) -(= i9x4y3 true) -(= i27x3y4 false) -(= i27x2y2 false) -(= i15x6y4 false) -(= i12x3y0 false) -(= i12x6y4 false) -(= i26x6y2 false) -(= i17x5y3 false) -(= i23x3y2 false) -(= i12x0y2 true) -(= i18x5y3 false) -(= i8x3y3 false) -(= i2x3y0 true) -(= i15x6y3 false) -(= i0x0y4 true) -(= i23x6y4 false) -(= i4x3y2 true) -(= i4x5y3 false) -(= i9x2y2 true) -(= i30x1y4 false) -(= i28x3y2 false) -(= i0x6y3 true) -(= i7x5y4 false) -(= i21x4y1 true) -(= i8x3y0 true) -(= i15x3y2 true) -(= i27x4y0 false) -(= i15x4y6 true) -(= i13x1y2 true) -(= i12x2y3 true) - diff --git a/a2/src/4/4.model.bak b/a2/src/4/4.model.bak new file mode 100644 index 0000000..3b52ae7 --- /dev/null +++ b/a2/src/4/4.model.bak @@ -0,0 +1,1059 @@ +sat + +(= i1x2y0 true) +(= i4x2y1 false) +(= i1x2y3 true) +(= i11x2y5 false) +(= i31x6y2 false) +(= i26x0y3 true) +(= i10x3y6 true) +(= i13x3y5 true) +(= i20x0y4 false) +(= i30x2y2 false) +(= i6x2y3 true) +(= i6x5y3 true) +(= i0x4y0 true) +(= i17x2y0 false) +(= i20x3y1 false) +(= i24x5y4 false) +(= i16x4y6 false) +(= i26x0y4 false) +(= i26x2y5 false) +(= i14x2y6 false) +(= i29x1y4 true) +(= i1x0y4 true) +(= i21x3y3 false) +(= i31x4y2 false) +(= i18x6y3 false) +(= i3x1y2 true) +(= i4x3y6 true) +(= i9x1y3 true) +(= i16x6y4 false) +(= i18x6y4 false) +(= i19x1y4 true) +(= i14x3y0 false) +(= i9x3y3 false) +(= i3x5y4 true) +(= i21x4y5 false) +(= i14x4y5 false) +(= i30x5y2 false) +(= i22x4y6 false) +(= i6x0y3 true) +(= i18x2y5 false) +(= i27x1y2 false) +(= i26x2y1 false) +(= i24x4y6 false) +(= i31x4y4 false) +(= i19x5y3 false) +(= i15x1y4 false) +(= i9x3y6 true) +(= i0x3y1 true) +(= i14x6y2 false) +(= i28x0y3 false) +(= i0x6y2 true) +(= i9x5y3 true) +(= i13x0y4 true) +(= i11x1y3 true) +(= i7x3y3 false) +(= i21x2y4 false) +(= i15x5y4 false) +(= i27x4y2 false) +(= i6x0y2 true) +(= i14x3y4 false) +(= i9x0y4 true) +(= i20x6y4 false) +(= i7x1y4 true) +(= i21x1y2 true) +(= i24x4y5 false) +(= i30x4y5 false) +(= i31x1y4 false) +(= i8x4y1 false) +(= i1x3y5 true) +(= i3x2y6 true) +(= i13x1y4 true) +(= i2x6y2 true) +(= i9x4y1 false) +(= i29x0y2 false) +(= i15x0y4 false) +(= i28x5y2 false) +(= i24x3y6 false) +(= i18x3y1 false) +(= i19x4y6 false) +(= i22x3y1 false) +(= i19x4y1 false) +(= i13x2y0 false) +(= i27x3y3 false) +(= i12x3y5 true) +(= i16x2y0 false) +(= i10x4y0 false) +(= i27x2y0 false) +(= i11x3y4 true) +(= i9x3y0 true) +(= i2x3y6 true) +(= i12x6y2 true) +(= i18x2y6 true) +(= i23x3y4 false) +(= i13x0y2 true) +(= i31x2y4 false) +(= i13x3y6 true) +(= i2x0y4 true) +(= i8x4y6 true) +(= i17x5y4 true) +(= i18x3y2 true) +(= i6x1y2 true) +(= i16x1y3 true) +(= i18x3y3 false) +(= i27x0y4 false) +(= i6x2y5 true) +(= i24x3y0 false) +(= i9x3y1 false) +(= i11x5y4 true) +(= i3x2y3 true) +(= i15x0y2 true) +(= i27x3y2 false) +(= i12x6y3 true) +(= i5x0y2 true) +(= i29x0y3 false) +(= i30x4y6 false) +(= i13x3y3 false) +(= i28x4y5 false) +(= i31x4y3 false) +(= i2x4y5 true) +(= i8x6y4 false) +(= i13x3y1 false) +(= i10x4y1 false) +(= i17x2y1 false) +(= i26x3y2 false) +(= i30x4y0 false) +(= i19x6y3 false) +(= i24x2y1 false) +(= i12x1y4 true) +(= i29x3y6 false) +(= i23x0y3 true) +(= i6x4y3 true) +(= i15x3y5 true) +(= i23x0y4 false) +(= i29x6y2 false) +(= i21x4y4 false) +(= i14x4y3 true) +(= i29x3y0 false) +(= i24x6y3 false) +(= i25x3y3 false) +(= i5x2y2 true) +(= i30x5y4 false) +(= i16x0y4 false) +(= i2x5y3 false) +(= i3x1y3 true) +(= i12x2y0 false) +(= i16x2y5 false) +(= i25x2y6 true) +(= i7x0y3 true) +(= i10x3y2 true) +(= i12x3y1 false) +(= i26x6y3 false) +(= i27x6y3 false) +(= i6x1y4 true) +(= i20x3y3 false) +(= i27x6y4 false) +(= i29x2y6 false) +(= i3x6y3 true) +(= i24x6y2 false) +(= i1x5y4 true) +(= i27x5y4 false) +(= i10x2y4 true) +(= i30x3y6 false) +(= i26x2y3 false) +(= i14x2y3 true) +(= i28x3y5 true) +(= i5x0y4 true) +(= i24x1y2 true) +(= i2x1y3 true) +(= i4x1y3 true) +(= i7x3y0 true) +(= i15x3y4 false) +(= i25x2y5 false) +(= i12x3y2 true) +(= i22x6y4 false) +(= i14x4y6 true) +(= i14x2y1 false) +(= i22x4y1 false) +(= i24x0y4 false) +(= i26x3y5 true) +(= i4x1y4 true) +(= i23x5y2 false) +(= i30x2y6 false) +(= i16x4y4 true) +(= i25x2y2 true) +(= i0x4y3 true) +(= i6x4y5 false) +(= i20x3y2 true) +(= i30x6y3 false) +(= i20x2y0 false) +(= i29x3y5 true) +(= i12x4y3 true) +(= i22x2y5 false) +(= i12x5y3 true) +(= i28x3y3 false) +(= i23x4y1 false) +(= i24x5y3 false) +(= i20x3y5 true) +(= i8x2y0 true) +(= i17x3y0 false) +(= i9x6y4 false) +(= i2x4y6 true) +(= i29x0y4 false) +(= i13x0y3 true) +(= i8x2y2 true) +(= i14x2y5 false) +(= i17x2y3 true) +(= i11x3y0 false) +(= i24x4y1 false) +(= i14x4y0 true) +(= i27x4y4 false) +(= i4x5y4 true) +(= i23x3y3 false) +(= i9x1y2 true) +(= i3x6y2 true) +(= i30x0y2 false) +(= i3x2y1 false) +(= i11x4y4 false) +(= i6x2y2 true) +(= i15x2y4 true) +(= i23x4y4 false) +(= i26x1y3 true) +(= i4x0y3 true) +(= i28x0y4 false) +(= i29x6y3 false) +(= i2x4y0 true) +(= i0x3y0 true) +(= i14x3y3 false) +(= i30x4y1 false) +(= i11x6y4 false) +(= i0x3y6 true) +(= i12x1y3 true) +(= i8x1y3 true) +(= i28x2y2 false) +(= i4x2y5 true) +(= i26x1y4 true) +(= i6x4y6 true) +(= i21x0y3 true) +(= i21x4y3 false) +(= i26x4y0 false) +(= i24x3y3 false) +(= i18x4y1 false) +(= i21x3y0 false) +(= i25x2y1 false) +(= i26x3y6 false) +(= i27x1y4 true) +(= i27x4y5 false) +(= i28x2y6 true) +(= i27x3y6 false) +(= i19x2y6 true) +(= i1x2y1 true) +(= i0x0y3 true) +(= i25x4y6 false) +(= i4x1y2 true) +(= i0x2y0 true) +(= i17x6y3 false) +(= i11x5y2 true) +(= i7x6y3 true) +(= i12x3y3 false) +(= i9x0y2 true) +(= i21x2y2 false) +(= i4x2y3 true) +(= i16x3y1 false) +(= i21x3y1 false) +(= i24x4y2 false) +(= i4x0y4 true) +(= i7x3y5 true) +(= i11x4y3 true) +(= i9x2y3 true) +(= i20x2y6 true) +(= i18x4y5 false) +(= i2x0y2 true) +(= i13x4y0 true) +(= i25x3y6 false) +(= i27x3y5 true) +(= i4x3y3 true) +(= i31x4y5 false) +(= i10x0y2 true) +(= i20x2y5 false) +(= i9x4y6 true) +(= i1x3y1 true) +(= i28x1y2 false) +(= i28x6y2 false) +(= i20x6y2 false) +(= i5x2y5 true) +(= i1x0y2 true) +(= i1x4y5 true) +(= i1x1y3 true) +(= i6x0y4 true) +(= i14x5y2 true) +(= i9x6y2 true) +(= i19x0y3 true) +(= i21x3y2 true) +(= i26x4y2 false) +(= i24x1y3 true) +(= i20x4y1 false) +(= i5x3y6 true) +(= i23x1y4 true) +(= i1x6y2 true) +(= i23x5y3 false) +(= i12x2y1 false) +(= i2x0y3 true) +(= i18x4y6 false) +(= i7x4y0 false) +(= i1x1y2 true) +(= i0x2y1 true) +(= i1x5y3 false) +(= i1x3y0 true) +(= i8x4y0 false) +(= i10x5y4 true) +(= i4x0y2 true) +(= i26x3y3 false) +(= i0x4y6 true) +(= i7x6y2 true) +(= i17x1y3 true) +(= i13x4y4 false) +(= i3x4y1 true) +(= i5x3y4 true) +(= i21x3y5 true) +(= i28x4y0 false) +(= i22x3y5 true) +(= i14x3y6 true) +(= i2x3y5 true) +(= i29x4y6 false) +(= i12x2y2 true) +(= i30x3y3 false) +(= i17x5y2 false) +(= i4x3y5 true) +(= i11x3y3 false) +(= i30x3y5 true) +(= i14x5y4 true) +(= i8x5y2 true) +(= i25x4y0 false) +(= i9x4y4 false) +(= i4x3y0 true) +(= i3x4y3 true) +(= i11x2y6 false) +(= i18x3y5 true) +(= i12x4y0 true) +(= i11x3y5 true) +(= i28x4y3 false) +(= i14x3y2 true) +(= i16x5y3 true) +(= i6x5y4 true) +(= i2x3y4 true) +(= i19x5y4 false) +(= i1x6y4 true) +(= i15x5y2 true) +(= i1x3y4 true) +(= i3x2y5 true) +(= i20x5y4 false) +(= i23x0y2 true) +(= i23x2y5 false) +(= i3x4y6 true) +(= i6x4y4 false) +(= i7x2y1 false) +(= i26x4y5 false) +(= i25x4y1 false) +(= i10x2y2 true) +(= i23x2y1 true) +(= i9x6y3 true) +(= i8x3y1 false) +(= i13x1y3 true) +(= i14x2y0 false) +(= i7x4y5 false) +(= i15x1y2 true) +(= i21x2y1 true) +(= i1x2y6 true) +(= i17x2y6 true) +(= i12x1y2 true) +(= i22x1y2 true) +(= i12x5y4 true) +(= i1x6y3 true) +(= i25x2y4 false) +(= i25x4y5 false) +(= i7x3y4 true) +(= i10x3y1 false) +(= i25x4y2 false) +(= i18x0y4 false) +(= i26x5y3 false) +(= i11x2y4 true) +(= i10x2y1 false) +(= i18x2y3 true) +(= i24x2y4 false) +(= i29x2y5 false) +(= i28x2y5 true) +(= i11x4y2 true) +(= i7x3y2 true) +(= i16x4y5 false) +(= i27x0y3 false) +(= i16x6y3 false) +(= i19x3y2 true) +(= i20x5y2 false) +(= i12x3y6 true) +(= i22x3y6 false) +(= i27x2y1 false) +(= i13x3y4 false) +(= i24x3y1 false) +(= i10x6y2 true) +(= i0x3y5 true) +(= i21x5y4 false) +(= i17x0y4 false) +(= i7x0y4 true) +(= i8x6y2 true) +(= i10x1y3 true) +(= i11x3y2 true) +(= i24x4y3 false) +(= i13x4y5 false) +(= i13x6y2 false) +(= i25x5y3 false) +(= i13x5y2 true) +(= i13x6y4 true) +(= i15x2y2 true) +(= i31x2y6 false) +(= i25x1y2 false) +(= i18x0y3 true) +(= i29x2y4 true) +(= i0x2y5 true) +(= i15x4y5 false) +(= i16x2y1 false) +(= i29x4y2 false) +(= i30x3y1 false) +(= i28x5y3 false) +(= i13x4y1 false) +(= i13x4y3 true) +(= i22x5y2 false) +(= i14x0y3 true) +(= i20x6y3 false) +(= i7x2y2 true) +(= i22x2y6 true) +(= i18x4y2 true) +(= i10x4y3 true) +(= i24x3y2 false) +(= i16x4y2 true) +(= i20x4y5 false) +(= i24x2y6 true) +(= i17x0y3 true) +(= i26x2y2 false) +(= i31x3y2 false) +(= i23x2y4 false) +(= i18x0y2 true) +(= i24x2y0 false) +(= i5x2y6 true) +(= i25x1y4 true) +(= i29x3y3 false) +(= i13x5y3 true) +(= i17x1y2 true) +(= i27x2y5 false) +(= i22x5y4 false) +(= i8x2y6 true) +(= i30x2y5 false) +(= i6x6y2 true) +(= i28x4y6 false) +(= i3x6y4 true) +(= i29x2y2 false) +(= i22x5y3 false) +(= i26x3y4 false) +(= i11x0y2 true) +(= i6x3y2 true) +(= i11x2y2 true) +(= i0x3y3 false) +(= i1x4y1 true) +(= i11x4y0 true) +(= i12x0y4 true) +(= i10x2y6 false) +(= i28x6y4 false) +(= i17x3y3 false) +(= i20x2y4 false) +(= i4x4y5 true) +(= i5x1y3 true) +(= i0x2y4 true) +(= i15x2y1 false) +(= i26x5y2 false) +(= i25x3y4 false) +(= i3x1y4 true) +(= i26x3y1 false) +(= i8x6y3 true) +(= i19x0y2 true) +(= i11x4y1 false) +(= i19x3y4 false) +(= i28x4y2 false) +(= i2x5y4 true) +(= i23x6y3 false) +(= i21x4y6 false) +(= i10x4y2 true) +(= i26x3y0 false) +(= i6x3y4 true) +(= i25x3y5 true) +(= i17x4y0 true) +(= i27x2y3 true) +(= i29x5y2 false) +(= i12x2y4 false) +(= i0x2y3 true) +(= i24x4y0 false) +(= i13x4y6 true) +(= i31x2y5 false) +(= i30x2y3 false) +(= i4x4y3 true) +(= i14x5y3 true) +(= i7x3y1 false) +(= i17x4y2 true) +(= i22x2y1 true) +(= i0x0y2 true) +(= i11x4y6 true) +(= i7x0y2 true) +(= i4x2y6 true) +(= i22x3y0 false) +(= i9x4y0 false) +(= i23x6y2 false) +(= i9x2y0 true) +(= i16x6y2 false) +(= i15x2y0 false) +(= i29x2y0 false) +(= i2x3y1 true) +(= i5x4y3 false) +(= i3x3y5 true) +(= i9x2y5 true) +(= i27x6y2 false) +(= i22x6y3 false) +(= i1x1y4 true) +(= i23x1y3 true) +(= i5x5y3 true) +(= i17x4y5 false) +(= i17x0y2 true) +(= i18x3y0 false) +(= i6x4y2 true) +(= i24x0y2 true) +(= i0x2y2 true) +(= i7x3y6 true) +(= i20x2y3 false) +(= i31x5y2 false) +(= i22x3y4 false) +(= i1x2y4 true) +(= i16x4y0 true) +(= i19x6y4 false) +(= i8x4y4 false) +(= i19x3y0 false) +(= i30x6y4 false) +(= i22x0y3 true) +(= i4x4y1 false) +(= i29x3y2 false) +(= i8x5y4 true) +(= i5x1y4 true) +(= i29x1y3 false) +(= i7x2y5 true) +(= i10x0y4 true) +(= i5x2y1 false) +(= i8x1y4 true) +(= i13x2y6 false) +(= i14x2y4 true) +(= i22x3y2 true) +(= i22x4y3 false) +(= i8x4y5 false) +(= i24x2y3 true) +(= i7x4y3 true) +(= i7x4y4 true) +(= i5x3y3 false) +(= i28x4y4 false) +(= i3x5y2 true) +(= i30x0y3 false) +(= i10x1y2 true) +(= i8x5y3 true) +(= i0x4y4 true) +(= i3x4y0 true) +(= i31x2y3 false) +(= i18x4y4 false) +(= i6x2y6 true) +(= i28x3y4 false) +(= i16x3y5 true) +(= i19x3y1 false) +(= i22x3y3 false) +(= i24x2y2 false) +(= i24x3y5 true) +(= i5x4y0 false) +(= i12x4y1 false) +(= i17x2y2 true) +(= i28x2y1 false) +(= i16x2y4 true) +(= i24x4y4 false) +(= i6x6y3 true) +(= i8x2y3 true) +(= i3x3y4 true) +(= i22x4y4 false) +(= i1x2y2 true) +(= i5x0y3 true) +(= i8x4y3 true) +(= i20x1y3 true) +(= i21x6y3 false) +(= i5x4y1 false) +(= i8x0y2 true) +(= i19x2y1 false) +(= i21x4y0 true) +(= i23x5y4 false) +(= i15x0y3 true) +(= i10x1y4 false) +(= i29x6y4 false) +(= i5x3y0 true) +(= i13x4y2 true) +(= i27x0y2 false) +(= i17x4y3 true) +(= i26x4y6 false) +(= i10x5y3 true) +(= i29x5y4 false) +(= i18x4y3 true) +(= i4x2y4 true) +(= i1x4y0 true) +(= i10x2y5 false) +(= i25x0y4 false) +(= i5x4y2 true) +(= i30x4y3 false) +(= i2x2y4 true) +(= i25x3y1 false) +(= i3x3y1 false) +(= i12x3y4 false) +(= i15x3y1 false) +(= i2x1y2 true) +(= i22x4y5 false) +(= i17x4y4 true) +(= i6x4y0 false) +(= i17x6y2 false) +(= i18x6y2 false) +(= i5x3y2 true) +(= i7x2y6 true) +(= i21x6y4 false) +(= i25x6y2 false) +(= i2x4y2 false) +(= i31x5y4 false) +(= i3x3y3 true) +(= i14x4y2 true) +(= i19x6y2 false) +(= i25x5y4 false) +(= i19x3y5 true) +(= i5x3y5 true) +(= i7x2y4 true) +(= i15x1y3 true) +(= i16x4y1 false) +(= i3x0y4 true) +(= i8x2y5 true) +(= i13x3y2 true) +(= i25x0y3 true) +(= i5x5y4 true) +(= i13x2y3 true) +(= i20x4y0 true) +(= i4x6y2 true) +(= i21x3y6 false) +(= i22x1y3 true) +(= i1x0y3 true) +(= i1x4y3 false) +(= i8x3y5 true) +(= i25x2y0 false) +(= i13x2y5 false) +(= i4x6y4 true) +(= i4x4y4 true) +(= i20x2y2 false) +(= i21x4y2 false) +(= i4x2y2 true) +(= i31x5y3 false) +(= i15x4y2 true) +(= i28x1y3 false) +(= i25x5y2 false) +(= i7x1y3 true) +(= i13x3y0 false) +(= i16x3y4 false) +(= i23x3y5 true) +(= i0x3y2 true) +(= i15x3y3 false) +(= i1x4y6 true) +(= i2x3y3 true) +(= i19x4y5 false) +(= i7x5y3 true) +(= i6x3y6 true) +(= i19x4y0 true) +(= i4x3y1 false) +(= i16x1y4 false) +(= i27x3y0 false) +(= i13x6y3 false) +(= i17x3y5 true) +(= i6x6y4 true) +(= i0x1y4 true) +(= i23x4y6 false) +(= i23x4y2 false) +(= i16x0y3 true) +(= i17x6y4 false) +(= i29x4y0 false) +(= i31x3y1 false) +(= i13x2y2 true) +(= i15x4y3 true) +(= i18x1y3 true) +(= i12x0y3 true) +(= i15x4y4 true) +(= i31x3y0 false) +(= i11x2y3 true) +(= i3x3y2 true) +(= i15x2y3 true) +(= i27x4y3 false) +(= i27x5y3 false) +(= i22x1y4 true) +(= i19x2y2 true) +(= i31x2y1 false) +(= i21x0y4 false) +(= i18x1y4 false) +(= i10x3y0 true) +(= i18x4y0 true) +(= i3x2y2 true) +(= i5x2y0 true) +(= i10x0y3 true) +(= i9x5y2 true) +(= i0x5y3 true) +(= i15x3y6 true) +(= i18x1y2 true) +(= i31x3y4 false) +(= i19x3y3 false) +(= i30x3y0 false) +(= i27x4y1 false) +(= i9x5y4 true) +(= i4x2y0 true) +(= i26x2y0 false) +(= i3x2y4 true) +(= i30x2y1 false) +(= i22x0y4 false) +(= i3x0y2 true) +(= i15x4y1 false) +(= i9x1y4 false) +(= i26x4y3 false) +(= i6x3y3 false) +(= i8x2y1 false) +(= i17x2y4 true) +(= i19x2y3 true) +(= i22x2y4 false) +(= i31x3y6 false) +(= i7x2y3 true) +(= i29x4y4 false) +(= i0x5y4 true) +(= i21x2y3 false) +(= i30x4y2 false) +(= i4x5y2 true) +(= i11x1y2 true) +(= i22x2y3 false) +(= i3x3y0 true) +(= i17x3y1 false) +(= i6x3y5 true) +(= i26x4y1 false) +(= i3x4y4 true) +(= i29x3y4 false) +(= i25x4y4 false) +(= i4x4y0 false) +(= i14x4y1 false) +(= i19x3y6 false) +(= i8x0y4 true) +(= i23x4y3 false) +(= i21x0y2 true) +(= i6x5y2 true) +(= i25x3y2 false) +(= i16x2y6 true) +(= i6x4y1 false) +(= i14x1y3 true) +(= i29x3y1 false) +(= i0x1y3 true) +(= i13x2y4 false) +(= i18x3y4 true) +(= i0x2y6 true) +(= i2x3y2 true) +(= i28x4y1 false) +(= i2x1y4 true) +(= i0x4y2 true) +(= i28x3y6 false) +(= i6x1y3 true) +(= i18x2y2 true) +(= i29x4y3 false) +(= i30x0y4 false) +(= i2x2y3 true) +(= i15x2y5 false) +(= i8x3y6 true) +(= i19x2y4 false) +(= i20x4y4 false) +(= i3x2y0 true) +(= i28x1y4 true) +(= i22x2y2 false) +(= i6x2y4 true) +(= i31x3y5 false) +(= i5x2y3 true) +(= i13x2y1 false) +(= i16x1y2 true) +(= i1x4y4 true) +(= i15x3y0 false) +(= i20x4y3 true) +(= i21x2y5 false) +(= i25x4y3 false) +(= i7x1y2 true) +(= i24x6y4 false) +(= i9x3y4 true) +(= i19x4y3 true) +(= i9x4y2 true) +(= i5x5y2 true) +(= i23x2y2 true) +(= i26x4y4 false) +(= i4x4y6 true) +(= i28x3y0 false) +(= i14x2y2 true) +(= i5x4y6 true) +(= i21x5y3 false) +(= i5x4y4 true) +(= i5x1y2 true) +(= i5x6y3 true) +(= i5x4y5 true) +(= i19x2y0 false) +(= i15x4y0 true) +(= i16x3y3 false) +(= i11x2y0 false) +(= i9x4y5 false) +(= i2x4y1 false) +(= i8x2y4 true) +(= i9x3y2 true) +(= i16x3y0 false) +(= i19x2y5 false) +(= i30x1y2 false) +(= i18x2y4 true) +(= i30x2y0 false) +(= i1x3y6 true) +(= i10x6y4 false) +(= i17x2y5 false) +(= i28x5y4 false) +(= i12x4y2 true) +(= i14x1y4 false) +(= i29x4y5 false) +(= i1x2y5 true) +(= i2x4y3 true) +(= i7x4y1 false) +(= i1x4y2 true) +(= i24x0y3 true) +(= i10x4y4 false) +(= i6x2y1 false) +(= i7x5y2 true) +(= i8x1y2 true) +(= i8x4y2 true) +(= i10x6y3 true) +(= i14x6y4 true) +(= i10x2y0 true) +(= i23x4y0 false) +(= i28x3y1 false) +(= i10x4y5 false) +(= i31x6y4 false) +(= i19x1y2 true) +(= i7x4y2 true) +(= i16x5y2 true) +(= i24x2y5 false) +(= i24x3y4 false) +(= i2x2y1 true) +(= i15x2y6 false) +(= i2x5y2 true) +(= i23x2y6 true) +(= i30x5y3 false) +(= i3x4y5 true) +(= i10x3y5 true) +(= i27x1y3 false) +(= i26x2y6 true) +(= i20x4y2 true) +(= i2x2y2 true) +(= i22x0y2 true) +(= i19x0y4 false) +(= i9x3y5 true) +(= i24x1y4 true) +(= i21x5y2 false) +(= i5x3y1 false) +(= i20x4y6 false) +(= i30x6y2 false) +(= i18x2y0 false) +(= i31x4y6 false) +(= i17x4y6 false) +(= i27x2y4 true) +(= i2x6y4 true) +(= i26x0y2 false) +(= i30x1y3 false) +(= i14x3y5 true) +(= i28x2y3 false) +(= i31x0y2 false) +(= i28x2y4 false) +(= i12x2y6 false) +(= i4x3y4 true) +(= i31x2y2 false) +(= i7x6y4 false) +(= i8x3y2 true) +(= i11x6y2 true) +(= i17x4y1 false) +(= i29x1y2 false) +(= i12x4y5 false) +(= i27x4y6 false) +(= i22x4y0 false) +(= i2x2y0 true) +(= i9x2y4 false) +(= i3x3y6 true) +(= i11x3y6 true) +(= i11x6y3 true) +(= i9x2y1 false) +(= i12x2y5 false) +(= i23x4y5 false) +(= i27x5y2 false) +(= i23x3y6 false) +(= i31x4y0 false) +(= i8x0y3 true) +(= i23x2y0 false) +(= i28x0y2 false) +(= i20x1y4 true) +(= i0x4y5 true) +(= i6x3y1 false) +(= i12x5y2 true) +(= i12x4y6 true) +(= i18x3y6 false) +(= i3x4y2 false) +(= i2x6y3 true) +(= i5x6y4 true) +(= i21x6y2 false) +(= i1x3y3 true) +(= i16x0y2 true) +(= i11x4y5 false) +(= i26x6y4 false) +(= i31x0y4 false) +(= i20x5y3 false) +(= i25x0y2 false) +(= i31x0y3 false) +(= i10x3y3 false) +(= i10x2y3 true) +(= i27x2y6 true) +(= i11x5y3 true) +(= i2x4y4 true) +(= i16x3y2 true) +(= i19x5y2 false) +(= i1x3y2 true) +(= i21x3y4 false) +(= i10x3y4 true) +(= i21x2y6 true) +(= i30x2y4 false) +(= i28x6y3 false) +(= i27x3y1 false) +(= i12x4y4 false) +(= i22x2y0 false) +(= i15x6y2 false) +(= i29x2y1 false) +(= i6x3y0 true) +(= i11x2y1 false) +(= i23x2y3 false) +(= i10x4y6 true) +(= i18x2y1 false) +(= i10x5y2 true) +(= i16x2y2 true) +(= i2x2y5 true) +(= i7x4y6 true) +(= i25x3y0 false) +(= i17x3y2 true) +(= i31x1y2 false) +(= i22x4y2 true) +(= i26x5y4 false) +(= i24x5y2 false) +(= i0x6y4 true) +(= i17x3y4 false) +(= i29x2y3 false) +(= i21x1y3 true) +(= i23x1y2 true) +(= i21x1y4 true) +(= i5x2y4 true) +(= i25x6y3 false) +(= i11x1y4 false) +(= i20x0y3 true) +(= i16x5y4 false) +(= i28x2y0 false) +(= i5x6y2 true) +(= i15x5y3 true) +(= i31x6y3 false) +(= i1x5y2 true) +(= i17x3y6 false) +(= i18x5y4 false) +(= i13x5y4 true) +(= i16x4y3 true) +(= i6x2y0 true) +(= i25x2y3 true) +(= i19x4y4 false) +(= i3x0y3 true) +(= i30x3y4 true) +(= i4x4y2 true) +(= i18x5y2 false) +(= i21x2y0 false) +(= i29x5y3 false) +(= i11x0y4 true) +(= i31x3y3 true) +(= i7x2y0 true) +(= i20x2y1 true) +(= i0x5y2 true) +(= i14x0y2 true) +(= i19x1y3 true) +(= i11x0y3 true) +(= i20x1y2 true) +(= i25x1y3 true) +(= i30x3y2 false) +(= i16x3y6 false) +(= i4x6y3 true) +(= i8x3y4 false) +(= i31x2y0 false) +(= i20x3y0 false) +(= i29x4y1 false) +(= i0x4y1 true) +(= i14x4y4 false) +(= i0x1y2 true) +(= i2x2y6 true) +(= i26x2y4 true) +(= i23x3y0 false) +(= i14x6y3 false) +(= i16x2y3 true) +(= i19x4y2 true) +(= i31x4y1 false) +(= i20x3y4 false) +(= i31x1y3 false) +(= i22x6y2 false) +(= i25x6y4 false) +(= i17x1y4 false) +(= i30x4y4 false) +(= i9x0y3 true) +(= i0x3y4 true) +(= i20x0y2 true) +(= i23x3y1 false) +(= i3x5y3 false) +(= i26x1y2 false) +(= i11x3y1 false) +(= i9x2y6 true) +(= i14x0y4 false) +(= i14x1y2 true) +(= i20x3y6 false) +(= i14x3y1 false) +(= i9x4y3 true) +(= i27x3y4 false) +(= i27x2y2 false) +(= i15x6y4 false) +(= i12x3y0 false) +(= i12x6y4 false) +(= i26x6y2 false) +(= i17x5y3 false) +(= i23x3y2 false) +(= i12x0y2 true) +(= i18x5y3 false) +(= i8x3y3 false) +(= i2x3y0 true) +(= i15x6y3 false) +(= i0x0y4 true) +(= i23x6y4 false) +(= i4x3y2 true) +(= i4x5y3 false) +(= i9x2y2 true) +(= i30x1y4 false) +(= i28x3y2 false) +(= i0x6y3 true) +(= i7x5y4 false) +(= i21x4y1 true) +(= i8x3y0 true) +(= i15x3y2 true) +(= i27x4y0 false) +(= i15x4y6 true) +(= i13x1y2 true) +(= i12x2y3 true) + diff --git a/a2/src/4/a4.py b/a2/src/4/a4.py index b216b3b..9c5b015 100644 --- a/a2/src/4/a4.py +++ b/a2/src/4/a4.py @@ -1,23 +1,17 @@ #!/bin/env python -#pylint: disable-msg=too-many-locals,invalid-name -"""hi""" +#pylint: disable-msg=too-many-locals,invalid-name,missing-docstring -def generate(): - """Generates the yices code for peg solitaire""" +if __name__ == '__main__': pos = [(x, y) for x in range(7) for y in range(7) if not ((x < 2 and y < 2) or # exclude topleft (x > 4 and y > 4) or # exclude bottomright (x > 4 and y < 2) or # exclude topright (x < 2 and y > 4)) # exclude bottomleft ] - ill_middles = [ - (2, 0), (4, 0), (0, 2), (0, 4), (6, 2), (6, 4), (2, 6), (4, 6)] holes = [(3, 3)] winning = (3, 3) - iterations = len(pos)-len(holes) - posp = [p for p in pos if p not in ill_middles] print """ (benchmark a1.smt :logic QF_UF @@ -39,7 +33,7 @@ def generate(): print ';Iteration {}'.format(i) print '(or' for sx, sy in pos: - for mx, my in posp: + for mx, my in pos: if mx == sx and my == sy: continue for ex, ey in pos: @@ -77,6 +71,3 @@ def generate(): for x, y in pos if (x, y) != winning) print '))' - -if __name__ == '__main__': - generate()