\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}