\documentclass{article} \usepackage{amsmath} \title{Notes on CSP} \author{Will Guaraldi (et al)} \date{version 1.1 10/10/2006} \begin{document} \maketitle 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, Wikipedia, \ldots . \newline \noindent \textbf{VERSIONS} \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. % % SECTION 1 % \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} Our class so far has been concerned 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. I'll go through the section of the tree we're primarily concerned with. \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} 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 2 % \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. 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{variable ordering} - For each variable, we pick an assignment that maximizes the potential solution. \end{itemize} Now we'll go through the algorithms we've used so far. \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} MAXMEAN is defined in the paper Partial Satisfiability SAT II. I reprint it here, but you should refer to the original paper for specifics. Note the invariants $ mean_{-1}(S) = mean_0(S) $ and $ mean_{n+1}(S) = mean_n(S) $. \begin{verbatim} max_assignment := 0 loop compute k such that: mean_k(S) = max (0 <= k' <= n) of mean_k'(S) for all variables x in S do: if mean_k-1(S[x=1]) > mean_k(S[x=0]): J[x] := 1, k := k-1, S := S[x=1] else: J[x] := 0, S := S[x=0] h := SATISFIED(S, J) if h > max_assignment: max_assignment = h else: exit loop end; \end{verbatim} \noindent where: \begin{itemize} \item \textbf{max\_assignment} is the best assignment we've found so far of variables to values. \item \textbf{J[x]} is variable $ x $ in assignment $ J $. \item \textbf{SATISFIED(S, J)} is the number of satisfied clauses in formula $ S $ using assignment $ J $. \item \textbf{$ mean_k(S) $} is the average fraction of satisfied clauses in $ S $ among all assignments having exactly $ k $ ones. Formally, $ mean_k(S) $ is calculated as: $$ mean_k^n(\overrightarrow{t}) = \sum_{i=1}^{m} t_{R_i} SAT_k^N(R_i) $$ \noindent where: \begin{itemize} \item $ R_i $ is a relation R \item $ t_{R_i} $ is the fraction of the clauses in $ S $ that are of relation $ R $. \item $ \overrightarrow{t} $ is the vector of $ t_{R_i} $. \end{itemize} $ SAT_k^N(R_i) $ is calculated as: $$ SAT_k^n(R) = \sum_{s=0}^{r(R)} q_s(R) \frac{(k)_s(n-k)_{r(R)-s}}{(n)_{r(R)}} $$ \end{itemize} MAXMEAN uses the lines: \begin{verbatim} if mean[k-1](S[x=1]) > mean[k](S[x=0]): x = 1 else: x = 0 \end{verbatim} \noindent to make the decision as to whether to set x to 0 or 1. This is called \textbf{value ordering}. \newpage \subsection{Homework 3: APPMEAN} We can approximate $ mean_k^n $ (where $ 0 <= k <= n $) using $ appmean_x $ (where $ 0 <= x <= 1 $ and $ x = k/n $). \begin{eqnarray} appmean_k( \overrightarrow{t} ) & = & \sum_{i=1}^m t_{R_i} appSAT_x(R_i) \\ appSAT_x(R) & = & \sum_{s=0}^{r(R)} q_s(R) x^s (1-x)^{r(R)-s} \end{eqnarray} The parts are similar to $ mean_k(S) $ and $ appmean_k(S) $. Intuitively, the computations for $ mean_k $ have the same structure as $ appmean_x $ where they're both computing a sum of operations on $ R_i $ and $ t_{R_i} $. \end{document}