\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}w<c_{j}x\\
		\nonumber & \qquad\qquad\qquad \vee c_{i}y>c_{j}y+c_{j}h\\
		\nonumber & \qquad\qquad\qquad 
			\vee c_{i}y+c_{j}h<c_{j}h\Bigr)\Biggr)\wedge\\
	\bigwedge_{i\in PC}\bigwedge_{j\in PC}\Biggl( & i=j\\
		\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_{i}x-1>c_{j}x+c_{j}w\\
		\nonumber & \vee c_{i}x+1+c_{j}w<c_{j}x\\
		\nonumber & \vee c_{i}y-1>c_{j}y+c_{j}h\\
		\nonumber & \vee c_{i}y+1+c_{j}h<c_{j}h\Biggr)
\end{align}

Every numbered subformula describes a constraint from the problem description.
We can separated the subformulas in formulas going over all components, only
power components and only regular components.
\begin{itemize}
	\item\textbf{All}
		\begin{enumerate}
			\setcounter{enumi}{7}
			\item Makes sure the width and the height of the
				component can be swapped thus allowing a
				rotation.
			\item Makes sure the components are placed on the
				chip by stating that the $x$ and $y$
				coordinates are bigger then $0$ and the $x$ and
				$y$ plus their width or height does not exceed
				the specified width and height 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 Makes sure power components are at least $17$
				block away from other power components by
				stating 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 Makes sure regular components are connected to a
				power component by stating, using the same
				method as in the overlay, that it has overlap
				with a power component that has had its size
				increased by $1$.
		\end{enumerate}
\end{itemize}

\subsection{SMT format solution}
The formula is easily convertable via a Python script to SMT format by literal
conversion and said script is listed in Listing~\ref{listing:a2.py}. The Python
script optimizes a little bit from the original formula by leaving out the
overlap checking between the same components. The solution is calculated using
the command shown in Listing~\ref{listing:2.bash}

\lstinputlisting[language=bash,
	caption={Find the shortest solution for problem 3},
	label={listing:2.bash}]{src/a2.bash}

\subsection{Solution}
Finding this solution takes less then $35$ seconds and is shown in
Table~\ref{tab:s2}.

\begin{table}[H]
	\centering
	\input{a2.tex}
\label{tab:s2}
	\caption{Solution visualization for problem 2}
\end{table}
