\documentclass{article}
\usepackage{graphicx}
\usepackage[colorlinks=true,urlcolor=blue,linkcolor=blue,citecolor=blue]{hyperref}%
\usepackage{fancyhdr}
\usepackage{tikz}
\usepackage{xspace}
\usepackage[margin=35mm]{geometry}
\usepackage{fontawesome5} % for lightbulb icons

% Define commands for ON and OFF bulbs
\newcommand{\lightbulbOn}{{\faLightbulb}\xspace}        % solid bulb = ON
\newcommand{\lightbulbOff}{{\faLightbulb[regular]}\xspace} % outline bulb = OFF


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

\lhead{\sf Automated Reasoning and Satisfiability}
\rhead{\sf Fall 2025}

\begin{document}

\bigskip

\begin{center}
{\Large Assignment 3}

\medskip

due Monday, October 6, 2025
\end{center}


\thispagestyle{fancy}

The third homework is due at 11:59pm on Monday, October 6. No third-party tools/solvers should be used to answer the questions. 
Please submit your homework via Gradescope, see \url{https://www.gradescope.com/courses/1087683}.

\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^2$. 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: i.e., unit propagation results in a satisfying assigment.
List all the clauses that become unit, in the order of becoming 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. Derive the empty clause via resolution. 
(Hint: A unit propagation sequence resulting in a conflict can be turned into resolution steps as shown on slide 10/33 of the ``Proof Systems and Proof Complexity'' lecture)

\newpage

\subsection*{Question 2}

We will use MaxSAT to solve a variant of the Lights Out puzzle. The puzzle is played on a $2 \times 2$ grid of lights, where each light is either ON or OFF. Pressing the switch at cell $(i,j)$ toggles that light along with its orthogonal neighbors (up, down, left, and right). In other words, if a light is ON, it becomes OFF, and vice versa. The objective is to turn \textbf{all lights OFF} while using the \textbf{minimum number of switches}.

Consider the initial configuration below, where 
\lightbulbOn denotes a light that is ON and \lightbulbOff denotes a light that is OFF:

\begin{table}[!h]
\begin{center}
\begin{tabular}{|c|c|}
\hline
\lightbulbOff & \lightbulbOn \\
\hline
\lightbulbOn & \lightbulbOff \\
\hline
\end{tabular}
\end{center}
\caption{Initial position where cells (1,1) and (2,2) have a light that is OFF (\lightbulbOff) and cells (1,2) and (2,1) have a light that is ON (\lightbulbOn).}
\end{table}



\paragraph*{(a) [10 points]} Write a MaxSAT encoding to find the minimum number of switch presses to solve the puzzle. 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{} document. (Hint: The XOR of several variables is true if an odd number of them are true, and false if an even number are true. Consider how this property may determine the final state of each light.)


\paragraph*{(b) [5 points]} Write an assignment to the switch variables that corresponds to an optimal solution of the puzzle.  

\paragraph*{(c) [10 points]} Write a SAT formula that encodes that there is a solution with strictly fewer presses than the one in part (b). Is this formula satisfiable or unsatisfiable? Your solution can be either a DIMACS file or the encoding written in a \LaTeX{} document.  

\end{document}
