\documentclass{report}

\usepackage{amsmath, amsthm, amssymb}
\usepackage{setspace, fancyhdr, extramarks, fullpage, lastpage}
\usepackage{fourier}
\usepackage{graphicx,float,wrapfig, algorithm2e}
\usepackage[all]{xy}
\usepackage{enumerate}



% Homework Specific Information
\newcommand{\hmwkTitle}{Homework 1}
\newcommand{\hmwkAssignDate}{January 18}
\newcommand{\hmwkDueDate}{February 1}
\newcommand{\hmwkClass}{Graduate Artificial Intelligence 15-780}
\newcommand{\hmwkClassInstructor}{Geoff Gordon \and Tuomas Sandholm}
\newcommand{\hmwkDescr}{Logic and Proofs}

%\newcommand{\Answer}[1]{\noindent\fbox{\begin{minipage}[c]{0.9\columnwidth}#1\end{minipage}}}
\newcommand{\Answer}[1]
  {}
  
\newenvironment{penumerate}{
\begin{enumerate}
  \setlength{\itemsep}{0pt}
  \setlength{\parsep}{3pt}
  \setlength{\topsep}{-8pt}
  \setlength{\partopsep}{0pt}
  \setlength{\leftmargin}{1.5em}
  \setlength{\labelwidth}{1em}
  \setlength{\labelsep}{0.5em}
  \setlength{\parskip}{0pt}
  \setlength{\parsep}{0pt}
}{\end{enumerate}}
\newenvironment{pitemize}{
\begin{itemize}
  \setlength{\itemsep}{0pt}
  \setlength{\parsep}{3pt}
  \setlength{\topsep}{-8pt}
  \setlength{\partopsep}{0pt}
  \setlength{\leftmargin}{1.5em}
  \setlength{\labelwidth}{1em}
  \setlength{\labelsep}{0.5em}
  \setlength{\parskip}{0pt}
  \setlength{\parsep}{0pt}
}{\end{itemize}}


\renewcommand{\labelenumi}{\alph{enumi})}

% In case you need to adjust margins:
\topmargin=-0.45in      %
\evensidemargin=0in     %
\oddsidemargin=0in      %
\textwidth=6.5in        %
\textheight=9.0in       %
\headsep=0.25in         %

% Setup the header and footer
\pagestyle{fancy}                                                       %                                          %
\lhead{\hmwkTitle}  %
\rhead{\hmwkClass }                                                     %                                                     %
\cfoot{}                                                                %
\rfoot{Page\ \thepage\ of\ \protect\pageref{LastPage}}                          %
\renewcommand\headrulewidth{0.4pt}                                      %
\renewcommand\footrulewidth{0.4pt}                                      %

% This is used to trace down (pin point) problems
% in latexing a document:
%\tracingall

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some tools
\newcommand{\enterProblemHeader}[1]{\nobreak\extramarks{#1}{#1 continued on next page\ldots}\nobreak%
                                    \nobreak\extramarks{#1 (continued)}{#1 continued on next page\ldots}\nobreak}%
\newcommand{\exitProblemHeader}[1]{\nobreak\extramarks{#1 (continued)}{#1 continued on next page\ldots}\nobreak%
                                   \nobreak\extramarks{#1}{}\nobreak}%

\newlength{\labelLength}
\newcommand{\labelAnswer}[2]
  {\settowidth{\labelLength}{#1}%
   \addtolength{\labelLength}{0.25in}%
   \changetext{}{-\labelLength}{}{}{}%
   \noindent\fbox{\begin{minipage}[c]{\columnwidth}#2\end{minipage}}%
   \marginpar{\fbox{#1}}%

   % We put the blank space above in order to make sure this
   % \marginpar gets correctly placed.
   \changetext{}{+\labelLength}{}{}{}}%

\newcommand{\homeworkProblemName}{}%
\newcounter{homeworkProblemCounter}%
\newenvironment{homeworkProblem}[1][Problem \arabic{homeworkProblemCounter}]%
  {\stepcounter{homeworkProblemCounter}%
   \renewcommand{\homeworkProblemName}{#1}%
   \section*{\homeworkProblemName}%
   \enterProblemHeader{\homeworkProblemName}}%
  {\exitProblemHeader{\homeworkProblemName}}%

\newcommand{\problemLAnswer}[1]
  {\labelAnswer{\homeworkProblemName}{#1}}

\newcommand{\homeworkSectionName}{}%
\newlength{\homeworkSectionLabelLength}{}%
\newenvironment{homeworkSection}[1]%
  {% We put this space here to make sure we're not connected to the above.
   % Otherwise the changetext can do funny things to the other margin

   \renewcommand{\homeworkSectionName}{#1}%
   \settowidth{\homeworkSectionLabelLength}{\homeworkSectionName}%
   \addtolength{\homeworkSectionLabelLength}{0.25in}%
   \changetext{}{-\homeworkSectionLabelLength}{}{}{}%
   \subsection*{\homeworkSectionName}%
   \enterProblemHeader{\homeworkProblemName\ [\homeworkSectionName]}}%
  {\enterProblemHeader{\homeworkProblemName}%

   % We put the blank space above in order to make sure this margin
   % change doesn't happen too soon (otherwise \sectionAnswer's can
   % get ugly about their \marginpar placement.
   \changetext{}{+\homeworkSectionLabelLength}{}{}{}}%

\newcommand{\sectionAnswer}[1]
  {% We put this space here to make sure we're disconnected from the previous
   % passage

   \noindent\fbox{\begin{minipage}[c]{\columnwidth}#1\end{minipage}}%
   \enterProblemHeader{\homeworkProblemName}\exitProblemHeader{\homeworkProblemName}%
   \marginpar{\fbox{\homeworkSectionName}}%

   % We put the blank space above in order to make sure this
   % \marginpar gets correctly placed.
   }%

\begin{document}
\begin{spacing}{1.1}

 \begin{titlepage}
   \begin{center}
~

\vspace{2in}
\Large{\textmd{\textbf{\hmwkClass}}}

\vspace{1in}
\Huge{\hmwkTitle: \emph{\hmwkDescr}}

\vspace{1in}

\decofourright

\vspace{1in}

\large{Out\ on\ \hmwkAssignDate}\\
\large{Due\ on\ \hmwkDueDate}
 \end{center}
 \end{titlepage}

% ---- Problem 1 -----

\begin{homeworkProblem}[Problem 1: Murder at the Chauvinistic Adventurer's Club]
Detective d'Civet tapped his cup of coffee against his saucer, calling the room to attention. "We know this much for certain: that the killer is still at large," he announced while smoothing his mustache. There are three members of the Adventurer's Club sitting in the room: Professor Agouti, Colonel Bandicoot, and Lord Crabb. "Let us review the facts of the case," he continued:
\begin{penumerate}
\item Each member of the Adventurer's Club likes to sail, mountain climb, or spelunk (explore caves);
\item Each member of the Adventurer's Club likes to smoke pipes or cigars;
\item Each member of the Adventurer's Club likes to drink gin or rum;
\item No one both climbs and spelunks;
\item No mountaineer likes to drink gin, but all sailors enjoy a good rum;
\item Every spelunkers smokes cigars, while no sailor smokes pipes;
\item Agouti likes rum and is a climber;
\item Crabb only smokes the finest Cuban cigars and is a spelunker;
\item Crabb and Agouti are old enemies: Crabb dislikes everything that Agouti likes, and likes whatever Agouti dislikes;
\item Bandicoot spelunks and does either mountain climbing or sailing;
\item The murderer likes both rum and cigars
\item Exactly one of Agouti, Bandicoot, and Crabb is the murderer.
\end{penumerate}
"Unfortunately," concluded the Detective with a sad sip of his coffee, "I am still unable to conclude the identity of the killer." \emph{Can you? Answer the following questions to find out.}

\begin{enumerate} [1) ]
\item Write each sentence out as a formula of first-order logic without equality. (\emph{Hint: consider the predicates $\mathit{Likes}(x,y)$ and $\mathit{IsMurderer}(x)$.})

\item Convert each formula to CNF.
\item Suppose you suspect that Bandicoot did it. Show this by doing the following three inferences:
	\begin{itemize}
		\item Could Agouti be the killer? (Does $(a)\wedge \ldots \wedge (l) \vDash \neg \mathit{IsMurderer}( \mathit{agouti})$?) 
		\item Could Crabb be the killer?
		\item Is Bandicoot the killer? (Does $(a)\wedge \ldots \wedge (l) \vDash \mathit{IsMurderer}( \mathit{bandicoot})$?) 
	\end{itemize} 
	Show a resolution proof for each of the three inferences. (\emph{Hint:} do the proofs for Agouti and Crabb first.)

\end{enumerate}
\end{homeworkProblem}

% ---- Problem 2 -----

\begin{homeworkProblem}[Problem 2: Cryptarithms, SAT, and CSPs]
A cryptarithm is a simple arithmetic problem, but the number have been replaced with letters. For example, the following is a classic example (borrowed from Wikipedia).

\begin{table}[htpb]
\begin{center}
\begin{tabular}{lllll}
&S&E&N&D\\
+&M&O&R&E\\\hline
M&O&N&E&Y
\end{tabular}
\end{center}
\caption{The SEND MORE MONEY Cryptarithm.}
\label{tab:sendmore}
\end{table}
A solution to this puzzle is O = 0, M = 1, Y = 2, E = 5, N = 6, D = 7, R = 8, and S = 9. 

Consider the general problem of cryptarithms. Suppose that there are up to $k$ string that are no more than $m$ characters long, and a final string that is no more than $m + \left\lceil \log_n(k) \right\rceil$ characters long. The strings represent base $n$ numbers, so each letter could represent a number in $[0,n-1]$. We are looking for an assignment of numbers to letters so that the first $k$ strings add up to the last string.

\begin{enumerate}[1.]
\item Describe a CSP that captures this problem. Try to use as few variables and constraints as possible. For this problem, please restrict yourself to simple linear constraints (constraints using $+, =, \leq, \ldots$) that are easy to explain and only reference  small number of variables.
\begin{itemize}
\item What are the variables? What do they represent? What are their domains?
\item What are the constraints? Explain what they do. How many of them (asymptotically) are there? 
\item Explicitly write out the CSP for the SEND MORE MONEY cryptarithm (Table~\ref{tab:sendmore}). Use $k = 2$, $m = 4$, and $n = 10$.
\end{itemize}
\item SAT solvers are extremely useful for solving problems like these. Please take your general CSP formulation that you wrote in part (1) of this question and convert it into a general SAT formula.
\begin{itemize}
\item What are the variables? 
\item What are the constraints? How many of them (asymptotically) are there?
\end{itemize}
\item Looking at these two formulations
\begin{itemize}
\item What advantages does the CSP formulation have over the SAT formulation?
\item What advantages does the SAT formulation have over the CSP formulation?
\end{itemize}
\end{enumerate}
\end{homeworkProblem}

% ---- Problem 3 -----

\begin{homeworkProblem}[Problem 3: A Tree Representation]
A decision tree is a way to represent a propositional formula. Each branch in a tree represents assigning a proposition like $p$ both of its possible values. The leaves of the tree are either \emph{true} or \emph{false}, depending on whether the path to them represents a satisfying or unsatisfying assignment. 

For example, consider the formula \begin{equation*}
p \vee (q \wedge r).
\end{equation*}

This formula could be represented by either decision tree:

\begin{figure}[h!tbp]
\begin{center}
\begin{minipage}{0.2\columnwidth}
\resizebox{\columnwidth}{!}{
\xymatrix{
& p \ar^T[dl] \ar_F[dr] & &\\
\mathbf{T} & & q \ar^T[dl] \ar_F[dr]&\\
& r\ar^T[dl] \ar_F[dr] &  & \mathbf{F}\\
\mathbf{T} & & \mathbf{F}
}}
\end{minipage}
\hspace{50pt}
\begin{minipage}{0.5\columnwidth}
\resizebox{\columnwidth}{!}{
\xymatrix{
& &&& q \ar^T[dlll] \ar_F[drrr] & & & &&&\\
& r\ar^T[dl] \ar_F[dr] & &&&&& r\ar^T[dl] \ar_F[dr] &\\
\mathbf{T} & & p\ar^T[dl] \ar_F[dr] & &&&p\ar_T[dl] \ar^F[d]&&p\ar_T[d] \ar^F[dr]\\
&\mathbf{T} && \mathbf{F}&&\mathbf{T} & \mathbf{F}&&\mathbf{T} & \mathbf{F}
}}
\end{minipage}
\end{center}
\end{figure}

We will restrict our attention to trees that follow a \emph{variable ordering}. This means that every path from the root of the tree assigns the variables in the same order. For example the left subtree follows the ordering $p > q > r$ since all $p$-nodes appear before $q$ nodes, and all $q$-nodes appear before $r$ nodes. The right subtree follows the ordering $q > r > p$. The variable ordering is important to the size of the tree---the left tree is much more compact than the right tree. 

A decision tree can either be \emph{reduced} or not. A reduced decision tree does not have any branching nodes that are redundant in the sense that both of its subtrees are identical. For example, in both trees above, several branching nodes are omitted because they are not necessary---after assigning $p = \mathbf{T}$ the formula is satisfied regardless of the values assigned to $q$ and $r$. A general decision tree may have redundant branching nodes.

\begin{enumerate}[1.]
\item Consider the formula $(p \rightarrow q) \wedge (r \rightarrow p)$. Draw the reduced decision tree for the ordering $p > q > r$.
\item If you were handed a formula with $n$ propositions, and an ordering, what is the worst-case (asymptotic) size of its reduced decision tree?
\item If someone gave you a general (not necessarily reduced) decision tree for a formula that contained $n$ propositions, how quickly could you tell if the formula is:
	\begin{itemize}
		\item satisfiable?
		\item valid?
	\end{itemize}
For each give a worst-case analysis which depends only on $n$, as well as a worst-case analysis which depends on the number of nodes $m$ in the tree. What if the tree was a reduced decision tree?
\item Give a sequence of formulas $\left<F_1, F_2, \ldots\right>$ such that $F_n$ has $n$ distinct propositions, along with two corresponding sequences of orderings $\left<A_1, A_2, \ldots\right>$ and $\left<B_1, B_2, \ldots\right>$ such that the reduced decision tree for $F_n$ under $B_n$ is exponentially larger than the reduced decision tree for $F_n$ under $A_n$.
\item Suppose that someone told you that they had an alternative representation for a formula with $n$ propositions that never required more than a polynomial number of bits (in $n$) to express. Do you believe them? Justify your answer.
\end{enumerate} 

\end{homeworkProblem}

% ---- Problem 4 -----

\begin{homeworkProblem}[Problem 4: Inductive Structures and Recursive Functions in FOL]
Terms---combinations of functions and constants---can represent a number of interesting data structures in FOL.
For example, we can express natural numbers with the constant $\mathbf{z}$ and the $1$-ary successor function $s(x)$. \emph{E.g.} $\mathbf{z}$ represents $0$, $s(\mathbf{z})$ represents $1$ and $s(s(\mathbf{z}))$ represents $2$. We use the boldface font for $\mathbf{z}$ to distinguish it.

As a more advanced example, consider the 2-ary construction function $\mathit{cons}(x,y)$ and constants $a,b,\mathit{nil}$. We can build strings on $a,b$ by combining constants with the $\mathit{cons}$ function like so:
\begin{equation*}
\mathit{cons}(a,\mathit{cons}(b,\mathit{cons}(b,\mathit{cons}(a,\mathit{nil})))).
\end{equation*}
This example term represents the string `abba'. Notice that first argument of $\mathit{cons}$ is always a constant and the second argument is either a $\mathit{cons}$ statement or $\mathit{nil}$. We will call such terms \emph{well-formed strings}. An example of non-well-formed strings would be $\mathit{cons}(\mathit{nil},a)$ or $\mathit{cons}(b,a)$ or $\mathit{cons}(\mathit{cons}(b,a),\mathit{nil})$.

Furthermore, we can define predicates that do useful things for us:
\begin{enumerate}[1.]
\item Define two predicates for natural numbers:
	\begin{itemize}
		\item \emph{plus}, where the first two numbers must sum to form the last number \emph{e.g.} $\mathit{plus}(s(\mathbf{z}), s(\mathbf{z}), s(s(\mathbf{z})))$. Feel free to use the notation $s^n(\mathbf{z}) \equiv \underbrace{s(\ldots s(}_n \mathbf{z}) \ldots )$.
		\item \emph{times}, where the product of the first two numbers is the last number \emph{e.g.} $\mathit{times}(s(\mathbf{z}), s(s(\mathbf{z})), s(s(\mathbf{z})))$.
	\end{itemize}
\item In words, what does $\mathit{foo}(\mathit{nil},\mathbf{z}) \wedge \left[\forall w,x,y,\; \mathit{foo}(w,x) \rightarrow \mathit{foo}(\mathit{cons}(y,w), s(x))\right]$ do?
%\item Write a predicate that is \emph{true} if and only if a well-formed string contains the constant $a$.
\item In this question we will extend well-formed string to be any string where the first argument of $\mathit{cons}$ is a natural number, \emph{e.g.} $\mathit{cons}(s(\mathbf{z}),\mathit{cons}(s(s(\mathbf{\mathbf{z}})),\mathit{cons}(s(s(\mathbf{z})),\mathit{cons}(s(\mathbf{z}),\mathit{nil}))))$ is a well-formed string of natural numbers.

Define a predicate $\mathit{sum}(N, S)$ that takes in a well-formed string of natural numbers $S$ and a number $N$. It must be true if and only if $N$ is the sum of numbers in the string. For example: \[\mathit{sum}(s^6(\mathbf{z}),\; \mathit{cons}(s(\mathbf{z}),\mathit{cons}(s(s(\mathbf{\mathbf{z}})),\mathit{cons}(s(s(\mathbf{z})),\mathit{cons}(s(\mathbf{z}),\mathit{nil})))))\]
is true since $1 + 2 + 2 + 1 = 6$.
\item How would we describe a binary tree-like structure?
\item For your above formulation of a binary tree, define two predicates:
	\begin{itemize}
		\item The first is true if and only if $d$ is the \emph{depth} of the binary tree
		\item The second is true if and only if $n$ is the \emph{size} (number of nodes) of the binary tree
	\end{itemize}
\end{enumerate}
\end{homeworkProblem}

\end{spacing}
\end{document}
