\documentclass{article}
\usepackage{graphicx}
\usepackage[colorlinks=true,urlcolor=black,linkcolor=blue,citecolor=blue]{hyperref}%
\usepackage{fancyhdr}
\usepackage[margin=35mm]{geometry}
\usepackage{amsmath,amssymb}
\usepackage{stmaryrd}   % for the tval symbol
\usepackage{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{trees}

\usepackage{xcolor}
\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
\definecolor{tacticcolor}{rgb}{0.1, 0.2, 0.6}    % blue
\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
\definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} % red

\usepackage{listings}
\def\lstlanguagefiles{lstlean.tex}
\lstset{language=lean,breakatwhitespace}
\lstset{upquote=true}

\newcommand{\fn}[1]{\mathrm{#1}}
\newcommand{\append}{\mathbin{+\mkern-10mu+}}
\newcommand{\cons}{\mathbin{::}}
\newcommand{\tval}[1]{\llbracket #1 \rrbracket}
% If you don't have the stmaryrd package, the following substitute will do.
%\newcommand{\tval}[1]{[\![ #1 ]\!]}
\newcommand{\liff}{\leftrightarrow}
\newcommand{\fa}[1]{\forall #1. \, }
\newcommand{\ex}[1]{\exists #1. \, }
\newcommand{\mdl}[1]{\mathfrak{#1}}

\pagestyle{fancy}
\fancyhf{}
\renewcommand{\headrulewidth}{0pt}

\lhead{\sf Logic and Mechanized Reasoning}
\rhead{\sf Fall 2021}

\begin{document}

\bigskip

\begin{center}
{\Large Assignment 11}

\medskip

due 6pm Thursday, December 2, 2021
\end{center}

\medskip

\thispagestyle{fancy}

\noindent This is the last assignment of the semester. It is due
after Thanksgiving, on the last day of class.
The material needed for problem 2 will be added to the textbook and
repository by Tuesday, November 23.

These problems rely on the latest version of the github lamr repository,
so be sure to use a new Gitpod image or update your repository following the instructions in the README.
They require you to use an SMT solver (Z3, CVC4, or CVC5) and a
first-order theorem prover (Vampire). The lamr repository contains Linux binaries
in the folder {\tt LAMR/bin}, but if you want to use the software on Windows or macOS,
you need to replace these with the appropriate binaries, which you can find online.


\subsection*{Problem 1}

The almost square of order $n$ is a rectangle of size $n \times (n + 1)$. The almost squares of orders $1$ to $3$ can fully cover the almost square of order $4$. A solution is shown below.

\begin{verbatim}
  1 1 3 3 3
  2 2 3 3 3
  2 2 3 3 3
  2 2 3 3 3
\end{verbatim}

In this exercise, we are going to use an SMT solver to determine whether the almost squares of order $1$ to $n$ can fully cover the almost square of order $m$. The encoding uses the theory QF\_LIA. The encoding uses $4n$ variables: for the almost square of order {\tt i}, we use variables {\tt xmin\_i}, {\tt xmax\_i}, {\tt ymin\_i}, and {\tt ymax\_i}. The variable {\tt xmin\_i} ({\tt xmax\_i}) denotes the first (last, respectively) row in which the almost square of order {\tt i} is placed. Similarly, the variable {\tt ymin\_i} ({\tt ymax\_i}) denotes the first (last, respectively) column in which the almost square of order {\tt i} is placed.

The covering of the almost square of order 4 shown above can be expressed using the following assignment to these variables

\begin{itemize}
\item {\tt xmin\_1 = 1}, {\tt xmax\_1 = 2}, {\tt ymin\_1 = 4}, {\tt ymax\_1 = 4}
\item {\tt xmin\_2 = 1}, {\tt xmax\_2 = 2}, {\tt ymin\_2 = 1}, {\tt ymax\_2 = 3}
\item {\tt xmin\_3 = 3}, {\tt xmax\_3 = 5}, {\tt ymin\_3 = 1}, {\tt ymax\_3 = 4}
\end{itemize}

The code fragment below shows the first part of the encoding used to compute the covering. It shows the declaration of the first variables and the first constraints on those variables.

\begin{verbatim}
    (set-logic QF_LIA)
    (declare-const xmin_1 Int)
    (declare-const xmax_1 Int)
    (declare-const ymin_1 Int)
    (declare-const ymax_1 Int)
    ...
    (assert (and (>= xmin_1 1) (<= xmax_1 5)))
    (assert (and (>= ymin_1 1) (<= ymax_1 4)))
    ...
\end{verbatim}

Finish the encoding use the following steps:

\subsubsection* {a) (3 points)} Express constraints that ensure that the almost square of order {\tt i} covers exactly a subgrid of
$n \times (n + 1)$ or $(n + 1) \times n$. The only variables that you can use are {\tt xmin\_i}, {\tt xmax\_i}, {\tt ymin\_i}, and {\tt ymax\_i}. Hint: Split the constraint into three parts with one part that enforces the relation between {\tt xmin\_i} and {\tt xmax\_i}, one part that enforces the relation between {\tt ymin\_i} and {\tt ymax\_i}, and one part that enforces the relation between all four variables.
You will get better results if you express the last part as a conjunction of linear constraints, without using disjunction.

\subsubsection* {b) (3 points)}  For each pair of almost squares, express the constraint that they cannot overlap each other, i.e., there is no cell that is covered by multiple almost squares.

\subsubsection* {c) (3 points)}  Determine a grid assignment showing that the almost squares of orders 1 to 8 can fully cover the almost square of order 15. SMT solvers should be able to quickly solve the intended encoding. Print the grid assignment in a format similar to the grid assignment shown above.

\subsubsection* {d) (3 points)}  Encode the same problem using the theory QF\_BV and compare the runtimes between both theories. It is important to use signed bitvectors. The signed bitverctor operations for $<$, $\leq$, $>$, and $\geq$ are {\tt bvslt}, {\tt bvsle}, {\tt bvsgt}, and {\tt bvsge}, respectively. Addition is {\tt bvadd} and subtraction {\tt bvsub}. The declaration of the variables and the initial bounds for these variables are shown below for $n=3$ and $m=4$. Note that for bitvectors, CVC4/5 are slow, Z3 a bit faster and Boolector is fastest.

\begin{verbatim}
    (set-logic QF_BV)
    (declare-const xmin_1 (_ BitVec 16))
    (declare-const xmax_1 (_ BitVec 16))
    (declare-const ymin_1 (_ BitVec 16))
    (declare-const ymax_1 (_ BitVec 16))
    ...
    (assert (and (bvsge xmin_1 #x0001) (bvsle xmin_1 #x0005)))
    (assert (and (bvsge xmax_1 #x0001) (bvsle xmax_1 #x0005)))
    (assert (and (bvsge ymin_1 #x0001) (bvsle ymin_1 #x0004)))
    (assert (and (bvsge ymax_1 #x0001) (bvsle ymax_1 #x0004)))
    ...
\end{verbatim}

\subsubsection*{e) Bonus point!}

The same encoding can also be used to cover the almost square of order 55 with the almost squares of order 1 to 20. Solving this formula can take minutes. Give it a try.

\subsection*{Problem 2 (6 points)}

Recall from the textbook Smullyan's asylum puzzles, where every inhabitant is a
patient or a doctor, and every inhabitant is either sane or insane.
Everything a sane inhabitant believes is true, and everything an insane
inhabited believes is false. So ``$x$ believes $P$'' can be represented as
$\fn{Sane}(x) \liff P$.

Smullyan's final asylum puzzle runs as follows:

\begin{quote}
The last asylum Craig visited he found to the be the most bizarre of all.
This asylum was run by two doctors named Doctor Tarr and Professor Fether.
There were other doctors on the staff as well.
Now, an inhabitant was called \emph{peculiar} if he believed that he was a patient.
An inhabitant was called \emph{special} if all patients believed he was peculiar
and no doctor believed he was peculiar.
Inspector Craig found out that at least one inhabitant was sane and that the
following condition held:

\emph{Condition C:} Each inhabitant had a best friend in the asylum.
Moreover, given any two inhabitants, $A$ and $B$, if $A$ believed that $B$
was special, then $A$'s best friend believed that $B$ was a patient.

Shortly after this discovery, Inspector Craig had private interviews with
Doctor Tarr and Professor Fether.
Here is the interview with Doctor Tarr:

\emph{Craig:} Tell me, Doctor Tarr, are all the doctors in this asylum sane?

\emph{Tarr:} Of course they are!

\emph{Craig:} What about the patients? Are they all insane?

\emph{Tarr:} At least one of them is.

The second answer struck Craig as a surprisingly modest claim! Of course, if all the
patients are insane, the it certainly is true that at least one is.
But why was Doctor Tarr being so cautious? Craig then had his interview with
Professor Fether, which went as follows:

\emph{Craig:} Doctor Tarr said that at least one patient here is insane. Surely that
is true, isn't it?

\emph{Professor Fether:} Of course it is true! All the patients in this asylum
are insane! What kind of asylum do you think we are running?

\emph{Craig:} What about Doctor Tarr? Is he sane?

\emph{Professor Fether:} Of course he is! How dare you ask me such a question?

At this point, Craig realized the full horror of the situation! What was it?
\end{quote}
Smullyan's solution shows that, under these hypotheses, all the
patients in the asylum are sane and all the doctors are insane.
Using Vampire, however, we were able to prove something stronger,
namely, that the hypotheses themselves are inconsistent.
In other words, no such asylum can possibly exist!

Try doing the same. You can start with these hypotheses:
\begin{lstlisting}
  def last_asylum_hypotheses : List FOForm := [
    fo!{Doctor(Tarr)},
    fo!{Doctor(Fether)},
    fo!{∀ x. Peculiar(%x) ↔ (Sane(%x) ↔ ¬ Doctor(%x))},
    fo!{∀ x. Special(%x) ↔ ∀ y. ¬ Doctor(%y) ↔ (Sane(%y) ↔ Peculiar(%x))},
    fo!{∃ x. Sane(%x)},
    ...
  ]
\end{lstlisting}
You can also introduce a function \lstinline{bf(x)} to denote the best friend of $x$,
and use constants \lstinline{Tarr} and \lstinline{Fether} for those two characters.

(This puzzle is an homage to a story by Edgar Allen Poe called ``The System
of Doctor Tarr and Professor Fether.'')

\end{document}