\documentclass{article}
\usepackage{amsmath}
\title{Notes on CSP}
\author{Will Guaraldi, et al}
\date{version 1.5 10/13/2006}
\begin{document}
\maketitle
\begin{abstract}
This document is a survey of the fundamentals of what we've covered
in the course up to this point.
The information in this document was culled from a variety of sources:
meetings with Professor Lieberherr, research papers we've been given
to read in class (CSG260), Wikipedia, \ldots .
Recent versions of these notes can be found at: \newline
http://www.ccs.neu.edu/home/guaraldi/csg260/
If you have any questions, comments, or find any issues, let Will know
by email sent to \emph{guaraldi at ccs dot neu dot edu}.
\end{abstract}
\tableofcontents
\newpage
%
% SECTION 1
%
\section*{Revision History}
\noindent version 1.5 (10/13/2006) - wbg (major edits) \newline
I added a TOC, moved the revision history to a new page, and
significantly expanded the sections on MAXMEAN, APPMEAN, and SAT Solvers.
\newline
\noindent version 1.1 (10/10/2006) - wbg (minor edits) \newline
Fixed an exponent that was a 5 and should have been an s. Removed
a line from one of the itemized lists that was incomplete and
shouldn't have been there. Moved the $ x = k/n $ to a better
place in the APPMEAN explanation. \newline
\noindent version 1.0 (10/10/2006) - wbg (major edits) \newline
Made a bunch of changes based on Professor Lieberherr's comments. \newline
\noindent version 0.5 (10/08/2006) - wbg (major edits) \newline
First write-up, csp information, precise, maxmean, and appmean.
\newpage
%
% SECTION 2
%
\section{What is CSP?}
Constraint Satisfiability Problems are problems that are formed by a
series of constraints which must be satisfied by an assignment formed
of variables set to values.
\begin{figure}
\begin{verbatim}
CSP
/ \
/ \
continuous discrete
/ \
/ \
Boolean Other domains
/ \ / \
/ \ / \
SAT 1-in-3 ... Domain={1..9}
/ | \ \
/ | \ \
3-SAT | ... Sudoku
2-SAT
\end{verbatim}
\caption{Sketch of CSP family}
\end{figure}
CSG260 has been concerned primarily with the section of the tree
in \emph{figure 1} where the values are discrete (i.e. all whole
numbers), the domain of values is boolean, and the rank of the
constraints is 3.
We talked briefly about CSP problems that are discrete where the
domain of values is not boolean. One such example of this is
Sudoku. We spent some time taking Sudoku and translating the
problem so that it was discrete and the domain of values was
boolean.
This paper covers the section of the tree we're primarily concerned
with along with SAT Solving algorithms.
\subsection{Boolean}
Boolean CSP is any CSP problem where the domain of values is boolean.
For any variable in the CSP, you can set it to either true (1) or
false (0).
\subsubsection{SAT}
SAT is a subset of CSP problems where:
\begin{enumerate}
\item the constraints are formed by literals that are connected by
logical \emph{or}, and
\item the constraints are connected by logical \emph{and}, and
\item the domain of values is $ {0, 1} $
\end{enumerate}
SAT is important because many other NP problems can be converted to
SAT problems and solved using SAT Solvers. There are a variety
of applications that benefit from this: program verification,
electronic design, automation, Bayesian network evaluation,
bioinformatics, \ldots .
The following terms are used when talking about SAT:
\begin{itemize}
\item \textbf{formula} - A specific instance of a CSP problem. A
formula consists of a series of clauses.
\item \textbf{clause} - A formula $ S $ is formed of clauses that
are connected by logical \emph{and}. \textbf{clauses} refer
specifically to SAT whereas \textbf{constraints} refer to
any CSP. For SAT, these two terms are interchangeable.
\item \textbf{literal} - Clauses are formed of literals. A literal
has a variable and is either positive or negative.
\item \textbf{interpretation} - An interpretation is a list of
variable to value assignments that solves the CSP.
\item \textbf{rank} - Rank refers to the number of literals in a clause.
For example: \newline
\begin{tabular}{l l}
Or( x1 x2 x3 ) & rank 3 \\
Or( x1 ) & rank 1 \\
Or( x y ) & rank 2
\end{tabular}
\item \textbf{weight} - Sometimes the clauses we're working with have
a weight associated with them. For example: \newline
\begin{tabular}{l l l}
Or3( x1 x2 x3 ) & : 10 & weight 10 \\
Or1( x1 ) & : 5 & weight 5 \\
Or2( x y ) & : 2 & weight 2
\end{tabular}
Intuitively, a clause with a weight $ w $ is equivalent to having
$ w $ of that clause in the formula of weight $ 1 $.
\item \textbf{3-SAT} - A 3-SAT problem is a SAT problem where the
clauses are restricted to Rank 3 or less.
Some papers use the term ``3-SAT'' to refer to SAT problems where
clauses are of Rank 3, though some papers refer to this as
Exact-3-SAT.
\end{itemize}
SAT problems are usually shown using Conjunctive Normal Form (CNF).
Examples of SAT in CNF:
\begin{verbatim}
X1 or X2 or !X13 or X4 or X10 AND
X21 or X22 or X23 AND
!X32 AND
X14 or !X33 AND ...
\end{verbatim}
Wikipedia adds that all of the following formulas are valid CNF:
\begin{verbatim}
A or B
!A or (B or C)
(A or B) or (!B or C or !D) or (D or E)
(!B or C)
\end{verbatim}
The following are \textbf{NOT} valid CNF:
\begin{verbatim}
!(B or C)
(A and B) or C
A and (B or (D and E))
\end{verbatim}
In class, we've been using syntax like this:
\begin{verbatim}
Or( x1 x2 !x3 ) and
Or( x2 ) and
Or( x1 !x3 )
\end{verbatim}
\noindent or syntax like this where we explicitly specify the
type of the constraints:
\begin{verbatim}
Or3( x1 x2 !x3 ) and
Or1( x2 ) and
Or2( x1 !x3 )
\end{verbatim}
2-SAT and 3-SAT are SAT problems of rank 2 and rank 3 respectively.
Any problem can be reduced to a 3-SAT problem by adding new variables.
\subsubsection{One-in-three}
In the one-in-three CSP problem, only one literal in a clause can
be set to 1:
\begin{verbatim}
x1 + x2 + x3 = 1
x1 + x5 + x6 = 1
x2 + x8 = 1
...
\end{verbatim}
In order to maintain the equality, only one of the literals in each
clause can be equal to 1---the others have to be equal to 0. For
example, if $ x1 $ and $ x2 $ were equal to $ 1 $, then we would have
this:
\begin{verbatim}
x1=x2=1, x3=x5=x6=x8=0
x1 + x2 + x3 = 1 unsatisfied
x1 + x5 + x6 = 1 satisfied
x2 + x8 = 1 satisfied
...
\end{verbatim}
In class, we've been using syntax for specifying one-in-three problems
that looks like this:
\begin{verbatim}
OneInThree( x1 x2 x3 )
OneInThree( x1 x5 x6 )
OneInTwo( x2 x8 )
\end{verbatim}
\noindent where the $ + $ and the $ = 1 $ are implied.
%
% SECTION 3
%
\section{SAT Solving}
SAT is the prototypical NP-complete problem. However, we can
approximate solutions that satisfy the maximum number of clauses
in polynomial time.
This section covers some of the terminology, but it's definitely
a good idea to read The Quest for Efficient Satisfiability Solvers
because it covers all of this in more depth.
SAT Solvers share various properties:
\begin{enumerate}
\item \textbf{complete} - A complete solver can find a solution to
a SAT problem or prove that no such solution exists.
\item \textbf{incomplete} - An incomplete solver can find a solution
to a SAT problem, but it can't distinguish between there being
no solution and the solver's inability to find it.
\item \textbf{randomized algorithm} - A randomized algorithm has
a random element. Running a solver that has a randomized algorithm
on a solution twice may not produce the same results. This is
also referred to as a \textbf{stochastic} algorithm.
\item \textbf{deterministic algorithm} - A deterministic algorithm
has no random elements. Running a solver that has a deterministic
algorithm on a solution multiple times will always produce the
same result.
\end{enumerate}
\begin{tabular}{l | c | c}
& \textbf{complete} & \textbf{incomplete} \\
\hline
\textbf{randomized} & biased coin-flipping with & MAXMEAN* \\
& superresolution & \\
\hline
\textbf{deterministic} & superresolution, precise, & MAXMEAN \\
& MAXMEAN with superresolution &
\end{tabular}
Terminology:
\begin{itemize}
\item \textbf{MAXSAT} - A MAXSAT algorithm produces an interpretation
that satisfies the maximum number of clauses in a SAT formula.
If the clauses have weight, then a MAX algorithm produces an
interpretation that has the maximum weight of satisfied clauses
in the SAT formula.
Similarly, a MAXCSP algorithm produces an interpretation that
satisfies the maximum number of constraints in a CSP formula.
\item \textbf{MAX-3-SAT} - A MAX algorithm that operates on a 3-SAT
problem.
\item \textbf{free variable} - A free variable is a variable that is
unassigned.
\item \textbf{decision} - A decision is any time you assign a value
to a free variable.
\item \textbf{conflicting clause} - A clause that has all its literals
assigned to 0.
\item \textbf{resolvent} - A resolvent is a clause that's generated
by a resolution step. For example if you had two clauses Or(a b) and
Or(!b c) then the resolvent would be Or(a c).
\item \textbf{variable ordering} - The algorithm uses a suitable
ordering of the free variables to decide in which order to set them.
\item \textbf{value ordering} - The algorithm looks at the values
of a variable in order to decide which value to try first.
\end{itemize}
\newpage
\subsection{Homework 2: Precise}
Precise is a recursive algorithm that finds the maximum interpretation
(i.e. satisfying the maximum weight) of a given formula F.
Precise will return an interpretation I that satisfies the maximum
weight of the clauses in f.
The intuition for Precise is:
\begin{verbatim}
P(f)
if f has at least one unassigned variable x
P(f[x=1])
P(f[x=0])
\end{verbatim}
However, this version of Precise will traverse the entire search tree
of $ 2^n $ steps.
For Homework 2, we used a version of Precise that prunes sections of
the tree that we discover aren't worth traversing.
\begin{verbatim}
Input: formula F, interpretation I, weight of unsatisfied clauses WUC
Output: interpretation I and weight of unsatisfied clauses WUC
Before calling Precise the first time, do these setup steps:
I = random assignment for all variables
WUC = total weight of unsatisfied clauses in F using I
Then call Precise:
I, WUC = Precise(F, I, WUC)
function Precise(F, I, WUC) returns I, WUC:
if F is empty (everything is satisfied or unsatisfied):
return I, WUC
v = variable in F
F' = F[v=1]
I' = I[v=1]
WUC' = total weight of unsatisfied clauses in F'
if WUC' < WUC:
I', WUC' = Precise(F', I', WUC')
I = I'
WUC = WUC'
F' = F[v=0]
I' = I[v=0]
WUC' = number of unsatisfied clauses in F'
if WUC' < WUC:
I', WUC' = Precise(F', I', WUC')
I = I'
WUC = WUC'
return I, WUC
\end{verbatim}
\newpage
\subsection{Homework 2: MAXMEAN and MAXMEAN*}
MAXMEAN and MAXMEAN* are defined in the paper Partial Satisfiability
SAT II. This paper covers large portions of it here, but you should
refer to the original paper for specifics.
MAXMEAN is a deterministic algorithm that uses value ordering to
determine which value to assign a variable.
In this section, we use the following notation:
\begin{itemize}
\item \textbf{S} - $ S $ refers to a CSP formula. MAXMEAN works for
SAT problems in CNF as well as OneInThree problems.
\item \textbf{R} - $ R $ refers to a relation of a constraint in
a CSP problem. If you're using CSP problems of rank 3 or less,
then it's convenient to represent $ R $ as an 8-bit number (0
through 255) that specifies which rows of the truth table for x,
y, and z are satisfied. For example:
\begin{verbatim}
row x y z R (!x or y)
--- --------- --------------
1 0 0 0 1 <- satisfied
2 0 0 1 1 <- satisfied
3 0 1 0 1 <- satisfied
4 0 1 1 1 <- satisfied
5 1 0 0 0
6 1 0 1 0
7 1 1 0 1 <- satisfied
8 1 1 1 1 <- satisfied
\end{verbatim}
The $ R $ here is binary number $ 11001111 $ which is $ 207 $ in
decimal. So we could refer to (!x or y) as $ R_207 $.
\end{itemize}
MAXMEAN uses a function $ \mathit{mean}_k^n(S) $ which takes $ k $,
$ n $, and $ S $ as input and returns the average fraction of
satisfied clauses in $ S $ among all assignments having exactly
$ k $ ones.
There are two invariants for $ mean_k^n(S) $:
\begin{itemize}
\item $ \mathit{mean}_{-1}^n(S) = \mathit{mean}_0^n(S) $, and
\item $ \mathit{mean}_{n+1}^n(S) = \mathit{mean}_n^n(S) $
\end{itemize}
Here's the algorithm for maxmean(S):
$$
\begin{array}{l}
\mathit{maxmean}(S): \\
\quad J := \text{empty assignment} \\
\\
\quad \text{compute $ k $ such that:} \\
\quad \mathit{mean}_k^n(S) = \max{0 <= k' <= n} \text{ of }
\mathit{mean}_{k'}^n(S) \\
\\
\quad \text{for all variables $ x $ in $ S $ do:} \\
\quad \quad \text{if } \mathit{mean}_{k-1}^{n-1}(S[x=1]) >
\mathit{mean}_k^{n-1}(S[x=0]): \\
\quad \quad \quad J[x] := 1, k := k-1, S := S[x=1] \\
\quad \quad \text{else:} \\
\quad \quad \quad J[x] := 0, S := S[x=0] \\
\\
\quad \text{return $ J $}
\end{array}
$$
\noindent where:
\begin{itemize}
\item \textbf{$ S[x=0] $} - The formula $ S $ reduced by the assignment
$ x = 0 $.
\item \textbf{$ J $} - An assignment of variables to values.
\item \textbf{$ J[x] $} - Variable $ x $ in assignment $ J $.
\item \textbf{$ \mathit{mean}_k^n(S) $} - The average fraction of
satisfied clauses in $ S $ among all assignments having exactly $ k $
ones out of $ n $ free variables.
\end{itemize}
$ \mathit{mean}_k^n(S) $ is defined as:
$$
\mathit{mean}_k^n(S) = \sum_{i=1}^{m} t_{R_i}(S) \
\mathit{SAT}_k^n(R_i)
$$
\noindent where:
\begin{itemize}
\item $ m $ - The number of clauses in $ S $.
\item $ R_i $ - A relation.
\item $ t_{R_i}(S) $ - The fraction of the clauses in $ S $ that are
of relation $ R $. For example, if there are 10 claues in $ S $
and three of them are relation $ R_5 $, then $ t_{R_5} $ would
be $ \frac{3}{10} $.
\end{itemize}
$ \mathit{SAT}_k^N(R_i) $ is defined as:
$$
\mathit{SAT}_k^n(R) = \sum_{s=0}^{r(R)}
q_s(R) \frac{\binom{k}{s} \binom{(n-k)}{r(R)-s}}{\binom{n}{r(R)}}
$$
\noindent where:
\begin{itemize}
\item \textbf{$ q_s(R) $} is the number of satisfying rows in the truth
table of $ R $ which contain $ s $ ones.
For example, if you had Or(!x y), then the truth table for the
$ R $ for that clause is:
\begin{verbatim}
row x y z R (!x or y)
--- --------- -----------
1 0 0 0 1
2 0 0 1 1
3 0 1 0 1
4 0 1 1 1
5 1 0 0 0
6 1 0 1 0
7 1 1 0 1
8 1 1 1 1
\end{verbatim}
$ R $ is satisfied in rows 1, 2, 3, 4, 7, and 8 because those rows
have values for x and y that satisfy !x or y.
If $ s = 0 $, then $ q_0(R) $ for this truth table would be 1
because row 1 is the only row in the truth table that has zero 1s
and is satisfied.
If $ s = 1 $, then $ q_1(R) $ for this truth table would be 2
because rows 2 and 3 both contain one 1 and are satisfied.
If $ s = 2 $, then $ q_2(R) $ for this truth table would be 2
because rows 4 and 7 both contain two 1s and are satisfied.
We don't compute at $ s = 3 $ because R is of rank 2 (there are
only two literals) and $ \mathit{SAT}_k^n $ is the summation from
$ s = 0 $ to $ r(R) $ which in this case is from 0 to 2.
\item \textbf{$ r(R) $} is the rank of $ R $.
\end{itemize}
The calculation for a binomial coefficient is:
$$
\binom{n}{k} = \frac{n!}{k! \ (n - k)!}
$$
MAXMEAN uses the lines:
$$
\begin{array}{l}
\quad \quad \text{if } \mathit{mean}_{k-1}^{n-1}(S[x=1]) >
\mathit{mean}_k^{n-1}(S[x=0]): \\
\quad \quad \quad J[x] := 1, k := k-1, S := S[x=1] \\
\quad \quad \text{else:} \\
\quad \quad \quad J[x] := 0, S := S[x=0] \\
\end{array}
$$
\noindent to make the decision as to whether to set x to 0 or 1.
This is called \textbf{value ordering}.
MAXMEAN* is defined as:
$$
\begin{array}{l}
\mathit{maxmean*}(S): \\
\quad \text{// max\_satisfied holds the maximum number of satisfied} \\
\quad \text{// clauses we've found so far.} \\
\quad \mathit{max\_satisfied} := 0 \\
\\
\quad \text{// max\_J holds the assignment that satisfies the maximum} \\
\quad \text{// number of clauses} \\
\quad \mathit{max\_J} := \text{empty assignment} \\
\\
\quad \text{loop} \\
\quad \quad J := \mathit{maxmean}(S) \\
\quad \quad h := \mathit{satisfied}(S, J) \\
\\
\quad \quad \text{if } h > \mathit{max\_satisfied}: \\
\quad \quad \quad \mathit{max\_satisfied} = h \\
\quad \quad \quad \mathit{max\_J} = J \\
\quad \quad \text{else}: \\
\quad \quad \quad \text{exit loop} \\
\\
\quad \quad \text{rename all variables in $ S $ which are
assigned $ 1 $ by $ \mathit{max\_J} $} \\
\quad \text{end} \\
\quad \text{return $ \mathit{max\_J} $}
\end{array}
$$
\noindent where:
\begin{itemize}
\item \textbf{satisfied(S, J)} - A function that takes a formula
$ S $ and an assignment $ J $ and returns the number of satisfied
clauses.
\end{itemize}
The Complexity of Partial Satisfaction II paper notes that ``already
after one iteration of the outermost loop of MAXMEAN* the fraction
$ \tau_\psi $ of the clauses is satisfied by assignment $ J $''.
\newpage
\subsection{Homework 3: MAXMEAN\_APPMEAN}
$ mean_k^n(S) $ is computationally intensive. However, we can
approximate $ mean_k^n(S) $ (where $ 0 <= k <= n $) using
$ appmean_x(S) $ (where $ 0 <= x <= 1 $ and $ x = k/n $).
\begin{eqnarray*}
\mathit{appmean}_x(S) & = & \sum_{i=1}^m t_{R_i}(S) \
\mathit{appSAT}_x(R_i) \\
\mathit{appSAT}_x(R) & = & \sum_{s=0}^{r(R)} q_s(R) \ x^s \ (1-x)^{r(R)-s}
\end{eqnarray*}
Intuitively, the computations for $ mean_k^n(S) $ have the same structure
as $ appmean_x(S) $ where they're both computing a sum of operations on
$ R_i $ and $ t_{R_i}(S) $.
Plugging in $ appmean_x(S) $ for $ mean_k^n(S) $, we get:
$$
\begin{array}{l}
\mathit{maxmean\_appmean}(S): \\
\quad J := \text{empty assignment} \\
\\
\quad \text{if } \mathit{maxappmean}_x(S[x=1]) >
\mathit{maxappmean}_x(S[x=0]): \\
\quad \quad J[x] := 1, S := S[x=1] \\
\quad \text{else}: \\
\quad \quad J[x] := 0, S := S[x=0] \\
\quad \text{return } J
\end{array}
$$
\noindent where:
\begin{itemize}
\item \textbf{ $ \mathit{maxappmean}_x(S) $ } -
$ \max{0 <= x <= 1} \mathit{appmean}_x(S) $. To figure this out, you
need to find the polynomial for $ \mathit{appmean}_x(S) $, take the
derivative of it which gives you a polynomial of degree 2. Then you
use the quadratic formula to find the two points where that polynomial
is equal to 0. Then:
$$
\mathit{maxappmean}_x(S) = \max \left\{
\begin{array}{l}
\mathit{appmean}_{point 1}(S) \\
\mathit{appmean}_{point 2}(S) \\
\mathit{appmean}_{0}(S) \\
\mathit{appmean}_{1}(S)
\end{array}
\right .
$$
\item the rest of the notation is defined in the same way it is defined
in the MAXMEAN section.
\end{itemize}
\end{document}