\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 2022}

\begin{document}

\bigskip

\begin{center}
{\Large Assignment 11}

\medskip

Wednesday, December 7
\end{center}

\medskip

\thispagestyle{fancy}

\noindent This is the last assignment of the semester.
These problems require you to use an SMT solver (Z3, CVC4, or CVC5) and a
first-order theorem prover (Vampire). The lamr github 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}

Use Vampire to verify each of these inferences. As a reality check, also make
sure that Vampire cannot refute the hypotheses.

\subsubsection*{a) (4 points)}

Consider these hypotheses:
\begin{enumerate}
 \item Every honest and industrious person is healthy.
 \item No grocer is healthy.
 \item Every industrious grocer is honest.
 \item Every cyclist is industrious.
 \item Every unhealthy cyclist is dishonest.
\end{enumerate}
Show that these imply that no grocer is a cyclist.

\subsubsection*{b) (4 points)}

Consider these hypotheses:
\begin{enumerate}
  \item Wolves, foxes, birds, caterpillars, and snails are animals, and there
  are some of each of them.
  \item There are some grains, and grains are plants.
  \item Every animal either likes to eat all plants or all animals smaller than
  itself that like to eat some plants.
  \item Caterpillars and snails are smaller than birds,
  which are smaller than foxes, which in turn are smaller than wolves.
  \item Wolves do not like to eat foxes or grains, while birds like to eat caterpillars
  but not snails.
  \item Caterpillars and snails like to eat some plants.
\end{enumerate}
Show that these imply that there is an animal that likes to eat an animal that eats grains.

\end{document}
