|
| 1 | +\documentclass[t]{sdqbeamer} |
| 2 | +%\documentclass[c]{sdqbeamer} |
| 3 | + |
| 4 | +\usepackage{listings} |
| 5 | +\usepackage{graphicx} |
| 6 | +\usepackage{tabularx} |
| 7 | +\usepackage{tikzsymbols} |
| 8 | + |
| 9 | +\hypersetup{ |
| 10 | + colorlinks=true, |
| 11 | + urlcolor=kit-orange |
| 12 | +} |
| 13 | + |
| 14 | +% set sdqbeamer options |
| 15 | +\titleimage{blender-render} |
| 16 | +\groupname{Algorithm Engineering} |
| 17 | +\grouplogo{ae} |
| 18 | +\selectlanguage{english} |
| 19 | + |
| 20 | +% define title etc.pp. |
| 21 | +\title[SAT Solving]{Practical SAT Solving} |
| 22 | +\subtitle{Lecture 2} |
| 23 | +\author{\underline{Markus Iser}, Dominik Schreiber, Tom\'a\v{s} Balyo} |
| 24 | +\date{April 22, 2024} |
| 25 | + |
| 26 | +% Existing KIT colors: kit-green, kit-blue, kit-red, kit-gray, kit-orange, kit-lightgreen, kit-brown, kit-purple, kit-cyan |
| 27 | +% configure appearance |
| 28 | +\setbeamercolor{block title}{bg=kit-blue} |
| 29 | +\setbeamercolor{block body}{bg=kit-blue!10} |
| 30 | +\setbeamercolor{block title example}{bg=kit-orange} |
| 31 | +\setbeamercolor{block body example}{bg=kit-orange!10} |
| 32 | +\setbeamertemplate{itemize item}{\color{kit-gray}\textbullet} |
| 33 | +\setbeamertemplate{itemize subitem}{\color{kit-gray}\textbullet} |
| 34 | +\setbeamercolor{item projected}{bg=kit-gray, fg=kit-gray} |
| 35 | +\renewcommand{\insertnavigation}[1]{} % remove navigation bar |
| 36 | + |
| 37 | +% define commands |
| 38 | +\input{l00-commands.tex} |
| 39 | +\setlength{\itemsep}{1em} |
| 40 | + |
| 41 | +\begin{document} |
| 42 | + |
| 43 | +\begin{frame} |
| 44 | + \thispagestyle{empty} |
| 45 | + \titlepage |
| 46 | +\end{frame} |
| 47 | + |
| 48 | +\begin{frame}{Overview} |
| 49 | + \begin{block}{Recap. Lecture 1} |
| 50 | + \begin{itemize}\setlength{\itemsep}{1em} |
| 51 | + \item Satisfiability: Propositional Logic, CNF Formulas, NP-completeness, Applications |
| 52 | + \item Examples: Pythagorean Triples, Arithmetic Progressions, k-Colorability |
| 53 | + \item Incremental SAT: IPASIR, Sample Code |
| 54 | + \end{itemize} |
| 55 | + \end{block} |
| 56 | + \begin{block}{Today's Topics} |
| 57 | + \begin{itemize}\setlength{\itemsep}{1em} |
| 58 | + \item Tractable Subclasses |
| 59 | + \item Constraint Encodings |
| 60 | + \item Encoding Techniques |
| 61 | + \end{itemize} |
| 62 | + \end{block} |
| 63 | +\end{frame} |
| 64 | + |
| 65 | +\begin{frame}{Tractable Subclasses} |
| 66 | +\begin{block}{Tractable Subclasses \href{https://doi.org/10.1145/800133.804350}{(cf.~Schaefer, 1978)}} |
| 67 | + \begin{itemize}\setlength{\itemsep}{1em} |
| 68 | + \item \textbf{2-SAT}\\Exactly two literals per clause |
| 69 | + \item \textbf{HORN-SAT}\\At most one positive literal per clause |
| 70 | + \item \textbf{Inverted HORN-SAT}\\At most one negative literal per clause |
| 71 | + \item \textbf{Positive / Negative}\\Literals occur only pure (either positive or negative) |
| 72 | + \item \textbf{XOR-SAT}\\No clauses, only XOR constraints |
| 73 | + \end{itemize} |
| 74 | +\end{block} |
| 75 | +\end{frame} |
| 76 | + |
| 77 | +\begin{frame}{2-SAT} |
| 78 | +Each clause has exactly two literals. |
| 79 | +\begin{example}[2-SAT Formulas] |
| 80 | +\vspace*{-3ex} |
| 81 | +\begin{flalign*} |
| 82 | + F_5 &= \{ \{ x_1, x_2 \}, \{ \overline{x_1}, x_2 \}, \{ x_1, \overline{x_2} \}, \{ \overline{x_1}, \overline{x_2} \} \} &\\ |
| 83 | + F_7 &= \{ \{ \overline{x_1}, x_2 \}, \{ \overline{x_2}, x_3 \}, \{ \overline{x_3}, x_1 \}, \{ x_2, x_4 \}, \{ x_3, x_4 \}, \{ x_1, x_3 \} \} & |
| 84 | +\end{flalign*} |
| 85 | +\end{example} |
| 86 | +\begin{block}{Linear Time Algorithm for 2-SAT \href{https://doi.org/10.1016/0020-0190(79)90002-4}{(cf.~Aspvall et al., 1979)}} |
| 87 | + \begin{itemize}\setlength{\itemsep}{1em} |
| 88 | + \item Construct Implication Graph |
| 89 | + \item Find Strongly Connected Components (SCC) with Tarjan's Algorithm\\ |
| 90 | + Complexity: $\mathcal{O}(n+m)$, where $m$ is the number of clauses |
| 91 | + \item Check for Complementary Literals in the same SCC |
| 92 | + \end{itemize} |
| 93 | +\end{block} |
| 94 | +\end{frame} |
| 95 | + |
| 96 | +% \begin{frame}{How to solve 2-SAT?} |
| 97 | +% \begin{block}{Saturation Algorithm} |
| 98 | +% The resolution saturation algorithm is \highl{polynomial} for 2-SAT. |
| 99 | +% \end{block} |
| 100 | +% \textbf{Proof} |
| 101 | +% \begin{itemize} |
| 102 | +% \item Only 2-literal resolvents are possible |
| 103 | +% \item There are only $\mathcal{O}(n^2)$ 2-literal clauses on $n$ variables |
| 104 | +% \end{itemize} |
| 105 | +% \textbf{Complexity} |
| 106 | +% \begin{itemize} |
| 107 | +% \item Both time and space $\mathcal{O}(n^2)$ |
| 108 | +% \item There exists a \highl{linear algorithm}! \cite{aspvall1979linear} \\($\mathcal{O}(n+m)$, where |
| 109 | +% $m$ is the number of clauses) |
| 110 | +% \end{itemize} |
| 111 | +% \end{frame} |
| 112 | + |
| 113 | +\begin{frame}{Implication Graph} |
| 114 | + An \textbf{implication graph} of a 2-SAT formula $F$ is a \highl{directed graph} with a vertex for each literal of $F$ and 2 edges for each clause $(l_1 \vee l_2)$: $\overline l_1 \rightarrow l_2$ and $\overline l_2 \rightarrow l_1$. |
| 115 | +\begin{example}[Implication Graph] |
| 116 | + \centering |
| 117 | + \vspace*{1ex} |
| 118 | + \begin{columns}[T] |
| 119 | + \begin{column}{0.6\textwidth} |
| 120 | + $F_7 = \{ \{ \overline{x_1}, x_2 \}, \{ \overline{x_2}, x_3 \}, \{ \overline{x_3}, x_1 \}, \{ x_2, x_4 \}, \{ x_3, x_4 \}, \{ x_1, x_3 \} \}$\\[1ex] |
| 121 | + \only<2>{ |
| 122 | + \begin{itemize}\setlength{\itemsep}{1em} |
| 123 | + \item Find \highl{Strongly Connected Components} (SCC) |
| 124 | + \item SCC: There is a path from every vertex to every other vertex |
| 125 | + \item \highl{Tarjan's algorithm} finds SCCs in $\mathcal{O}(|V|+|E|)$ |
| 126 | + \end{itemize} |
| 127 | + } |
| 128 | + \only<3->{ |
| 129 | + \begin{itemize}\setlength{\itemsep}{1em} |
| 130 | + \item If an SCC contains both $x$ and $\overline{x}$, the formula is \highlo{UNSAT} |
| 131 | + \begin{itemize}\setlength{\itemsep}{1ex} |
| 132 | + \item $x$ implies its own negation! |
| 133 | + \item Literals in an SCC must be either all true or all false |
| 134 | + \end{itemize} |
| 135 | + \item<4> What about \highlo{SAT}? How to get a solution? |
| 136 | + \begin{itemize}\setlength{\itemsep}{1ex} |
| 137 | + \item Contract each SCC into one vertex |
| 138 | + \item In reverse topological order, set unassigned literals to \texttt{true}. |
| 139 | + % \item Example: $x_1 = x_2 = x_3 = \texttt{true}$, $x_4 = \texttt{true}$, the rest is already assigned. |
| 140 | + \end{itemize} |
| 141 | + \end{itemize} |
| 142 | + } |
| 143 | + \end{column}% |
| 144 | + \begin{column}{0.3\textwidth} |
| 145 | + \only<1>{\includegraphics[width=.9\textwidth]{figures/l02/impgraph.pdf}} |
| 146 | + \only<2-3>{\includegraphics[width=.9\textwidth]{figures/l02/impgraph-comp.pdf}} |
| 147 | + \only<4>{\includegraphics[width=.9\textwidth]{figures/l02/impgraph-cond.pdf}} |
| 148 | + \end{column} |
| 149 | + \end{columns} |
| 150 | +\end{example} |
| 151 | +\end{frame} |
| 152 | + |
| 153 | + |
| 154 | +\begin{frame}{HornSAT} |
| 155 | + Each clause contains at most one positive literal. |
| 156 | + \begin{example}[Horn Formula] |
| 157 | + Each clause can be written as an implication with \highl{positive literals only and a single consequent}: |
| 158 | + \vspace*{-1ex} |
| 159 | + \begin{flalign*} |
| 160 | + F_6 &= \bigl\{ \{ \overline{x_1}, x_2 \}, \{ \overline{x_1}, \overline {x_2}, x_3 \}, \{ x_1 \} \bigr\} &\\ |
| 161 | + &\equiv \bigl(x_1 \rightarrow x_2\bigr) \wedge \bigl((x_1 \wedge x_2) \rightarrow x_3\bigr) \wedge \bigl(\top \rightarrow x_1\bigr) & |
| 162 | + \end{flalign*} |
| 163 | + \end{example} |
| 164 | + \pause |
| 165 | + \begin{block}{Solving Horn Formulas} |
| 166 | + \begin{itemize} |
| 167 | + \item Propagate until fixpoint |
| 168 | + \item If $\top \rightarrow \bot$ then the formula is \highlo{UNSAT}. Otherwise it is \highl{SAT}. |
| 169 | + \item Construct a satisfying assignment by setting the remaining variables to \texttt{false} |
| 170 | + \end{itemize} |
| 171 | + \end{block} |
| 172 | +\end{frame} |
| 173 | + |
| 174 | +\begin{frame}{Hidden / Renamable / Disguised Horn} |
| 175 | + A CNF formula is \highl{Hidden Horn} if it can be made \highl{Horn} by flipping the polarity of some of its variables. |
| 176 | + \begin{example}[Hidden Horn Formula] |
| 177 | + \vspace*{-3ex} |
| 178 | + \begin{flalign*} |
| 179 | + F_8 = &\{ \{ x_1, x_2, x_4 \}, \{ x_2, \overline{x_4} \}, \{ x_1 \} \} &\\ |
| 180 | + \leadsto &\{ \{ \overline{x_1}, \overline{x_2}, x_4 \}, \{ \overline{x_2}, \overline{x_4} \}, \{ \overline{x_1} \} \} & |
| 181 | + \end{flalign*} |
| 182 | + \end{example} |
| 183 | + \highl{How to recognize} a Hidden Horn formula? \highlo{And how to hard is it?} |
| 184 | + \pause |
| 185 | + \begin{block}{Recognizing Hidden Horn Formula $F$} |
| 186 | + Construct 2-SAT formula $R_F$ that contains the clause $\{l_1, l_2\}$ iff there is a clause $C \in F$ such that $\{l_1, l_2\} \subseteq C$.\\[1ex] |
| 187 | + \begin{itemize}\setlength{\itemsep}{1em} |
| 188 | + \item Example: $R_{F_8} = \{ \{ x_1, x_2 \}, \{ x_1, x_4 \}, \{ x_2, x_4 \}, \{ x_2, \overline{x_4} \} \}$ |
| 189 | + \item If the 2-SAT formula is satisfiable, then $F$ is Hidden Horn |
| 190 | + \item If $x_i = \texttt{true}$ in $\phi$, then $x_i$ needs to be renamed to $\overline x_i$ |
| 191 | + \end{itemize} |
| 192 | + \end{block} |
| 193 | +\end{frame} |
| 194 | + |
| 195 | +\begin{frame}{Mixed Horn} |
| 196 | + A CNF formula is \highl{Mixed Horn} if it contains only binary and Horn clauses. |
| 197 | + \begin{example}[Mixed Horn Formula] |
| 198 | + \vspace*{-3ex} |
| 199 | + \begin{flalign*} |
| 200 | + F_9 = &\{ \{ \overline{x_1}, \overline{x_7}, x_3 \}, \{ \overline{x_2}, \overline{x_4} \}, \{ x_1, x_5 \}, \{ x_3 \} \} & |
| 201 | + \end{flalign*} |
| 202 | + \end{example} |
| 203 | + \highl{How to solve} a Mixed Horn formula? \highlo{And how to hard is it?} |
| 204 | + \pause |
| 205 | + \begin{block}{Mixed Horn is NP-complete} |
| 206 | + \textbf{Proof}: \highl{Reduce SAT} to Mixed Horn SAT |
| 207 | + \begin{itemize}\setlength{\itemsep}{1em} |
| 208 | + \item For each non-Horn non-quadratic clause $C=(l_1 \vee l_2 \vee l_3 \vee \dots)$ |
| 209 | + \begin{itemize}\setlength{\itemsep}{1ex} |
| 210 | + \item for each but one positive $l_i$ $\in C$ introduce a new variable $l'_i$ |
| 211 | + \item replace $l_i$ in $C$ by $\overline{l'_i}$ |
| 212 | + \item add $(l'_i \vee l_i) \wedge (\overline{l'_i} \vee \overline{l_i})$ to establish $l_i = \overline{l'_i}$ |
| 213 | + \end{itemize} |
| 214 | + \end{itemize} |
| 215 | + \end{block} |
| 216 | +\end{frame} |
| 217 | + |
| 218 | +\end{document} |
0 commit comments