From 4eaa9c4aa694d8bab2cb202bda57c434db1fe142 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Mon, 26 Oct 2015 15:32:32 +0100 Subject: [PATCH] initial commit, transfer from own repo --- .gitignore | 8 ++++ 1.tex | 115 ++++++++++++++++++++++++++++++++++++++++++++++++ 2.tex | 122 +++++++++++++++++++++++++++++++++++++++++++++++++++ 3.tex | 77 ++++++++++++++++++++++++++++++++ 4.tex | 89 +++++++++++++++++++++++++++++++++++++ Makefile | 20 +++++++++ README.md | 20 +++++++++ a.tex | 22 ++++++++++ ar.tex | 21 +++++++++ preamble.tex | 30 +++++++++++++ src/a1.bash | 6 +++ src/a1.smt | 60 +++++++++++++++++++++++++ src/a2.bash | 1 + src/a2.py | 64 +++++++++++++++++++++++++++ src/a3.bash | 50 +++++++++++++++++++++ src/a4.bash | 63 ++++++++++++++++++++++++++ 16 files changed, 768 insertions(+) create mode 100644 .gitignore create mode 100644 1.tex create mode 100644 2.tex create mode 100644 3.tex create mode 100644 4.tex create mode 100644 Makefile create mode 100644 README.md create mode 100644 a.tex create mode 100644 ar.tex create mode 100644 preamble.tex create mode 100644 src/a1.bash create mode 100644 src/a1.smt create mode 100644 src/a2.bash create mode 100644 src/a2.py create mode 100644 src/a3.bash create mode 100644 src/a4.bash diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..94feb01 --- /dev/null +++ b/.gitignore @@ -0,0 +1,8 @@ +*.log +*.fmt +*.fmt +*.aux +*.out +*.toc +*.pdf +*.png diff --git a/1.tex b/1.tex new file mode 100644 index 0000000..098a2e3 --- /dev/null +++ b/1.tex @@ -0,0 +1,115 @@ +\section{Problem 1} +{\em +Six trucks have to deliver pallets of obscure building blocks to a magic +factory. Every truck has a capacity of 7800 kg and can carry at most +eight pallets. In total, the following has to be delivered: +\begin{itemize} + \item Four pallets of nuzzles, each of weight 700 kg. + \item A number of pallets of prittles, each of weight 800 kg. + \item Eight pallets of skipples, each of weight 1000 kg. + \item Ten pallets of crottles, each of weight 1500 kg. + \item Five pallets of dupples, each of weight 100 kg. +\end{itemize} +Prittles and crottles are an explosive combination: they are not allowed to be +put in the same truck. + +Skipples need to be cooled; only two of the six trucks have facility for +cooling skipples. Dupples are very valuable; to distribute the risk of loss no +two pallets of dupples may be in the same truck. + +Investigate what is the maximum number of pallets of prittles that can be +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,\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 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_{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( + & \left(\sum^{T}_{i=1}t_{i}r\right)=n(r)\Biggr) +\end{align} + +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 + 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 + 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 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. + \end{enumerate} + \item \textbf{Pallets} + \begin{enumerate} + \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)$. + \end{enumerate} +\end{itemize} + +\subsection{SMT format solution} +The formula is easily convertable to SMT format by literal conversion and is +listed in 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}. + +\lstinputlisting[language=bash, + caption={Iteratively find the largest solution for problem 1}, + label={listing:1.bash}]{src/a1.bash} + +\subsection{Solution} +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] + \centering + \begin{tabular}{l|lllll|ll} + \toprule + Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & + Weight & Pallets\\ + \midrule + 1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\ + 2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\ + 3 & 0 & 8 & 0 & 0 & 0 & 6400 & 7\\ + 4 & 0 & 7 & 0 & 0 & 1 & 5700 & 8\\ + 5 & 0 & 0 & 0 & 5 & 1 & 7600 & 6\\ + 6 & 4 & 0 & 0 & 3 & 1 & 7400 & 8\\ + \midrule + total & 4 & 18 & 8 & 10 & 5 & &\\ + \bottomrule + \end{tabular} + \caption{Solution visualization for problem 1} +\label{tab:s1} +\end{table} diff --git a/2.tex b/2.tex new file mode 100644 index 0000000..12ed33d --- /dev/null +++ b/2.tex @@ -0,0 +1,122 @@ +\section{Problem 2} +{\em + Give a chip design containing three power components and eight regular +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 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). +\end{itemize} +} + +\newpage +\subsection{Formal definition} +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_{i}h=h(i)\vee c_{i}h=w(i))\wedge(c_{i}w=w(i)\vee c_{i}w=h(i))\\ + & \wedge 29-c_{i}w\geq c_{i}x>0\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_{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_{i}x-1>c_{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}+i/$i/g" a1.smt | yices-smt) = "sat" ]; do + echo "n(p)=$i is still sat" + i=$((i+1)) +done +echo "n(p)=$i is unsat thus maximum n(p)=$((i-1))" diff --git a/src/a1.smt b/src/a1.smt new file mode 100644 index 0000000..cf5342e --- /dev/null +++ b/src/a1.smt @@ -0,0 +1,60 @@ +(benchmark a1.smt +:logic QF_UFLIA +:extrafuns ( + (t1p Int) (t1n Int) (t1s Int) (t1c Int) (t1d Int) + (t2p Int) (t2n Int) (t2s Int) (t2c Int) (t2d Int) + (t3p Int) (t3n Int) (t3s Int) (t3c Int) (t3d Int) + (t4p Int) (t4n Int) (t4s Int) (t4c Int) (t4d Int) + (t5p Int) (t5n Int) (t5s Int) (t5c Int) (t5d Int) + (t6p Int) (t6n Int) (t6s Int) (t6c Int) (t6d Int) +) +:formula +(and + (>= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0) + (>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0) + (>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0) + (>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0) + (>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0) + (>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0) + + (<= (+ t1p t1n t1s t1c t1d) 8) + (<= (+ t2p t2n t2s t2c t2d) 8) + (<= (+ t3p t3n t3s t3c t3d) 8) + (<= (+ t4p t4n t4s t4c t4d) 8) + (<= (+ t5p t5n t5s t5c t5d) 8) + (<= (+ t6p t6n t6s t6c t6d) 8) + + (<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800) + (<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800) + (<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800) + (<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800) + (<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800) + (<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800) + + (or (= 0 t1p) (= 0 t1c)) + (or (= 0 t2p) (= 0 t2c)) + (or (= 0 t3p) (= 0 t3c)) + (or (= 0 t4p) (= 0 t4c)) + (or (= 0 t5p) (= 0 t5c)) + (or (= 0 t6p) (= 0 t6c)) + + (<= t1d 1) + (<= t2d 1) + (<= t3d 1) + (<= t4d 1) + (<= t5d 1) + (<= t6d 1) + + (= t3s 0) + (= t4s 0) + (= t5s 0) + (= t6s 0) + + (= (+ t1n t2n t3n t4n t5n t6n) 4) + (= (+ t1s t2s t3s t4s t5s t6s) 8) + (= (+ t1c t2c t3c t4c t5c t6c) 10) + (= (+ t1d t2d t3d t4d t5d t6d) 5) + + (>= (+ t1p t2p t3p t4p t5p t6p) ) +) +) diff --git a/src/a2.bash b/src/a2.bash new file mode 100644 index 0000000..5462573 --- /dev/null +++ b/src/a2.bash @@ -0,0 +1 @@ +python3 a2.py | yices-smt -m diff --git a/src/a2.py b/src/a2.py new file mode 100644 index 0000000..a782fe7 --- /dev/null +++ b/src/a2.py @@ -0,0 +1,64 @@ +#!/usr/bin/env python3 +pc = [(4, 2), (4, 2), (4, 2)] +rc = [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)] +mx = 29 +my = 22 +pd = 17 + +# Print variables and preamble +print('(benchmark a4.smt') +print(':logic QF_UFLIA') +print(':extrafuns (') +for i, (w, h) in enumerate(pc+rc, 1): + print('(c{}x Int)'.format(i), end=' ') + print('(c{}y Int)'.format(i), end=' ') + print('(c{}w Int)'.format(i), end=' ') + print('(c{}h Int)'.format(i)) +print(')') + +print(':formula') +print('(and') + +# Print the PC and RC subformulas +for i, (w, h) in enumerate(pc+rc, 1): + # Print the width and height + print(('(or ' + '(and (= c{0}w {1}) (= c{0}h {2})) ' + '(and (= c{0}w {2}) (= c{0}h {1})))').format(i, w-1, h-1)) + # Print the bounds of the coordinates + print(('(> c{0}x 0) (> c{0}y 0)' + '(<= (+ c{0}x c{0}w) {1}) (<= (+ c{0}y c{0}h) {2})' + ).format(i, mx, my)) + + # Print the non overlap with others + for j in range(1, 1+len(pc+rc)): + if i != j: + print(( + '(or ' + '(> c{0}x (+ c{1}x c{1}w)) (< (+ c{0}x c{0}w) c{1}x) ' + '(> c{0}y (+ c{1}y c{1}h)) (< (+ c{0}y c{0}h) c{1}y)' + ')').format(i, j)) + +# Print the PC distance to eachother +for i, _ in enumerate(pc, 1): + for j, _ in enumerate(pc, 1): + if i != j: + print(('(or ' + '(> (- (+ c{0}x (/ c{0}w 2)) (+ c{1}x (/ c{1}w 2))) {2}) ' + '(> (- (+ c{1}x (/ c{1}w 2)) (+ c{0}x (/ c{0}w 2))) {2}) ' + '(> (- (+ c{0}y (/ c{0}h 2)) (+ c{1}y (/ c{1}h 2))) {2}) ' + '(> (- (+ c{1}y (/ c{1}h 2)) (+ c{0}y (/ c{0}h 2))) {2})' + ')').format(i, j, pd)) + + # Print the constraint that they have to be connected to a ps +for i, _ in enumerate(rc, 1+len(pc)): + print('(or') + for j, _ in enumerate(pc, 1): + print(('(not (or ' + '(> c{0}x (+ c{1}x 1 c{1}w)) (< (+ c{0}x c{0}w) (- c{1}x 1)) ' + '(> c{0}y (+ c{1}y 1 c{1}h)) (< (+ c{0}y c{0}h) (- c{1}y 1))' + '))').format(i, j)) + print(')') + +# Close the and,benchmark parenthesis +print('))') diff --git a/src/a3.bash b/src/a3.bash new file mode 100644 index 0000000..5b16adc --- /dev/null +++ b/src/a3.bash @@ -0,0 +1,50 @@ +#!/bin/bash +JOBS=12 +J=$(seq 1 $JOBS) +JPRIME="5 7 10" + +function pi { + case $1 in + 3) echo 1 2;; + 5) echo 3 4;; + 7) echo 3 4 6;; + 9) echo 5 8;; + 11) echo 10;; + 12) echo 9 11;; + *);; + esac +} + +function generate { + local i j + echo "(benchmark a4.smt" + echo ":logic QF_UFLIA" + echo ":extrafuns (" + for i in $J; do + echo "(j$i Int)" + done + echo ")" + echo ":formula" + echo "(and" + for i in $J; do + echo "(> j$i 0) (<= (+ j$i $i) $1)" + for j in $(pi $i); do + echo "(>= j$i (+ j$j $j))" + done + done + for i in $JPRIME; do + for j in $JPRIME; do + if [ $i != $j ]; then + echo "(or (>= j$i (+ j$j $j))" + echo " (<= (+ j$i $i) j$j))" + fi + done + done + echo "))" +} + +i=1 +while [ $(generate $i | yices-smt) = "unsat" ]; do + echo "T=$((i++)) is still unsat" +done +echo "T=$i is sat thus the minimum T=$i" diff --git a/src/a4.bash b/src/a4.bash new file mode 100644 index 0000000..7f9e0f9 --- /dev/null +++ b/src/a4.bash @@ -0,0 +1,63 @@ +#!/usr/bin/env python3 +NUMA=7 + +function generate { + local i n j + echo "(benchmark a4.smt" + echo ":logic QF_UFLIA" + echo ":extrafuns (" + echo "(a1 Int)" + echo "(a$NUMA Int)" + for i in $(seq 2 $((NUMA-1))); do + for n in $(seq 0 $1); do + echo "(i${n}a$i Int)" + done + done + echo ")" + echo ":formula" + echo "(and" + + echo "(= a1 1)" + echo "(= a$NUMA $NUMA)" + for i in $(seq 2 $((NUMA-1))); do + echo "(= i0a$i $i)" + done + + for n in $(seq 1 $1); do + echo "(or" + for i in $(seq 2 $((NUMA-1))); do + echo "(and" + [ $i = 2 ] && prev=1 || prev="i$((n-1))a$((i-1))" + [ $i = $((NUMA-1)) ] && next=7 || next="i$((n-1))a$((i+1))" + echo "(= i${n}a$i (+ $prev $next)) " + for j in $(seq 2 $((NUMA-1))); do + if [ $i != $j ]; then + echo "(= i${n}a$j i$((n-1))a$j)" + fi + done + echo ")" + done + echo ")" + done + + echo "(or" + for i in $(seq 2 $((NUMA-1))); do + echo "(and" + echo "(>= i${1}a$i 50)" + echo "(or" + for j in $(seq 2 $((NUMA-1))); do + if [ $i != $j ]; then + echo "(= i${1}a$i i${1}a$j)" + fi + done + echo "))" + done + echo ")))" +} + +i=1 +while [ $(generate $i | yices-smt) = "unsat" ]; do + echo "N=$i is still unsat" + i=$((i+1)) +done +echo "N=$i is sat thus minimum N=$i" -- 2.20.1