\nonumber & \qquad\qquad\qquad \vee c_iy>c_jy+c_jh\\
\nonumber & \qquad\qquad\qquad \vee c_iy+c_jh<c_jh\Bigr)\Biggr)\wedge\\
\bigwedge_{i\in PC}\bigwedge_{j\in PC}\Biggl( & i=j\\
- \nonumber & \vee c_ix+\frac{c_iw}{2}-c_jx+\frac{c_jw}{2}>15\\
- \nonumber & \vee c_jx+\frac{c_jw}{2}-c_ix+\frac{c_iw}{2}>15\\
- \nonumber & \vee c_iy+\frac{c_ih}{2}-c_jy+\frac{c_jh}{2}>15\\
- \nonumber & \vee c_jy+\frac{c_jh}{2}-c_iy+\frac{c_ih}{2}>15\Biggr)\wedge\\
+ \nonumber & \vee c_ix+\frac{c_iw}{2}-c_jx+\frac{c_jw}{2}>17\\
+ \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\\
\bigwedge_{i\in RC}\bigvee_{j\in PC}\neg\Biggl(
& (c_ix-1>c_jx+c_jw\\
\nonumber & \vee c_ix+1+c_jw<c_jx\\
\nonumber & \vee c_iy+1+c_jh<c_jh\Biggr)
\end{align}
+All subformulas describe a constraint from the problem description and can be
+separated in three groups. Subformulas going over all components, only power
+components and only regular components.
+\begin{itemize}
+ \item\textbf{All}
+ \begin{enumerate}
+ \setcounter{enumi}{7}
+ \item Describes that the width and the height of the component can be
+ swapped(in case of rotation).
+ \item Constrains location of the components in regard to the size of
+ the chip.
+ \item Makes sure the components do not overlap by defining for all
+ pairs of components that they either are strictly right, strictly
+ left, strictly above or strictly below the other.
+ \end{enumerate}
+ \item\textbf{Power only}
+ \begin{enumerate}
+ \setcounter{enumi}{10}
+ \item Power components must be at least $17$ block away from
+ other power components. This is defined by saying that the
+ difference between the center of each pair of components is
+ bigger then $17$.
+ \end{enumerate}
+ \item\textbf{Regular only}
+ \begin{enumerate}
+ \setcounter{enumi}{11}
+ \item Regular components must be connected to a power
+ components. This is described using the method from the
+ overalap calculation in a negated way. Every regular
+ component must have overlap with a power component that
+ has been enlarged by $1$.
+ \end{enumerate}
+\end{itemize}
+
\subsection{SMT format solution}
+The formula is easily convertable via a Python script to SMT format and said
+script is listed in Listing~\ref{listing:2.py}. The Python script optimizes a
+little bit from the original formula by leaving out the overlap checking
+between the same components. When we run the file a solution is found within
+$30$ seconds.
+
+\subsection{Solution}
+Figure~\ref{fig:s2} shows the configuration found by the solver. Light gray
+components are regular components and darker gray components are power
+components.
+
+\begin{figure}[H]
+ \includegraphics[scale=0.75]{s2.png}
+ \label{fig:s2}
+ \caption{Solution visualization for problem 2}
+\end{figure}
#!/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
print("(c{:02d}h Int)".format(i))
print(")")
-# Preamble2
print(":formula")
print("(and")
for i, (w, h) in enumerate(pc+rc, 1):
# Print the width and height
print((
- '\t(or '
+ '(or '
'(and (= c{0:02d}w {1}) (= c{0:02d}h {2})) '
- '(and (= c{0:02d}w {2}) (= c{0:02d}h {1}))'
- ')').format(i, w-1, h-1))
+ '(and (= c{0:02d}w {2}) (= c{0:02d}h {1})))').format(i, w-1, h-1))
- # Print the bounds of the coordinates
+ # Print the bounds of the coordinates
print((
- '\t(> c{0:02d}x 0) (> c{0:02d}y 0)\n'
- '\t(<= (+ c{0:02d}x c{0:02d}w) {1}) (<= (+ c{0:02d}y c{0:02d}h) {2})\n'
- ).format(i, mx, my))
+ '(> c{0:02d}x 0) (> c{0:02d}y 0)'
+ '(<= (+ c{0:02d}x c{0:02d}w) {1}) (<= (+ c{0:02d}y c{0:02d}h) {2})'
+ ).format(i, mx, my))
- # Print the non overlap with others
+ # Print the non overlap with others
for j in range(1, 1+len(pc+rc)):
if i != j:
print((
- '\t(or \n'
- '\t\t(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) '
- '(< (+ c{0:02d}x c{0:02d}w) c{1:02d}x)\n'
- '\t\t(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) '
- '(< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
- ')').format(i, j))
+ '(or '
+ '(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) (< (+ c{0:02d}x c{0:02d}w) c{1:02d}x) '
+ '(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) (< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
+ ')').format(i, j))
-# Print the PC distance to eachother
+ # Print the PC distance to eachother
for i, _ in enumerate(pc, 1):
for j, _ in enumerate(pc, 1):
if i != j:
print((
- '\t(or \n'
- '\t\t(> \n'
- '\t\t\t(- \n'
- '\t\t\t\t(+ \n'
- '\t\t\t\t\tc{0:02d}x \n'
- '\t\t\t\t\t(/ c{0:02d}w 2) \n'
- '\t\t\t\t) \n'
- '\t\t\t\t(+ \n'
- '\t\t\t\t\tc{1:02d}x \n'
- '\t\t\t\t\t(/ c{1:02d}w 2) \n'
- '\t\t\t\t) \n'
- '\t\t\t) \n'
- '\t\t\t{2} \n'
- '\t\t)\n'
- '\t\t(> (- (+ c{1:02d}x (/ c{1:02d}w 2)) '
- '(+ c{0:02d}x (/ c{0:02d}w 2))) {2})\n'
- '\t\t(> (- (+ c{0:02d}y (/ c{0:02d}h 2)) '
- '(+ c{1:02d}y (/ c{1:02d}h 2))) {2})\n'
- '\t\t(> (- (+ c{1:02d}y (/ c{1:02d}h 2)) '
- '(+ c{0:02d}y (/ c{0:02d}h 2))) {2})'
+ '(or '
+ '(> (- (+ c{0:02d}x (/ c{0:02d}w 2) ) (+ c{1:02d}x (/ c{1:02d}w 2) ) ) {2} ) '
+ '(> (- (+ c{1:02d}x (/ c{1:02d}w 2)) (+ c{0:02d}x (/ c{0:02d}w 2))) {2}) '
+ '(> (- (+ c{0:02d}y (/ c{0:02d}h 2)) (+ c{1:02d}y (/ c{1:02d}h 2))) {2}) '
+ '(> (- (+ c{1:02d}y (/ c{1:02d}h 2)) (+ c{0:02d}y (/ c{0:02d}h 2))) {2})'
')').format(i, j, pd))
-# Print the constraint that they have to be connected to a ps
+ # Print the constraint that they have to be connected to a ps
for i, _ in enumerate(rc, 1+len(pc)):
- print('\t(or')
+ print('(or')
for j, _ in enumerate(pc, 1):
print((
- '\t(not (or \n'
- '\t\t(> c{0:02d}x (+ c{1:02d}x 1 c{1:02d}w)) '
- '(< (+ c{0:02d}x c{0:02d}w) (- c{1:02d}x 1))\n'
- '\t\t(> c{0:02d}y (+ c{1:02d}y 1 c{1:02d}h)) '
- '(< (+ c{0:02d}y c{0:02d}h) (- c{1:02d}y 1))'
+ '(not (or '
+ '(> c{0:02d}x (+ c{1:02d}x 1 c{1:02d}w)) (< (+ c{0:02d}x c{0:02d}w) (- c{1:02d}x 1)) '
+ '(> c{0:02d}y (+ c{1:02d}y 1 c{1:02d}h)) (< (+ c{0:02d}y c{0:02d}h) (- c{1:02d}y 1))'
'))').format(i, j))
- print('\t)')
+ print(')')
# Close the and,benchmark parenthesis
print("))")
repositories / master.git / commitdiff
