\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 2021}
\begin{document}
\title{Assignment 2}
\author{Marijn Heule}
\date{}
\maketitle
\thispagestyle{fancy}
The second homework is due at 6pm on Wednesday October 6, 2021. Please email your answers
to {\tt marijn@cmu.edu} with subject ``15-816 Homework Assignment 2''.
%The questions below are mostly encoding questions. 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, question 1(d) and question 2 (b) can only
%be solved using a generated DIMACS file.
\subsection*{Question 1}
\paragraph*{(a) [5 points]} Write a DIMACS generator {\tt colorA} $(n)$ for the problem that there exists a 2-coloring of the positive
numbers $1$ to $n$ such that for every integer solution of $a^2 + b^2 = c^2$ with $1 \leq a < b < c \leq n$ holds that $a$, $b$, and $c$
do \emph{not} all have the same color. (Hint 1: use a Boolean variable $x_i$ for each integer. Assigning $x_i$ to true means that $i$ has the first
color, while assigning it to false means that $i$ has the second color. Hint 2: not all variables are required).
\paragraph*{(b) [8 points]} Use the above generator to construct {\tt colorA} $(40)$ and remove all clauses
using blocked clause elimination. In which order can the clauses be removed? Put the blocking literal as the
first literal in each eliminated clause.
\paragraph*{(c) [4 points]} Now, start with the assignment that makes all variables false. Construct a solution of
{\tt colorA} $(40)$ by using the order in which blocked clauses were eliminated. List the variables that are assigned to true in the solution.
\paragraph*{(d) [8 points]} Again use {\tt colorA} $(40)$. Eliminate all clauses using variable elimination (either by distribution or by substitution).
(Hint: the order in which blocked clauses are removed is an effective heuristic for variable elimination.)
\subsection*{Question 2}
\paragraph*{(a) [5 points]} Write a DIMACS generator {\tt colorB} $(n)$ for the problem that there exists a 2-coloring of the positive
numbers $1$ to $n$ such that for every integer solution of $a + b = c$ with $1 \leq a < b < c \leq n$ holds that $a$, $b$, and $c$
do \emph{not} all have the same color.
(Hint: use a Boolean variable $x_i$ for each integer. Assigning $x_i$ to true means that $i$ has the first
color, while assigning it to false means that $i$ has the second color).
\paragraph*{(b) [10 points]} Use the above generator to construct {\tt colorB} $(7)$. Consider the initial steps of
a CDCL solver in which the first decision is $x_1 = 1$ and the second decision is $x_3 = 1$. Now unit propagation
results in a conflict. Draw an {\em implication graph} and compute the first unit implication point of that graph.
This question can be answered by scanning in a drawing of the implication graph.
\paragraph*{(c) [10 points]} Now use {\tt colorB} $(9)$ and construct a DPLL tree by hand (no implementation) to show that this formula is unsatisfiable.
Recall that the vertices of DPLL only consist of decision variables and not variables implied by unit propagation.
Only use unit propagation and chronological backtracking (i.e., no clause learning).
\subsection*{Bonus Question}
Consider the DIMACS formula shown below with 11 variables and 20 clauses, also
available on \url{http://www.cs.cmu.edu/~mheule/15816-f21/bonusQ.cnf}.
Reduce the size of
the formula by introducing new variables. The reduced formula should have the same set of solutions
over the common (i.e., non auxiliary) variables. The number of points for a correct answer is 31 (11+20) minus the sum of the
number of variables and the number of clauses of the reduced formula.
\bigskip
\begin{figure}[ht]
\begin{minipage}{.15\textwidth}
~
\end{minipage}
\begin{minipage}{.33\textwidth}
%\large
\begin{verbatim}
p cnf 11 20
-1 -2 -3 4 -5 6 -7 -8 -9 -10 11 0
-1 -2 3 -4 -5 6 -7 -8 -9 -10 11 0
-1 -2 -3 4 5 -6 -7 -8 -9 -10 11 0
-1 -2 3 -4 5 -6 -7 -8 -9 -10 11 0
-1 -2 -3 4 -5 6 -7 -8 -9 10 -11 0
-1 -2 3 -4 -5 6 -7 -8 -9 10 -11 0
-1 -2 -3 4 5 -6 -7 -8 -9 10 -11 0
-1 -2 3 -4 5 -6 -7 -8 -9 10 -11 0
-1 -2 -3 4 -5 6 7 8 -9 0
-1 -2 3 -4 -5 6 7 8 -9 0
-1 -2 -3 4 5 -6 7 8 -9 0
-1 -2 3 -4 5 -6 7 8 -9 0
1 2 -3 4 -5 6 -7 -8 9 0
1 2 3 -4 -5 6 -7 -8 9 0
1 2 -3 4 5 -6 -7 -8 9 0
1 2 3 -4 5 -6 -7 -8 9 0
1 2 -3 4 -5 6 7 8 9 0
1 2 3 -4 -5 6 7 8 9 0
1 2 -3 4 5 -6 7 8 9 0
1 2 3 -4 5 -6 7 8 9 0
\end{verbatim}
\end{minipage}
\end{figure}
\end{document}