\documentclass{article}
\usepackage{graphicx}
\usepackage[colorlinks=true,urlcolor=blue,linkcolor=blue,citecolor=blue]{hyperref}%
\usepackage{fancyhdr}
\usepackage[margin=35mm]{geometry}
\usepackage{amsmath}
\usepackage{stmaryrd}   % for the tval symbol
\usepackage{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{trees}
\newcommand{\fn}[1]{\mathrm{#1}}
\newcommand{\append}{\mathbin{+\mkern-10mu+}}
\newcommand{\cons}{\mathbin{::}}
\newcommand{\tval}[1]{\llbracket #1 \rrbracket}
\newcommand{\liff}{\leftrightarrow}
% If you don't have the stmaryrd package, the following substitute will do.
%\newcommand{\tval}[1]{[\![ #1 ]\!]}

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

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


\begin{document}

\bigskip

\begin{center}
{\Large Assignment 6}

\medskip

due 6pm Friday, October 15, 2021
\end{center}

\medskip

\thispagestyle{fancy}

\subsection*{Problem 1 (6 points)}

Recall from the class and the textbook that an \emph{autarky} is an assignment $\tau$
that satisfies all clauses in a CNF formula $\Gamma$ that it touches. A
literal $l$ in a CNF formula $\Gamma$ is called \emph{pure} if $\lnot l$ does not occur in $\Gamma$.
An assignment that sets a pure literal to \emph{true} and leaves all the other variables unassigned is an instance of an autarky.

\medskip


\noindent
A) (3 points) Write in Lean a predicate {\tt isAutarky} that takes an assignment
{$\tau$ : \tt PropAssignment} and a CNF formula  {$\Gamma$ : \tt CnfForm} and returns a Boolean
whether $\tau$ is an autarky for $\Gamma$.

\medskip


\noindent
B) (3 points) Write in Lean a function {\tt getPure} that a CNF formula  {$\Gamma$ : \tt CnfForm} and returns
a {\tt List Lit} of all pure literals in $\Gamma$. The function does not need to find all pure literals until fixpoint,
only the literals the are pure in $\Gamma$.

\subsection*{Problem 2 (12 points)}

In this problem we focus on coloring a $n \times m$ grid with $k$ colors.
Consider all possible rectangles within the grid whose length and width are
at least 2. The goal is to color the grid using $k$ colors so that no such rectangle
has the same color for its four corners. When this is possible, we say that
the $n \times m$ grid is \emph{$k$-colorable while avoiding monochromatic rectangles}. When
using $k$ colors, it is relatively easy to construct a valid $k$-coloring of a $k^2 \times k^2$ grid.
However, only few valid $k$-colorings are known for grids that are larger than $k^2 \times k^2$.
An example of a valid $3$-coloring of the $9 \times 9$ grid is shown below.

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

\noindent
A) (4 points) Write a Lean function that takes as input three natural numbers
$n$, $m$, and $k$, which returns a CNF formula of
Lean data type {\tt CnfForm} which is satisfiable if an only if there
exists a valid $k$-coloring of the $n \times m$ grid, i.e., a coloring without
monochromatic rectangles. (Hint: The
encoding requires two types of clauses. First, each square needs to have one color. Second, if four squares form the corners of a rectangle,
then they cannot have the same color.)

\medskip

\noindent
B) (4 points) Use the Lean interface to CaDiCaL to solve the formula
with $n=10$, $m=10$, and $k=3$ and the formula with $n=9$, $m=12$, and $k=3$.
Both formulas should be satisfiable. The answer should consist of two lists (one for each formula)
using Lean data type {\tt List Lit} containing only all positive literals assigned to true ($\top$).

\medskip

\noindent
C) (4 points) Given a {\tt List Lit} containing only all positive literals assigned to true
for a grid-coloring problem, decode it into a grid of numbers similar to the $9 \times 9$ grid shown above.
Use the function to display the solutions of $n=10$, $m=10$, and $k=3$ and of $n=9$, $m=12$, and $k=3$.
You can assume that the decoding function knows $n$, $m$, and $k$ of the grid-coloring problem.

\end{document}