\documentclass{article}
\usepackage{graphicx}
\usepackage[colorlinks=true,urlcolor=blue,linkcolor=blue,citecolor=blue]{hyperref}%
\usepackage{fancyhdr}
\usepackage{tikz}
\usepackage{xspace}
\usepackage[margin=35mm]{geometry}
\pagestyle{fancy}
\fancyhf{}
\renewcommand{\headrulewidth}{0pt}
\lhead{\sf Automated Reasoning and Satisfiability}
\rhead{\sf Fall 2021}
\begin{document}
\title{Assignment 3}
\author{Marijn Heule}
\date{}
\maketitle
\thispagestyle{fancy}
The third homework is due at 6pm on Monday, October 18. No third-party tools/solvers should be used to answer the questions.
Please email your answers to {\tt marijn@cmu.edu} with subject ``15-816: Homework Assignment 3''.
\newcounter{row}
\newcounter{col}
\newcommand\setrow[4]{
\setcounter{col}{1}
\foreach \n in {#1, #2, #3, #4} {
\edef\x{\value{col} - 0.5}
\edef\y{4.5 - \value{row}}
\node[anchor=center] at (\x, \y) {\n};
\stepcounter{col}
}
\stepcounter{row}
}
\newcommand\setrowB[9]{
\setcounter{col}{1}
\foreach \n in {#1, #2, #3, #4, #5, #6, #7, #8, #9} {
\edef\x{\value{col} - 0.5}
\edef\y{9.5 - \value{row}}
\node[anchor=center] at (\x, \y) {\n};
\stepcounter{col}
}
\stepcounter{row}
}
\subsection*{Question 1}
An $n$-Sudoku puzzle consists of grid with $n^2 \times n^2$ cells with some of the cells assigned a
number in between $1$ and $n$. The solve the puzzle, all cells need to be numbered using the following constraints:
In each row, column, and $n \times n$ subgrids the numbers $1$ to $n^2$ occur exactly once. Moreover, an
$n$-Sudoku puzzle is valid if there exists exactly one assignment to the cells that satisfies these
constraints.
\paragraph*{(a) [10 points]} Write a generic DIMACS generator for $n$-Sudoku puzzles, i.e., without the initial numbers.
\paragraph*{(b) [5 points]} Consider the three $2$-Sudoku puzzles below. Which one(s) can be solved by unit propagation?
Pick one puzzle that can be solved with unit propagation. List all the clauses that become unit with the unit literal (the literal
that is forced to true) occurring as the first literal in the clause.
\begin{figure}[ht]
\centering
\begin{tikzpicture}[scale=0.8]
\draw (0, 0) grid (4, 4);
\draw[very thick, scale=2] (0, 0) grid (2, 2);
\setcounter{row}{1}
\setrow {2}{ } { }{ }
\setrow { }{ } {3}{ }
\setrow { }{} { }{1}
\setrow { }{} {2}{ }
\end{tikzpicture}
~~~~~
\begin{tikzpicture}[scale=0.8]
\draw (0, 0) grid (4, 4);
\draw[very thick, scale=2] (0, 0) grid (2, 2);
\setcounter{row}{1}
\setrow {2}{ } { }{ }
\setrow { }{ } {3}{ }
\setrow { }{} { }{1}
\setrow { }{1} { }{ }
\end{tikzpicture}
~~~~~
\begin{tikzpicture}[scale=0.8]
\draw (0, 0) grid (4, 4);
\draw[very thick, scale=2] (0, 0) grid (2, 2);
\setcounter{row}{1}
\setrow {2}{ } { }{ }
\setrow { }{ } {3}{ }
\setrow { }{} { }{1}
\setrow { }{3} { }{ }
\end{tikzpicture}
\end{figure}
\paragraph*{(c) [5 points]} Consider the three $2$-Sudoku puzzles above.
Which one(s) are satisfiable? Provide all satisfying assignments for all puzzles as a list of literals that are true. Which one(s) are valid?
\paragraph*{(d) [5 points]} The right 2-Sudoku is unsatisfiable. Construct a resolution proof that derives the empty clause.
(Hint: The unit propagation sequence can be turned into resolution proof as shown on slide 10 of the ``Proof Systems and Proof Complexity'' lecture)
\subsection*{Question 2}
\paragraph*{(a) [10 points]} Consider the maze depicted below:
\begin{center}
\begin{tikzpicture}
\draw (0,0) grid (3,3);
\draw[fill=black] (1,1) rectangle (2,2);
\node at (0.5,2.5) (a) {$S$};
\node at (1.5,2.5) (a) {$x_1$};
\node at (2.5,2.5) (a) {$x_2$};
\node at (0.5,1.5) (a) {$x_3$};
\node at (2.5,1.5) (a) {$x_4$};
\node at (0.5,0.5) (a) {$x_5$};
\node at (1.5,0.5) (a) {$G$};
\node at (2.5,0.5) (a) {$x_6$};
\end{tikzpicture}
\end{center}
Write a MaxSAT encoding to find the shortest path from $S$ to $G$ considering that you can only move either vertically or horizontally. Note that the black square should be seen as a wall and cannot be part of the path. What are the soft and hard clauses of your encoding? Your solution can be either a WCNF file or the encoding written in a \LaTeX\xspace document.
\paragraph*{Hints:}
\begin{itemize}
\item You may want to have a Boolean variable for each square, denoting if that square will be part of the shortest path.
\item You can encode path connectivity by ensuring that: (i) S and G must have exactly one visited neighbor, (ii) other visited squares must have exactly two visited neighbors.
\end{itemize}
\paragraph*{(b) [5 points]} Write an assignment to the problem variables that corresponds to the shortest path from $S$ to $G$.
\paragraph*{(c) [10 points]} Write a SAT formula that encodes that no shorter path exists for this maze, i.e. that the assignment in \textbf{(2b)} is an optimal solution to the MaxSAT formula. Is this formula satisfiable or unsatisfiable? Your solution can be either a DIMACS file or the encoding written in a \LaTeX\xspace document. (Hint: recall the relaxation variables introduced by MaxSAT algorithms.)
\end{document}