\documentclass{article}
\usepackage{graphicx}
\usepackage[colorlinks=true,urlcolor=blue,linkcolor=blue,citecolor=blue]{hyperref}
\usepackage{fancyhdr}
\usepackage[margin=35mm]{geometry}

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

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

\begin{document}

\bigskip

\begin{center}
{\Large Assignment 1}

\medskip

due Wednesday, September 17, 2025
\end{center}

\medskip

\thispagestyle{fancy}

The homework is due at 11:59pm on Wednesday, September 17, 2025. Each student has to complete the homework assignment on their own. 
Please submit your homework via Gradescope, see \url{https://www.gradescope.com/courses/1087683}.
Your submission can be a combination of code {\bf with comments}, PDFs, {\bf clearly readable} scans of handwritten answers,
and scripts or screenshots of solver runs. Pages and code are
different assignments within Gradescope. 

The questions below are mostly encoding questions. 
Encoding tools, such as PySAT, are allowed for Question 4. 
We prefer answers that consist of a generator that produces
the requested DIMCAS file in a common programming language, such as Python or C(++). 
Alternatively, you can submit the encoding answers as a \LaTeX~document. 
However, Questions 4(b) and 4(c) can only be solved using a generated DIMACS file. 


\subsection*{Question 1}

Consider the following conjunction of clauses:
\begin{eqnarray*}
1: (a \lor b \lor \overline c) \\
2: (\overline a \lor \overline b \lor c) \\
3: (b \lor c \lor \overline d) \\
4: (\overline b \lor \overline c \lor d) \\
5: (a \lor c \lor d) \\
6: (\overline a \lor \overline c \lor \overline d) \\
7: (\overline a \lor b \lor d) \\
\end{eqnarray*}
\vspace{-35pt}

\paragraph*{(a) [8 points]} Derive all possible unit clauses via resolution. In each step, print the step number (starting with 8) followed by the resolvent and the two clause indices used for resolution. E.g., the first steps could be 
\begin{eqnarray*}
8: (a \lor b \lor \overline d)~~1 + 3\\
9: (b \lor \overline c \lor \overline d)~~6 + 8
\end{eqnarray*}
Hint: work toward producing smaller clauses, in which case 15 resolution steps are enough.

\subsection*{Question 2  \normalsize (no encoding tools allowed)}

Consider the following constraint: $x_1 + x_2 + x_3 + x_4 \leq 1$.

\paragraph*{(a) [4 points]} Express this constraint in disjunctive normal form (DNF). A formula is in DNF if it is written as a disjunction of conjunctions of literals. Do not introduce any auxiliary variables.

\paragraph*{(b) [8 points]} Apply the Tseitin transformation to the answer of (a) to turn it into conjunctive normal form (CNF), i.e., a conjunction of disjuctions of literals. For this question it is required to use auxiliary variables. You are allowed to use the optimizations discussed in class.


\newpage

\subsection*{Question 3 \normalsize (no encoding tools allowed)}

Consider graph $G = (V,E)$ with $V = \{u,v,w,x,y\}$ and $E = \{(u,v), (v,w), (w,x), (x,y), (u,y)\}$.

\paragraph*{(a) [6 points]} Encode whether $G$ can be colored with two colors. Either write out the formula or submit a program that generates the clauses in the DIMACS format. Test whether this formula is satisfiable using a SAT solver.

\paragraph*{(b) [4 points]} Construct a symmetry-breaking predicate in CNF that breaks the color symmetry. 


\subsection*{Question 4 \normalsize}

\paragraph*{(a) [10 points]} Consider a $n \times m$ grid of squares and all possible
rectangles within the grid whose length and width are at least 2. Encode whether
there exists a coloring of the grid using three colors so that no such rectangle has
the same color for its four corners. Submit a program that takes $n$ and $m$ as inputs
and creates a formula in the DIMACS format. (Hint: The encoding requires two types of constraints. 
First, each square needs to have at least one color. Second, if four squares form the 
corners of a rectangle, then they cannot have the same color.)


\begin{figure}[ht]
\begin{minipage}{.33\textwidth}
~
\end{minipage}
\begin{minipage}{.33\textwidth}
\large
\begin{verbatim}
    0 0 1 1 2 2 0 2 1
    1 0 0 1 1 2 2 0 2
    2 1 0 0 1 1 2 2 0
    0 2 1 0 0 1 1 2 2
    2 0 2 1 0 0 1 1 2
    2 2 0 2 1 0 0 1 1
    1 2 2 0 2 1 0 0 1
    1 1 2 2 0 2 1 0 0
    0 1 1 2 2 0 2 1 0
\end{verbatim}
\end{minipage}
\end{figure}

\paragraph*{(b) [5 points]} Solve the encoding for a $10 \times 10$ grid using a SAT solver and decode the 
solution into a valid coloring. Show the output of the SAT solver and a valid 3-coloring similar
to the one above of the $9\times9$ grid.

\paragraph*{(c) [5 points]} Solve the encoding for a $9 \times 12$ grid using a SAT solver and decode the 
solution into a valid coloring. Show the output of the SAT solver and a valid 3-coloring similar
to the one above of the $9\times9$ grid.

\end{document}
