From 0ceec1deebde03d3e5c4d2081c5d54ce2fddd01b Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Thu, 22 Oct 2015 21:31:25 +0200 Subject: [PATCH] finished 1-3 --- ar/assignments/1.tex | 88 ++++++++--------- ar/assignments/2.tex | 139 +++++++++++++++------------ ar/assignments/3.tex | 76 +++++++++++++++ ar/assignments/4.tex | 1 + ar/assignments/a.tex | 13 ++- ar/assignments/preamble.tex | 3 +- ar/assignments/s3.png | Bin 0 -> 7129 bytes ar/assignments/src/1.model | 33 ------- ar/assignments/src/2.model | 47 --------- ar/assignments/src/4.model | 71 -------------- ar/assignments/src/a1.bash | 5 + ar/assignments/src/{1.smt => a1.smt} | 0 ar/assignments/src/a2.bash | 1 + ar/assignments/src/{2.py => a2.py} | 0 ar/assignments/src/a3.bash | 5 + ar/assignments/src/a3.py | 47 +++++++++ ar/assignments/src/a4.bash | 5 + ar/assignments/src/{4.py => a4.py} | 0 18 files changed, 272 insertions(+), 262 deletions(-) create mode 100644 ar/assignments/s3.png delete mode 100644 ar/assignments/src/1.model delete mode 100644 ar/assignments/src/2.model delete mode 100644 ar/assignments/src/4.model create mode 100644 ar/assignments/src/a1.bash rename ar/assignments/src/{1.smt => a1.smt} (100%) create mode 100644 ar/assignments/src/a2.bash rename ar/assignments/src/{2.py => a2.py} (100%) create mode 100644 ar/assignments/src/a3.bash create mode 100644 ar/assignments/src/a3.py create mode 100644 ar/assignments/src/a4.bash rename ar/assignments/src/{4.py => a4.py} (100%) diff --git a/ar/assignments/1.tex b/ar/assignments/1.tex index 317ae58..8506da9 100644 --- a/ar/assignments/1.tex +++ b/ar/assignments/1.tex @@ -22,46 +22,48 @@ delivered, and show how for that number all pallets may be divided over the six trucks. } +\newpage \subsection{Formal definition} -For every truck $t_i$ for $i\in T$ where $T=[1\ldots6]$ in combination with +For every truck $t_i$ for $i\in T$ where $T=\{1,\ldots,6\}$ in combination with every nuzzle $n$, prittle $p$, skipple $s$, crottle $c$ and dupple $d$ we -declare a variable that holds the amount of that type of building block. -We group all pallets $r$ for $r\in P$ where $P=[n,p,s,c,d]$. We also define -function $w(r)$ that defines the weight of the pallet and $n(r)$ that defines -the number of pallets needed. Then the following combination of subformulas -describes the problem. +declare a variable that holds the amount of that type of building block in that +truck. We group all pallets $r\in P$ where $P=\{n,p,s,c,d\}$. We also +define function $w(r)$ that defines the weight of the pallet and $n(r)$ that +defines the number of pallets needed. + +This leads to the following formalization where we maximize $n(p)$. \begin{align} \bigwedge^{T}_{i=1}\Biggl( - & \bigwedge_{r\in P}t_ir\geq0\\ - & \wedge \sum_{r\in P}t_ir\leq8\\ - & \wedge \left(\sum_{r\in P}t_ir*w(r)\right)\leq7800)\\ - & \wedge (t_ip=0\vee t_ic=0)\\ - & \wedge t_id\leq1\\ - & \wedge (t_i=t_1 \vee t_i=t_2 \vee t_is=0)\Biggr)\wedge\\ + & \bigwedge_{r\in P}t_{i}r\geq0\\ + & \wedge \sum_{r\in P}t_{i}r\leq8\\ + & \wedge \left(\sum_{r\in P}t_{i}r\cdot w(r)\right)\leq7800)\\ + & \wedge (t_{i}p=0\vee t_{i}c=0)\\ + & \wedge t_{i}d\leq1\\ + & \wedge (t_{i}=t_{1} \vee t_{i}=t_{2} \vee t_{i}s=0)\Biggr)\wedge\\ \bigwedge_{r\in P}\Biggl( - & r=p\vee\left(\sum^{T}_{i=1}t_ir\right)=n(r)\Biggr) + & \left(\sum^{T}_{i=1}t_{i}r\right)=n(r)\Biggr) \end{align} -All the subformulas describe a constraint from the problem description and we -can separate two groups. Subformulas going over all trucks and subformulas over -all pallets. +Every numbered subformula describes a constraint from the problem description. +We can separated the subformulas in formulas going over all trucks and formulas +going over all pallets. + \begin{itemize} \item \textbf{Trucks} \begin{enumerate} - \item Makes sure you can not have a negative number of pallets. - by stating that all pallets numbers per truck are - bigger then $0$. + \item Makes sure you can not have a negative number of pallets + in a truck by stating that the number of pallets in a + truck is not smaller then $0$. \item Makes sure you can not have more then $8$ pallets in a truck by stating that the sum of all pallets in a truck is not bigger then $8$. - \item Makes sure the weight will never go over the maximum by - stating that all the pallets times their weight in a - truck may not go over $7800$kg. + \item Makes sure the weight will never go over the maximum + weight per truck by stating that all the pallets times + their weight in a truck will not go over $7800$kg. \item Makes sure prittles and crottles are never together in a truck by stating that either the number of prittles is - zero or the number of crottles is zero. Note that they - therefore also can both be zero. + zero or the number of crottles is zero in a truck. \item Makes sure that skipples are only in the first two cooled trucks by stating that if the truck number not one or two the number of skipples is zero. @@ -71,39 +73,31 @@ all pallets. \setcounter{enumi}{6} \item Makes sure that all mandatory pallets are transported by summing over all trucks and assuring the number of the - pallets of that type is exactly $n(r)$. Note that this - should hold or that the current pallet is a prittle - pallet since we do not have a limit on prittles. + pallets of that type is exactly $n(r)$. \end{enumerate} \end{itemize} \subsection{SMT format solution} The formula is easily convertable to SMT format and is listed in -Listing~\ref{listing:a1.smt}. A final condition is added with a special -variable named \texttt{} that we increment to find the maximum amount of -prittles transportable. When running the script in Listing~\ref{listing:1bash} -the loop terminates after it echoed $20$ meaning that the maximum number of -prittles is 20. This iterative solution takes less then $0.1$ seconds to -calculate. +Listing~\ref{listing:a1.smt}. The maximization is done by incrementing a +special variable called \texttt{} which is an instantiation of $n(p)$. +When the iteration yields unsat we know that the current number minus one is +the maximum amount of prittles the trucks can carry. The maximization is done +with a bash script shown in Listing~\ref{listing:1.bash}. -\begin{lstlisting}[language=bash, - caption={Iteratively find the largest solution},label={listing:1bash}] -i=1 -while [ $(sed "s//$i/g" a1.smt | yices-smt) = "sat" ] -do - echo $((++i)); -done -\end{lstlisting} +\lstinputlisting[language=bash, + caption={Iteratively find the largest solution for problem 1}, + label={listing:1.bash}]{src/a1.bash} \subsection{Solution} -The iterative solution terminates with $i=18$ so the maximum number of prittles -to be deliverd is $18$. When we rerun the solution with $18$ prittles and the -\texttt{-m} flag we can see the solution as in Table~\ref{tab:s1}. +The bash script finds and shows the maximal solution of $18$ prittles. Finding +this solution takes less then $0.12$ seconds and is shown in Table~\ref{tab:s1}. \begin{table}[H] \begin{tabular}{|l|lllll|l|l|} \hline - Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & Weight & Pallets\\ + Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & + Weight & Pallets\\ \hline 1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\ 2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\ @@ -115,6 +109,6 @@ to be deliverd is $18$. When we rerun the solution with $18$ prittles and the total & 4 & 18 & 8 & 10 & 5 & &\\ \hline \end{tabular} - \caption{Solution table for problem 1} - \label{tab:s1} + \caption{Solution visualization for problem 1} +\label{tab:s1} \end{table} diff --git a/ar/assignments/2.tex b/ar/assignments/2.tex index f4789d8..7fd4047 100644 --- a/ar/assignments/2.tex +++ b/ar/assignments/2.tex @@ -6,97 +6,116 @@ components satisfying the following constraints: \begin{itemize} \item The width of the chip is 29 and the height is 22. \item All power components have width 4 and height 2. - \item The sizes of the eight regular components are $9\times7$, $12\times6,$ - $10\times7,$ $18\times5,$ $20\times4,$ $10\times6,$ $8\times6$ and - $10\times8$ respectively. + \item The sizes of the eight regular components are $9\times7$, + $12\times6,$ $10\times7,$ $18\times5,$ $20\times4,$ + $10\times6,$ $8\times6$ and $10\times8$ respectively. \item All components may be turned 90, but may not overlap. \item In order to get power, all regular components should directly be - connected to a power component, that is, an edge of the component should - have at least one point in common with an edge of the power component. - \item Due to limits on heat production the power components should be not too - close: their centres should differ at least $17$ in either the $x$ - direction or the $y$ direction (or both). + connected to a power component, that is, an edge of the + component should have at least one point in common with an edge + of the power component. + \item Due to limits on heat production the power components should be + not too close: their centres should differ at least $17$ in + either the $x$ direction or the $y$ direction (or both). \end{itemize} } +\newpage \subsection{Formal definition} -For every component $c$ for $i\in PC\cup RC$ where $PC=[01,02,03]$ and -$RC=[04,05,06,07,08,09,10,11]$ we define a width, a height variable, an x and a -y variable. $c_iw$, $c_ih$, $c_ix$ and $c_iy$. Although we call the height and -width they represent just the sides since the components can be rotated. To -represent this we introduce functions $h(c)$ and $w(c)$ that return the -specified width and height. +For every component $c_{i}$ for $i\in PC\cup RC$ where $PC=\{1,\ldots,3\}$ and +$RC=\{4,\ldots,11\}$ we define a width, a height, an $x$ and a $y$ variables +$c_{i}w$, $c_{i}h$, $c_{i}x$ and $c_{i}y$. $c_ih$ does not necessarily have the +specified height of the components since the components may be rotated. For the +specified width and height we introduce the functions $h(c)$ and $w(c)$ that +return the specified width and height. + +This leads to the following formalization. \begin{align} \bigwedge_{i\in PC\cup RC}\Biggl( - & (c_ih=h(i)\vee c_ih=w(i))\wedge(c_iw=w(i)\vee c_iw=h(i))\\ - & \wedge 29-c_iw\geq c_ix>0\wedge 22-c_ih\geq c_iy>0\\ - & \wedge \bigwedge_{j\in PC\cup RC}\Bigl(\\ - \nonumber & \qquad\qquad\qquad j\geq i\\ - \nonumber & \qquad\qquad\qquad \vee c_ix>c_jx+c_jw\\ - \nonumber & \qquad\qquad\qquad \vee c_ix+c_jwc_jy+c_jh\\ - \nonumber & \qquad\qquad\qquad \vee c_iy+c_jh0\wedge 22-c_{i}h\geq c_{i}y>0\\ + & \wedge \bigwedge_{j\in PC\cup RC}\Bigl(j\geq i\\ + \nonumber & \qquad\qquad\qquad \vee c_{i}x>c_{j}x+c_{j}w\\ + \nonumber & \qquad\qquad\qquad \vee c_{i}x+c_{j}wc_{j}y+c_{j}h\\ + \nonumber & \qquad\qquad\qquad + \vee c_{i}y+c_{j}h17\\ - \nonumber & \vee c_jx+\frac{c_jw}{2}-c_ix+\frac{c_iw}{2}>17\\ - \nonumber & \vee c_iy+\frac{c_ih}{2}-c_jy+\frac{c_jh}{2}>17\\ - \nonumber & \vee c_jy+\frac{c_jh}{2}-c_iy+\frac{c_ih}{2}>17\Biggr)\wedge\\ + \nonumber & \vee c_{i}x+\nicefrac{c_{i}w}{2}- + c_{j}x+\nicefrac{c_{j}w}{2}>17\\ + \nonumber & \vee c_{j}x+\nicefrac{c_{j}w}{2}- + c_{i}x+\nicefrac{c_{i}w}{2}>17\\ + \nonumber & \vee c_{i}y+\nicefrac{c_{i}h}{2}- + c_{j}y+\nicefrac{c_{j}h}{2}>17\\ + \nonumber & \vee c_{j}y+\nicefrac{c_{j}h}{2}- + c_{i}y+\nicefrac{c_{i}h}{2}>17\Biggr)\wedge\\ \bigwedge_{i\in RC}\bigvee_{j\in PC}\neg\Biggl( - & (c_ix-1>c_jx+c_jw\\ - \nonumber & \vee c_ix+1+c_jwc_jy+c_jh\\ - \nonumber & \vee c_iy+1+c_jhc_{j}x+c_{j}w\\ + \nonumber & \vee c_{i}x+1+c_{j}wc_{j}y+c_{j}h\\ + \nonumber & \vee c_{i}y+1+c_{j}h0\wedge j_{i}+ij_{k}+k\Biggr)\\ + & \wedge \bigwedge_{i\in J'}\bigwedge_{k\in J'} + i=j\vee j_{i}>j_{k}+k \vee j_{i}+iW=+m7JgmvhB%Rd{qCncd}5{oK6B zIBlMfKf!uF&U&bFy(<0CX2tCXyRLfo-9Z{+<8^-m`w5X3_=?erOeQ*F_lHI|B*SM2 zcN<>xgbTNJcEK+4wmp0or5549ZntSOTsi$A=bo33iAmCyxw^Tks%o5Cz{$gR>2GlD zRQOmtuqON z1GY=H%`CD~&^P6jXn$o2*Hqzm0ETDOC!>-r+y)Go3VDqWYznugz{jY?<30#m4%qy{ zKq=4{PvqIjKp2;s9Vey=idd21{O$G4Xfd)J_%-sduWkXtBvu6F*QIx4nqSYKVzH2c z7L-?q!;0uXJbPcjXO$gV(XD$brpp~`wjSJEdWeWqM+m4thUB{wLb7$JPpWIqkG;9A z2GE4YLHSZO{(}q7HR>T7-+8u5Q-9X5=y4*-WPDago>;it$1=N!hM5dg1dXq#d9>4I z6&-#0qqVfagXdlMpz%eXN;~b7`PxW^O;+qB2C2FCS(v*lmNu2gaP!+Y=W_O3WarG` zyQ&iDI-DKyu5Ax+NMhm<9vYU28KHOYLOalzz2n#HVyX>J8r!aLF8?74h z05^MPE9fCo12II+alW|!r;c`^=!{L+IPy!y!Px~<|cV8w|4=SCCTeCluonS3%}5m(2L~?%jF$tdYM&Ib~J22 z#lvX6BT1^D*%O!F%NU9F*+vHn1YZd5eqo*eU>YrKd@WN4nnS2xoxpW2iHQ8d3~D+cF^_g+2~qM@{WFLJwT= z6cIlmI8aCj_$CLULVfL4g0)WBk2|gXXrw6c4*!-Quk5a~SKD~* zCTy0`dodmZ-B#SA%I@*prr<6G#qS{HeM0-8g$UQykMHV*SA1xgp-2{qoAxAF47{6=(?ASalhPnmU*}E!^7E1G^%lnlIPvpIVfb$!@ zRjfH0YomHK9VqHs=vc5AcLTn0))o;R#jYG}dQRQe(Lv;M)=c=(v%COq)N&$iDx>VK zRuj)`f>`BnF-=aRY}NZ`aEY|uLB3@j{4Xw`*wJPaB0HZoq+|lOw4_YQ*@&C8xu0m| z&j|i^ok3YbjuO*&LeOpv^Nl9u}>=#VG>Q#OT^L^2wQ@tJ$ z`Fs||mjK)r#r*^1asnVI&{8>?Iv$L7iK{F3!~+hw{QVMkW8gu|r+S}Y=XP%OH;#w5MD)0RGB2~FM_4YXm zDI1eoQ)6-RotFWs+1j#r5Ln-82G98fQI-wjW=M}LPS!n<-?W*y_-$*JPz78~wK?GP za%2<=_N_H~esSt1*{}8!!FMc@-Ul@|fFF6$F|ctqCV1r)8$@dtNCba{5_8lBs@ibm zONus3lsL#!U*>6jDB|mc+)BPUB&v>kf;g)v)E$fYJ97H{_2>mw{*BKA;I;hpDk39A zCIl-7098Z%X3SIwa8ctUZR8>`Jj=mnxzzemt3hDlh1iBm>%QnF50jTU3S~~~B>;DV zCJa)i*YIg>MBtpBHj({~<0+oh6RVv?@i8`um+8vME&dW{8kBZEv|kRctM=0M60=9| zr{7V2xd-#<4VRF9?km-vd3VX}^+k!;yub@39M{aDr_M>0=-0>}8KD^;MZXMdny02O z$SwVP^78~T=5njA4%zp}emqY-;F3U!23e;UV!>_zPxC$mfoq zY#h3+^Td>~%Sn{%m+lB-=N1$rqof|jwal17%K>Z;4te)e&@Kn^_b~LzADv(V94iMr z+nb?yv8p3EI`WEQP=m+X$a&%zo7#pa88bUUw~G*{TI1YsBZHZzN{a? zZ%puntkRvU)W4Waoj);5+gq1*cQ4W}mT9(no6{yalDb&y;f!a-+-Pj3UT=96l64{c zr3RW>6*rEEy7}&@kcQ5U_emP^8pOd6yx6(9$rHlM3I}H8e&)m!5Nd_Rtal5Hmp(Hh zhZig86bHehZpW3+qbej02*7#9LQgO-}T_I{J2Nj?i9QuCTlT$r*#Yu`k1 zFW>@n^d|8Ts9e{lqAof2(g}B+Ty?K&9aEz975_X5A3CyPnQlDlhz1`Qlk_E+7#=Dn zP3tBJR%jh;8l9Hs8F8ieuc~Pmp1^CSJD;SiD>uY`EdDYXo1*i(P%jZttB1}|fJLrY z95MYmEBZWE4m)#D=Vd>oc>0HKRKG@Ne_6)U$|z9PfP&oY^wrBwjIm;RS>5+lckR2Z;?0j3ko6!!QrFiy8xS)IT587hd2wmSAa(sgT z*6k+|`#`rvyc@x$X{p8TOi|9Q8WRsyO=v4r6R@V(A4QcZ{Rtln_{T&{C{s-LYXIiR7oYy8Uhb59lLk39JuV5W)`k!EN?DC#K zhKs*C7uZ{{S*+TkrURI|!@R^{H{&xx^ ze?@tbJSZOxwV|KI{;RIDu%i&*FkYx~x)B*<8=o zSI}`fuo)%`pFV4#fog0hdFELPq&Ab-0QwHkSB_d9o9XkoR8;ws| zq};yR6|X(6`C&B#&g4tnIC-{hJ4%)|T&&$o$D`ldRINF%@Vi}lJo|xfr>@u;SqL${ zMRg^!ModlvYpxb!-v>{ATj^xmEx#MeZZr`XP}=h*VVUC7_$>|&K8VwsqK1;Avs~>7 z*75aq;e+ht(dYFmFtU5|TwwhLrN#pb$uOBuqAGbyA0t7vzS3hv5${5`sCx>AsTqzr z1YR1_rclC*oni(>K9<5SE@?^JIJBOn0ZZGL|8!SH~2oP=bkTh_a;W68ihMLc?M z!(5x!!+u!t(`&O_p0nliHj?t(fZZg%jj3gM_g745#p3m@3k_Y$aT?1{#UIiNkd+7k zORv+N$|kozLinEs4x7@AcK1$*YJYTtBZPOpAG3*!m?UfPXzz5VFDl-~#DG(N?XiTl#8sOopYETgCUK&8 z8jbdn#q)O=Wv%s%CPGZ9>vkH-mvQJ77`+;mHq)QGZ?CJpULV<5bD8ymRPwwM;U~ph zY3Q{J|?)L{bQ|nPBqbv7KcAK2%U+F?) z4v{Z}dVReSM<;<;j7~o{#4-}YWQz)ZN+%7R6$zSH{D6s$O0lfZo4)wtCT7zaxI*y=wR(^4sC#T0Z&#sk8H)BegtHm$ygp-|-A^_D@u!MpjT1W1rM8y~C{c{I?YWig4;m&wdWEyWXSxI{+hw8c_$0%9aN+T=z$(!~_=-U!X zUq{O^1Y4jPg}tK4F`jH9nd9#!kOp90vyu%Su-2v%KjQhfwD!Pc`0?Y%cTR^%L#mJE zhyeH$jjNzO&4z)vhP9%yzIp&WQr|II8;_n?G(@t?b$e{(s*X#g|iaMv@z)`m|wOO1j5{5_A78`s@-xD7U$q@dDf9$ zwABIeOmD3dZ!e96)+!5}R-c@A-(SZxKD=m0$5?yGFyui$`SsUCjW?YC-We#G%3?pl zy7o6;Oa6ZneeRYm%Au36C}qUci68Yqb;97iW#@RBn+Ea5f*8g>}*x-dcuV_cmsp1rS?fVden1^F0Pbhm#ry3Isjre zQy~{>aL?iK*U9fk%UJHUNo;se-c00nT2rZRTfgxZeOJ;2>X^gAS6l~eu1xBfQBl-Sl%L!;EJFyq%`(m?38QS~GF?P@v)q3JEEAW}@GzW7U>@VW}21A(bP zjd#cFPumytq?bZT_~EC+abFtSGFb?d9Y$^v0l^-i1o+{QYITQl^7pWnj=4G9eQsyn zAjdb>YjUhOl87QzT%M**iW_v~}-#docBe+_5bK7v5^xxr;DqajK4 zB;E=*=h781IjI7s#ffO5`#+tPJulcCRK7P{d&g0S80VVEn1BgJ6z_>IYWb8z9P_he+GjNm(zZCt=A3uOpV{EbP)UhCjr>QyoZG4zePuF6G&{SbKwE7S_AbCwAp(KjBNyeShrMErg#MEPscwkgk3j zH)!VK%V>Q&XP&&b#dFPIi$SJ7yGvYIt`y2Fba6#mI#J!gyvOd@lEC>K?~T&5=PixL zt2hPjYf5co<~%Pt`jzio8)Lx-q@LrC`!}uwNy0o8os{IXmUr-8@m!w$JNr1KJjBc@ zpLg86j73iwkrdlNJ;GdykFn-t8J_lQN@S}r!El(wcjwJwVcV^aN<3{Lr10!iY=1}! z@6IVL(KIJlbx7kI@RZKShyTD*#snyqFnc+&e-6DWuS7qud%|)wK&-5Vi19G5!ITAn zLOuGv#J~3QTR`*j=A^rj)j28~$fBFSY+27n`IhoTP^~__$tsU|g}G-`fMLqf3!Ayz zZu5nrXbE_^fc0i#fguErTITi@a`>B1;$UFfakt$*@?%Cxuu|}8!C7m&1`&^1tsY-9 z6FK?cAY=khAQ>w1T2_3VwIS+rI+L!xR2m(xU_lw)hEClD^l* zpS+FiJ5~6T|1j^QxfW7|Wuxj_9uRU>_?}=tgRTn>j^DN~lRaLJ$lr%C#-wGk*ru)(#;B`QN%J9twCPQ)Txs z(}8l7cQfiiYF9io?rGI30D|7r+ID;)hZNGox!3nk)YPsQQu*+P8m`|W2qrHyBAekH@ zi2N_?<>ZF2r9Q;OyvHDL*DDO6;uaEFwZl8q`@%%3sz9D+dY1+V6nm4_&M#P-##{+$0axwgy7;L}5YPX^2_Zm*W%0P! z7}sFc0f3U-k#_4ECr|GKiAgiy$Mo-cE?q-K_tF3Fy97U8y!adk&50g5_XlkpaTB51 z#xIweh1}ioSAEUb`V|!KJ;sjsckNeEyg_wT-At=v9HZmtPj#u2P~Cz>MuwV=#n~T@ zxC~|`9NGP%eHI`8J=+aTH(fVtw7dObgA7bX-TjdhO5&Yt{cniW-Hv9r-tEvn@--UqyTMypbl#zn?2VRb&i3B+ z4B04`i3s7f*NT+30a7hnx3!>?~!BlH5-wF!iwOtzIbplWaFG)Wii7)o+Ttjl>(cJbisnd~Nm z@GP#Bv~AzdnYhDVqf&19`H-)DH?D2>^Lqo7z5vpj*w65CZjwbDU=iozU;*pxgI(Nq z;%E6ikN%Mblf`Qw>Ib&r4A)Ve62tT8N|l}Dq}_Nip(Gh~PZ(pmCxyDzUyX=ZL{7nh z{2O>H=p)2|vO?Z`H#96vxT$oh8F<4*gM#P>{bvqt1G8dUdc$;w3D*W8/$i/g" a1.smt | yices-smt) = "sat" ]; do + i=$((i+1)) +done +sed "s//$((i-1))/g" a1.smt | yices-smt -m diff --git a/ar/assignments/src/1.smt b/ar/assignments/src/a1.smt similarity index 100% rename from ar/assignments/src/1.smt rename to ar/assignments/src/a1.smt diff --git a/ar/assignments/src/a2.bash b/ar/assignments/src/a2.bash new file mode 100644 index 0000000..5462573 --- /dev/null +++ b/ar/assignments/src/a2.bash @@ -0,0 +1 @@ +python3 a2.py | yices-smt -m diff --git a/ar/assignments/src/2.py b/ar/assignments/src/a2.py similarity index 100% rename from ar/assignments/src/2.py rename to ar/assignments/src/a2.py diff --git a/ar/assignments/src/a3.bash b/ar/assignments/src/a3.bash new file mode 100644 index 0000000..115f1fd --- /dev/null +++ b/ar/assignments/src/a3.bash @@ -0,0 +1,5 @@ +i=1 +while [ $(python3 a3.py $i | yices-smt) = "unsat" ]; do + i=$((i+1)) +done +python3 a3.py $i | yices-smt -m diff --git a/ar/assignments/src/a3.py b/ar/assignments/src/a3.py new file mode 100644 index 0000000..a295c8d --- /dev/null +++ b/ar/assignments/src/a3.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python3 +import sys + +if len(sys.argv) != 2: + print("usage: {} maxjobstart".format(sys.argv[0])) + exit() + +maxjobstart = sys.argv[1] +jobs = 12 +J = range(1, jobs+1) +Jprime = {5, 7, 10} +pi = { + 3: {1,2}, + 5: {3,4}, + 7: {3,4,6}, + 9: {5,8}, + 11: {10}, + 12: {9,11} +} + +# Print preamble +print("(benchmark a4.smt") +print(":logic QF_UFLIA") + +# Print variables +print(":extrafuns (") +for i in J: + print("(j{} Int)".format(i), end=' ') +print("\n)") + +print(":formula") +print("(and") +for i in J: + # Make sure the times are positive and within the bound + print("(> j{0} 0) (<= (+ j{0} {0}) {1})".format(i, maxjobstart)) + # Make sure the dependencies are done when a task is scheduled + for k in pi.get(i, {}): + print("(>= j{0} (+ j{1} {1}))".format(i, k)) +# Make sure the shared resources are not used by two tasks at once +for i in Jprime: + for k in Jprime: + if i != k: + print("(or (>= j{0} (+ j{1} {1}))".format(i,k), end=' ') + print("(<= (+ j{0} {0}) j{1}))".format(i,k)) + +# Close the and,benchmark parenthesis +print("))") diff --git a/ar/assignments/src/a4.bash b/ar/assignments/src/a4.bash new file mode 100644 index 0000000..7a5211d --- /dev/null +++ b/ar/assignments/src/a4.bash @@ -0,0 +1,5 @@ +i=1 +while [ $(python3 a4.py $i | yices-smt) = "unsat" ]; do + i=$((i+1)) +done +python3 a3.py $((i-1)) | yices-smt -m diff --git a/ar/assignments/src/4.py b/ar/assignments/src/a4.py similarity index 100% rename from ar/assignments/src/4.py rename to ar/assignments/src/a4.py -- 2.20.1