From 57f6812be145949f0dd9f442d41156e06c416e09 Mon Sep 17 00:00:00 2001 From: nianze Date: Mon, 24 May 2021 11:19:16 +0800 Subject: [PATCH] Add discussion of DPMC and ProCount - In slides: move the SSAT-encoding table back to related work --- Talks/oral_defense/background/ssat.tex | 319 +++++++++---------- Talks/oral_defense/preamble.tex | 142 +++++---- Talks/oral_defense/prob.bib | 24 ++ Talks/oral_defense/related-work/counting.tex | 81 +++-- paper/preamble.tex | 2 + paper/prob.bib | 42 +++ paper/related-work/model-counting.tex | 15 +- 7 files changed, 355 insertions(+), 270 deletions(-) diff --git a/Talks/oral_defense/background/ssat.tex b/Talks/oral_defense/background/ssat.tex index a16bec6..b4c71f5 100644 --- a/Talks/oral_defense/background/ssat.tex +++ b/Talks/oral_defense/background/ssat.tex @@ -1,178 +1,161 @@ \begin{frame} - \frametitle{Background} - \begin{block}{Stochastic Boolean Satisfiability (SSAT)} - $\Qf=Q_1 x_1,\ldots,Q_n x_n.\pf$ - \pause - \begin{itemize} - \item $Q_1 x_1,\ldots,Q_n x_n$: quantification structure, $Q_i \in \{\random{p},\exists\}$ (\emph{prefix}) - \pause - \item $\pf$: quantifier-free formula over $\{x_1,\ldots,x_n\}$ (\emph{matrix}) - \end{itemize} - \end{block} - \pause - \begin{block}{Computational Rules for Satisfying Probability} - Let $x$ be the outermost variable in the prefix: - \pause - \begin{enumerate} - \item[a)] $\spb{\top}=1$, - \pause - \item[b)] $\spb{\bot}=0$, - \pause - \item[c)] $\spb{\Qf}=\max\{\spb{\ncf{\Qf}{x}},\spb{\pcf{\Qf}{x}}\}$, if $x$ is quantified by $\exists$, - \pause - \item[d)] $\spb{\Qf}=(1-p)\spb{\ncf{\Qf}{x}}+p\spb{\pcf{\Qf}{x}}$, if $x$ is quantified by $\random{p}$. - \end{enumerate} - \end{block} + \frametitle{Background} + \begin{block}{Stochastic Boolean Satisfiability (SSAT)} + $\Qf=Q_1 x_1,\ldots,Q_n x_n.\pf$ + \pause + \begin{itemize} + \item $Q_1 x_1,\ldots,Q_n x_n$: quantification structure, $Q_i \in \{\random{p},\exists\}$ (\emph{prefix}) + \pause + \item $\pf$: quantifier-free formula over $\{x_1,\ldots,x_n\}$ (\emph{matrix}) + \end{itemize} + \end{block} + \pause + \begin{block}{Computational Rules for Satisfying Probability} + Let $x$ be the outermost variable in the prefix: + \pause + \begin{enumerate} + \item[a)] $\spb{\top}=1$, + \pause + \item[b)] $\spb{\bot}=0$, + \pause + \item[c)] $\spb{\Qf}=\max\{\spb{\ncf{\Qf}{x}},\spb{\pcf{\Qf}{x}}\}$, if $x$ is quantified by $\exists$, + \pause + \item[d)] $\spb{\Qf}=(1-p)\spb{\ncf{\Qf}{x}}+p\spb{\pcf{\Qf}{x}}$, if $x$ is quantified by $\random{p}$. + \end{enumerate} + \end{block} \end{frame} \begin{frame} - \frametitle{Background} - \begin{block}{Example: Computation of Satisfying Probability} - \abovedisplayskip=0pt - \begin{align*} - & \Qf=\random{0.5} x_1, \exists y_1, \random{0.5} x_2, \exists y_2. \pf \\ - & \pf=(x_1 \lor \lnot y_1) - (\lnot x_1 \lor y_1) - (\lnot x_1 \lor \lnot x_2 \lor y_2) - (x_1 \lor \lnot y_2) - (x_2 \lor \lnot y_2) - \end{align*} - \end{block}\pause - \begin{figure} - \centering - \begin{tikzpicture}[ - baseline, - level distance=10mm, - level 1/.style={sibling distance=10em}, - level 2/.style={sibling distance=5em}, - level 3/.style={sibling distance=7em}, - level 4/.style={sibling distance=5em}, - every node/.style={solid,draw}, - positive/.style={edge from parent/.style={solid,draw}}, - negative/.style={edge from parent/.style={dashed,draw}}] + \frametitle{Background} + \begin{block}{Example: Computation of Satisfying Probability} + \abovedisplayskip=0pt + \begin{align*} + & \Qf=\random{0.5} x_1, \exists y_1, \random{0.5} x_2, \exists y_2. \pf \\ + & \pf=(x_1 \lor \lnot y_1) + (\lnot x_1 \lor y_1) + (\lnot x_1 \lor \lnot x_2 \lor y_2) + (x_1 \lor \lnot y_2) + (x_2 \lor \lnot y_2) + \end{align*} + \end{block}\pause + \begin{figure} + \centering + \begin{tikzpicture}[ + baseline, + level distance=10mm, + level 1/.style={sibling distance=10em}, + level 2/.style={sibling distance=5em}, + level 3/.style={sibling distance=7em}, + level 4/.style={sibling distance=5em}, + every node/.style={solid,draw}, + positive/.style={edge from parent/.style={solid,draw}}, + negative/.style={edge from parent/.style={dashed,draw}}] - \action<2>{\node{$\random{0.5} x_1$};} - \action<3>{\node{$\random{0.5} x_1$} - child[negative]{node{$\exists y_1$}} - child[positive]{node{$\exists y_1$}};} - \action<4>{\node{$\random{0.5} x_1$} - child[negative]{node{$\exists y_1$} - child[negative]{node{$\random{0.5} x_2$}} - child[positive]{node{$0$}}} - child[positive]{node{$\exists y_1$}};} - \action<5>{\node{$\random{0.5} x_1$} - child[negative]{node{$\exists y_1$} - child[negative]{node{$\random{0.5} x_2$}} - child[positive]{node{$0$}}} - child[positive]{node{$\exists y_1$} - child[negative]{node{$0$}} - child[positive]{node{$\random{0.5} x_2$}}};} - \action<6>{\node{$\random{0.5} x_1$} - child[negative]{node{$\exists y_1$} - child[negative]{node{$\random{0.5} x_2$} - child[negative]{node{$\exists y_2$} - child[negative]{node{$1$}} - child[positive]{node{$0$}}} - child[positive]{node{$\exists y_2$} - child[negative]{node{$1$}} - child[positive]{node{$0$}}}} - child[positive]{node{$0$}}} - child[positive]{node{$\exists y_1$} - child[negative]{node{$0$}} - child[positive]{node{$\random{0.5} x_2$}}};} - \action<7>{\node{$\random{0.5} x_1$} - child[negative]{node{$\exists y_1$} - child[negative]{node{$\random{0.5} x_2$} - child[negative]{node{$\exists y_2$} - child[negative]{node{$1$}} - child[positive]{node{$0$}}} - child[positive]{node{$\exists y_2$} - child[negative]{node{$1$}} - child[positive]{node{$0$}}}} - child[positive]{node{$0$}}} - child[positive]{node{$\exists y_1$} - child[negative]{node{$0$}} - child[positive]{node{$\random{0.5} x_2$} - child[negative]{node{$\exists y_2$} - child[negative]{node{$1$}} - child[positive]{node{$0$}}} - child[positive]{node{$\exists y_2$} - child[negative]{node{$0$}} - child[positive]{node{$1$}}}}};} - \action<8>{\node{$\random{0.5} x_1$} - child[negative]{node{$\exists y_1$} - child[negative]{node{$\random{0.5} x_2$} - child[negative]{node{$1$}} - child[positive]{node{$1$}}} - child[positive]{node{$0$}}} - child[positive]{node{$\exists y_1$} - child[negative]{node{$0$}} - child[positive]{node{$\random{0.5} x_2$} - child[negative]{node{$1$}} - child[positive]{node{$1$}}}};} - \action<9>{\node{$\random{0.5} x_1$} - child[negative]{node{$\exists y_1$} + \action<2>{\node{$\random{0.5} x_1$};} + \action<3>{\node{$\random{0.5} x_1$} + child[negative]{node{$\exists y_1$}} + child[positive]{node{$\exists y_1$}};} + \action<4>{\node{$\random{0.5} x_1$} + child[negative]{node{$\exists y_1$} + child[negative]{node{$\random{0.5} x_2$}} + child[positive]{node{$0$}}} + child[positive]{node{$\exists y_1$}};} + \action<5>{\node{$\random{0.5} x_1$} + child[negative]{node{$\exists y_1$} + child[negative]{node{$\random{0.5} x_2$}} + child[positive]{node{$0$}}} + child[positive]{node{$\exists y_1$} + child[negative]{node{$0$}} + child[positive]{node{$\random{0.5} x_2$}}};} + \action<6>{\node{$\random{0.5} x_1$} + child[negative]{node{$\exists y_1$} + child[negative]{node{$\random{0.5} x_2$} + child[negative]{node{$\exists y_2$} + child[negative]{node{$1$}} + child[positive]{node{$0$}}} + child[positive]{node{$\exists y_2$} + child[negative]{node{$1$}} + child[positive]{node{$0$}}}} + child[positive]{node{$0$}}} + child[positive]{node{$\exists y_1$} + child[negative]{node{$0$}} + child[positive]{node{$\random{0.5} x_2$}}};} + \action<7>{\node{$\random{0.5} x_1$} + child[negative]{node{$\exists y_1$} + child[negative]{node{$\random{0.5} x_2$} + child[negative]{node{$\exists y_2$} + child[negative]{node{$1$}} + child[positive]{node{$0$}}} + child[positive]{node{$\exists y_2$} + child[negative]{node{$1$}} + child[positive]{node{$0$}}}} + child[positive]{node{$0$}}} + child[positive]{node{$\exists y_1$} + child[negative]{node{$0$}} + child[positive]{node{$\random{0.5} x_2$} + child[negative]{node{$\exists y_2$} + child[negative]{node{$1$}} + child[positive]{node{$0$}}} + child[positive]{node{$\exists y_2$} + child[negative]{node{$0$}} + child[positive]{node{$1$}}}}};} + \action<8>{\node{$\random{0.5} x_1$} + child[negative]{node{$\exists y_1$} + child[negative]{node{$\random{0.5} x_2$} + child[negative]{node{$1$}} + child[positive]{node{$1$}}} + child[positive]{node{$0$}}} + child[positive]{node{$\exists y_1$} + child[negative]{node{$0$}} + child[positive]{node{$\random{0.5} x_2$} + child[negative]{node{$1$}} + child[positive]{node{$1$}}}};} + \action<9>{\node{$\random{0.5} x_1$} + child[negative]{node{$\exists y_1$} + child[negative]{node{$1$}} + child[positive]{node{$0$}}} + child[positive]{node{$\exists y_1$} + child[negative]{node{$0$}} + child[positive]{node{$1$}}};} + \action<10>{\node{$\random{0.5} x_1$} child[negative]{node{$1$}} - child[positive]{node{$0$}}} - child[positive]{node{$\exists y_1$} - child[negative]{node{$0$}} - child[positive]{node{$1$}}};} - \action<10>{\node{$\random{0.5} x_1$} - child[negative]{node{$1$}} - child[positive]{node{$1$}};} - \action<11>{\node{$\spb{\Qf}=1$};} - \end{tikzpicture} - \end{figure} + child[positive]{node{$1$}};} + \action<11>{\node{$\spb{\Qf}=1$};} + \end{tikzpicture} + \end{figure} \end{frame} \begin{frame} - \frametitle{Express Model-Counting Variants with SSAT} - \begin{table}[t] - \centering - \begin{tabular}{c|c} - Variant & SSAT encoding \\ - \hline - Unweighted & $\random{0.5}x_1,\ldots,\random{0.5}x_n.\pf$ \\ - Weighted & $\random{p_1}x_1,\ldots,\random{p_n}x_n.\pf$ \\ - Projected & $\random{0.5}x_1,\ldots,\random{0.5}x_n,\exists y_1,\ldots,\exists y_m.\pf$ \\ - Maximum & $\exists x_1,\ldots,\exists x_n,\random{0.5}y_1,\ldots,\random{0.5}y_m.\pf$ \\ - Weighted projected & $\random{p_1}x_1,\ldots,\random{p_n}x_n,\exists y_1,\ldots,\exists y_m.\pf$ \\ - Weighted maximum & $\exists x_1,\ldots,\exists x_n,\random{p_1}y_1,\ldots,\random{p_m}y_m.\pf$ \\ - \end{tabular} - \end{table} -\end{frame} - -\begin{frame} - \frametitle{Background} - \begin{block}{Game-Theoretical Interpretation of SSAT} - $\Qf=Q_1 x_1,\ldots,Q_n x_n.\pf$, $Q_i \in \{\random{p},\exists\}$ - \pause - \begin{itemize} - \item $\random{p}$: nondeterministic factors - \pause - \item $\exists$: an agent who plays under uncertainty - \pause - \item $\pf$: game matrix - \pause - \item $\spb{\Qf}$: the maximum winning probability of the agent - \pause - \item \alert{Skolem functions}: a winning/optimization strategy of the agent - \end{itemize} - \end{block}\pause - \begin{block}{Example: Skolem Functions} - \abovedisplayskip=0pt - \belowdisplayskip=0pt - \begin{align*} - & \Qf=\random{0.5} x_1, \exists y_1, \random{0.5} x_2, \exists y_2. \pf \\ - & \pf=(x_1 \lor \lnot y_1) - (\lnot x_1 \lor y_1) - (\lnot x_1 \lor \lnot x_2 \lor y_2) - (x_1 \lor \lnot y_2) - (x_2 \lor \lnot y_2) - \end{align*} - \pause - \begin{itemize} - \item Variable $y_1$: $f_1(x_1)=x_1$; variable $y_2$: $f_2(x_1,x_2)=x_1 \land x_2$ - \end{itemize} - \end{block} + \frametitle{Background} + \begin{block}{Game-Theoretical Interpretation of SSAT} + $\Qf=Q_1 x_1,\ldots,Q_n x_n.\pf$, $Q_i \in \{\random{p},\exists\}$ + \pause + \begin{itemize} + \item $\random{p}$: nondeterministic factors + \pause + \item $\exists$: an agent who plays under uncertainty + \pause + \item $\pf$: game matrix + \pause + \item $\spb{\Qf}$: the maximum winning probability of the agent + \pause + \item \alert{Skolem functions}: a winning/optimization strategy of the agent + \end{itemize} + \end{block}\pause + \begin{block}{Example: Skolem Functions} + \abovedisplayskip=0pt + \belowdisplayskip=0pt + \begin{align*} + & \Qf=\random{0.5} x_1, \exists y_1, \random{0.5} x_2, \exists y_2. \pf \\ + & \pf=(x_1 \lor \lnot y_1) + (\lnot x_1 \lor y_1) + (\lnot x_1 \lor \lnot x_2 \lor y_2) + (x_1 \lor \lnot y_2) + (x_2 \lor \lnot y_2) + \end{align*} + \pause + \begin{itemize} + \item Variable $y_1$: $f_1(x_1)=x_1$; variable $y_2$: $f_2(x_1,x_2)=x_1 \land x_2$ + \end{itemize} + \end{block} \end{frame} \ No newline at end of file diff --git a/Talks/oral_defense/preamble.tex b/Talks/oral_defense/preamble.tex index 3161582..e9b31c8 100644 --- a/Talks/oral_defense/preamble.tex +++ b/Talks/oral_defense/preamble.tex @@ -27,16 +27,16 @@ % Plots with BenchExec \usepackage{standalone} \usepackage[ - group-digits=integer, group-minimum-digits=4, % group digits by thousands - free-standing-units, unit-optional-argument, % easier input of numbers with units + group-digits=integer, group-minimum-digits=4, % group digits by thousands + free-standing-units, unit-optional-argument, % easier input of numbers with units ]{siunitx} \usepackage{pgfplots} \pgfplotsset{ - compat=1.9, - %log ticks with fixed point, % no scientific notation in plots - table/col sep=tab, % only tabs are column separators - unbounded coords=jump, % better have skips in a plot than appear to be interpolating - filter discard warning=false, % Don't complain about empty cells + compat=1.9, + %log ticks with fixed point, % no scientific notation in plots + table/col sep=tab, % only tabs are column separators + unbounded coords=jump, % better have skips in a plot than appear to be interpolating + filter discard warning=false, % Don't complain about empty cells } \SendSettingsToPgf % use siunitx formatting settings in PGF, too % end packages @@ -95,6 +95,8 @@ \definetool{\minisat}{MiniSat} \definetool{\cachet}{Cachet} \definetool{\approxmc}{ApproxMC} +\definetool{\dpmc}{DPMC} +\definetool{\procount}{ProCount} \definetool{\cnfgen}{CNFgen} \definetool{\benchexec}{BenchExec} \definetool{\abc}{ABC} @@ -144,61 +146,61 @@ % customize package "pgfplotstable" \pgfplotstableset{ - circuit column/.style={ - /pgfplots/table/display columns/#1/.style={ - string type,column type=l,column name=\textsc{Circuit} - } - }, - formula column/.style={ - /pgfplots/table/display columns/#1/.style={ - string type,column type=l,column name=\textsc{Formula} - } - }, - pi column/.style={ - /pgfplots/table/display columns/#1/.style={fixed,column type=r,column name=\#PI} - }, - ai column/.style={ - /pgfplots/table/display columns/#1/.style={fixed,column type=r,column name=\#AI} - }, - po column/.style={ - /pgfplots/table/display columns/#1/.style={fixed,column type=r,column name=\#PO} - }, - and column/.style={ - /pgfplots/table/display columns/#1/.style={fixed,column type=r,column name=\#And} - }, - level column/.style={ - /pgfplots/table/display columns/#1/.style={fixed,column type=r,column name=\#Level} - }, - time column/.style={ - /pgfplots/table/display columns/#1/.style={ - string replace={nan}{},fixed,fixed zerofill,dec sep align,precision=2,column name=T (s) - } - }, - prob column/.style={ - /pgfplots/table/display columns/#1/.style={ - string replace={nan}{},sci,sci zerofill,sci sep align,precision=2,sci e,column name=$\Pr$ - } - }, - ubound column/.style={ - /pgfplots/table/display columns/#1/.style={ - string replace={nan}{},sci,sci zerofill,sci sep align,precision=2,sci e,column name=UB - } - }, - lbound column/.style={ - /pgfplots/table/display columns/#1/.style={ - string replace={nan}{},sci,sci zerofill,sci sep align,precision=2,sci e,column name=LB - } - }, - ubtime column/.style={ - /pgfplots/table/display columns/#1/.style={ - string replace={nan}{},fixed,fixed zerofill,dec sep align,precision=2,column name=T-UB (s) - } - }, - lbtime column/.style={ - /pgfplots/table/display columns/#1/.style={ - string replace={nan}{},fixed,fixed zerofill,dec sep align,precision=2,column name=T-LB (s) - } - } + circuit column/.style={ + /pgfplots/table/display columns/#1/.style={ + string type,column type=l,column name=\textsc{Circuit} + } + }, + formula column/.style={ + /pgfplots/table/display columns/#1/.style={ + string type,column type=l,column name=\textsc{Formula} + } + }, + pi column/.style={ + /pgfplots/table/display columns/#1/.style={fixed,column type=r,column name=\#PI} + }, + ai column/.style={ + /pgfplots/table/display columns/#1/.style={fixed,column type=r,column name=\#AI} + }, + po column/.style={ + /pgfplots/table/display columns/#1/.style={fixed,column type=r,column name=\#PO} + }, + and column/.style={ + /pgfplots/table/display columns/#1/.style={fixed,column type=r,column name=\#And} + }, + level column/.style={ + /pgfplots/table/display columns/#1/.style={fixed,column type=r,column name=\#Level} + }, + time column/.style={ + /pgfplots/table/display columns/#1/.style={ + string replace={nan}{},fixed,fixed zerofill,dec sep align,precision=2,column name=T (s) + } + }, + prob column/.style={ + /pgfplots/table/display columns/#1/.style={ + string replace={nan}{},sci,sci zerofill,sci sep align,precision=2,sci e,column name=$\Pr$ + } + }, + ubound column/.style={ + /pgfplots/table/display columns/#1/.style={ + string replace={nan}{},sci,sci zerofill,sci sep align,precision=2,sci e,column name=UB + } + }, + lbound column/.style={ + /pgfplots/table/display columns/#1/.style={ + string replace={nan}{},sci,sci zerofill,sci sep align,precision=2,sci e,column name=LB + } + }, + ubtime column/.style={ + /pgfplots/table/display columns/#1/.style={ + string replace={nan}{},fixed,fixed zerofill,dec sep align,precision=2,column name=T-UB (s) + } + }, + lbtime column/.style={ + /pgfplots/table/display columns/#1/.style={ + string replace={nan}{},fixed,fixed zerofill,dec sep align,precision=2,column name=T-LB (s) + } + } } % Fix line counters if multiple algorithms exist @@ -226,16 +228,16 @@ \AtBeginSection[] { - \begin{frame} - \frametitle{Outline} - \tableofcontents[currentsection,hideallsubsections] - \end{frame} + \begin{frame} + \frametitle{Outline} + \tableofcontents[currentsection,hideallsubsections] + \end{frame} } \AtBeginSubsection[] { - \begin{frame} - \frametitle{Outline} - \tableofcontents[currentsection,currentsubsection,subsectionstyle=show/shaded/hide] - \end{frame} + \begin{frame} + \frametitle{Outline} + \tableofcontents[currentsection,currentsubsection,subsectionstyle=show/shaded/hide] + \end{frame} } \ No newline at end of file diff --git a/Talks/oral_defense/prob.bib b/Talks/oral_defense/prob.bib index 3efdc1a..6d4a023 100644 --- a/Talks/oral_defense/prob.bib +++ b/Talks/oral_defense/prob.bib @@ -518,6 +518,30 @@ @article{MC-COMP2020 eprint = {2012.01323} } +@inproceedings{Dudek2020, + author = {J.~M.~Dudek and + V.~H.~N.~Phan and + M.~Y.~Vardi}, + title = {{DPMC:} {Weighted} Model Counting by Dynamic Programming on Project-Join + Trees}, + booktitle = {Proc.\ CP}, + series = {LNCS~12333}, + pages = {211--230}, + publisher = {Springer}, + year = {2020}, + doi = {10.1007/978-3-030-58475-7\_13} +} + +% TODO +@inproceedings{Dudek2021, + author = {J.~M.~Dudek and + V.~H.~N.~Phan and + M.~Y.~Vardi}, + title = {{ProCount:} {Weighted} Projected Model Counting with Graded Project-Join Trees}, + booktitle = {Proc.\ SAT}, + year = {2021} +} + %%% Integer linear programming %SIP tutorial @article{Schultz2003, diff --git a/Talks/oral_defense/related-work/counting.tex b/Talks/oral_defense/related-work/counting.tex index 7e96163..90a623f 100644 --- a/Talks/oral_defense/related-work/counting.tex +++ b/Talks/oral_defense/related-work/counting.tex @@ -1,30 +1,55 @@ \begin{frame} - \frametitle{Model Counting} - \begin{itemize} - \item Exact: find the precise count - \pause - \begin{itemize} - \item \cachet~\cite{Sang2004,Sang2005ModelCounting}: DPLL search plus subformula caching - \pause - \item \texttt{c2d}~\cite{Darwiche2001,Darwiche2002dDNNF}: CNF-to-d-DNNF compilation - \pause - \end{itemize} - \item Approximate: bounds with guarantee - \pause - \begin{itemize} - \item \approxmc~\cite{Chakraborty2013,Chakraborty2016}: $\Pr[(1+\epsilon)^{-1}\#\pf \leq A \leq (1+\epsilon)\#\pf] \geq 1-\delta$ - \pause - \end{itemize} - \item Variants: expressible by SSAT - \pause - \begin{itemize} - \item Weighted model counting~\cite{Sang2005BayesianInference,Chavira2008} - \pause - \item Projected model counting~\cite{Aziz2015} - \pause - \item Maximum model counting~\cite{Fremont2017} - \pause - \end{itemize} - \item Model Counting Competition~\cite{MC-COMP2020} - \end{itemize} + \frametitle{Model Counting} + \begin{itemize} + \item Exact: find the precise count + \pause + \begin{itemize} + \item \cachet~\cite{Sang2004,Sang2005ModelCounting}: DPLL search plus subformula caching + \pause + \item \texttt{c2d}~\cite{Darwiche2001,Darwiche2002dDNNF}: CNF-to-d-DNNF compilation + \pause + \item \dpmc~\cite{Dudek2020}: project-join tree and arithmetic decision diagrams + \pause + \end{itemize} + \item Approximate: bounds with guarantee + \pause + \begin{itemize} + \item \approxmc~\cite{Chakraborty2013,Chakraborty2016}: $\Pr[(1+\epsilon)^{-1}\#\pf \leq A \leq (1+\epsilon)\#\pf] \geq 1-\delta$ + \pause + \end{itemize} + \item Variants: expressible by SSAT + \pause + \begin{itemize} + \item Weighted model counting~\cite{Sang2005BayesianInference,Chavira2008} + \pause + \item Projected model counting~\cite{Aziz2015} + \pause + \item Maximum model counting~\cite{Fremont2017} + \pause + \item Weighted projected model counting + \pause + \begin{itemize} + \item \procount~\cite{Dudek2021}: ordering of projected and non-projected variables + \pause + \end{itemize} + \end{itemize} + \item Model Counting Competition~\cite{MC-COMP2020} + \end{itemize} +\end{frame} + +\begin{frame} + \frametitle{Express Model-Counting Variants with SSAT} + \begin{table}[t] + \centering + \begin{tabular}{c|c} + Variant & SSAT encoding \\ + \hline + Unweighted & $\random{0.5}x_1,\ldots,\random{0.5}x_n.\pf$ \\ + Weighted & $\random{p_1}x_1,\ldots,\random{p_n}x_n.\pf$ \\ + Projected & $\random{0.5}x_1,\ldots,\random{0.5}x_n,\exists y_1,\ldots,\exists y_m.\pf$ \\ + Maximum & $\exists x_1,\ldots,\exists x_n,\random{0.5}y_1,\ldots,\random{0.5}y_m.\pf$ \\ + Weighted projected & $\random{p_1}x_1,\ldots,\random{p_n}x_n,\exists y_1,\ldots,\exists y_m.\pf$ \\ + Maximum weighted & $\exists x_1,\ldots,\exists x_n,\random{p_1}y_1,\ldots,\random{p_m}y_m.\pf$ \\ + \end{tabular} + \end{table} \end{frame} \ No newline at end of file diff --git a/paper/preamble.tex b/paper/preamble.tex index a53c3be..b7c8d3b 100644 --- a/paper/preamble.tex +++ b/paper/preamble.tex @@ -106,6 +106,8 @@ \definetool{\minisat}{MiniSat} \definetool{\cachet}{Cachet} \definetool{\approxmc}{ApproxMC} +\definetool{\dpmc}{DPMC} +\definetool{\procount}{ProCount} \definetool{\cnfgen}{CNFgen} \definetool{\benchexec}{BenchExec} \definetool{\abc}{ABC} diff --git a/paper/prob.bib b/paper/prob.bib index 479b9b7..6d4a023 100644 --- a/paper/prob.bib +++ b/paper/prob.bib @@ -190,6 +190,14 @@ @incollection{SATHandbook-QBF doi = {10.3233/978-1-58603-929-5-735} } +%frohlich2012dpll +@inproceedings{Frohlich2012, + title = {A {DPLL} algorithm for solving {DQBF}}, + author = {A.~Fr{\"o}hlich and G.~Kov{\'a}sznai and A.~Biere}, + booktitle = {Proc.\ POS}, + year = {2012} +} + %balabanov2014henkin @article{Balabanov2014, author = {V.~Balabanov and @@ -204,6 +212,16 @@ @article{Balabanov2014 doi = {10.1016/j.tcs.2013.12.020} } +%GitinaWRSSB15 +@inproceedings{Gitina2015, + author = {K.~Gitina and R.~Wimmer and S.~Reimer and M.~Sauer and C.~Scholl and B.~Becker}, + booktitle = {Proc.\ DATE}, + title = {Solving {DQBF} through quantifier elimination}, + year = {2015}, + pages = {1617-1622}, + doi = {10.7873/DATE.2015.0098} +} + %JanotaM15 @inproceedings{Janota2015, author = {M.~Janota and J.~P.~Marques-Silva}, @@ -500,6 +518,30 @@ @article{MC-COMP2020 eprint = {2012.01323} } +@inproceedings{Dudek2020, + author = {J.~M.~Dudek and + V.~H.~N.~Phan and + M.~Y.~Vardi}, + title = {{DPMC:} {Weighted} Model Counting by Dynamic Programming on Project-Join + Trees}, + booktitle = {Proc.\ CP}, + series = {LNCS~12333}, + pages = {211--230}, + publisher = {Springer}, + year = {2020}, + doi = {10.1007/978-3-030-58475-7\_13} +} + +% TODO +@inproceedings{Dudek2021, + author = {J.~M.~Dudek and + V.~H.~N.~Phan and + M.~Y.~Vardi}, + title = {{ProCount:} {Weighted} Projected Model Counting with Graded Project-Join Trees}, + booktitle = {Proc.\ SAT}, + year = {2021} +} + %%% Integer linear programming %SIP tutorial @article{Schultz2003, diff --git a/paper/related-work/model-counting.tex b/paper/related-work/model-counting.tex index 4011588..fa9b5e2 100644 --- a/paper/related-work/model-counting.tex +++ b/paper/related-work/model-counting.tex @@ -4,7 +4,7 @@ \section{Model counting} Model-counting~\cite{SATHandbook-ModelCounting} algorithms can be classified into two categories: exact counting and approximate counting. The former adopts DPLL-based search with additional techniques, -such as component analysis and caching, to improve the counting efficiency\cite{Sang2004,Sang2005ModelCounting}. +such as component analysis and caching, to improve the counting efficiency~\cite{Sang2004,Sang2005ModelCounting}. The latter takes a different strategy, aiming at providing lower and/or upper bounds with guarantee on confidence level. Ideas from statistics~\cite{Chakraborty2016} have been adopted to increase the capacity limit of model counting. @@ -21,7 +21,7 @@ \section{Model counting} The above variants of model counting can be expressed via SSAT, because the randomized quantifiers of SSAT essentially aggregate the results from different branches with weights. \Cref{tbl:related-work-model-counting} shows the variants of model-counting problems and their respective SSAT encodings. -Note that projected weighted model counting and maximum weighted model counting are equivalent to +Note that weighted projected model counting and maximum weighted model counting are equivalent to random-exist quantified SSAT and exist-random quantified SSAT, respectively. \begin{table}[t] @@ -35,9 +35,16 @@ \section{Model counting} Weighted & $\random{p_1}x_1,\ldots,\random{p_n}x_n.\pf(x_1,\ldots,x_n)$ \\ Projected & $\random{0.5}x_1,\ldots,\random{0.5}x_n,\exists y_1,\ldots,\exists y_m.\pf(x_1,\ldots,x_n,y_1,\ldots,y_m)$ \\ Maximum & $\exists x_1,\ldots,\exists x_n,\random{0.5}y_1,\ldots,\random{0.5}y_m.\pf(x_1,\ldots,x_n,y_1,\ldots,y_m)$ \\ - Projected weighted & $\random{p_1}x_1,\ldots,\random{p_n}x_n,\exists y_1,\ldots,\exists y_m.\pf(x_1,\ldots,x_n,y_1,\ldots,y_m)$ \\ + Weighted projected & $\random{p_1}x_1,\ldots,\random{p_n}x_n,\exists y_1,\ldots,\exists y_m.\pf(x_1,\ldots,x_n,y_1,\ldots,y_m)$ \\ Maximum weighted & $\exists x_1,\ldots,\exists x_n,\random{p_1}y_1,\ldots,\random{p_m}y_m.\pf(x_1,\ldots,x_n,y_1,\ldots,y_m)$ \\ \end{tabular} \end{table} -The latest developments of model counting can be found in the report~\cite{MC-COMP2020} of the 2020 Model Counting Competition. \ No newline at end of file +Model counting is under active research. +Recent advancements include \dpmc~\cite{Dudek2020}, +a dynamic-programming framework for exact weighted model counting based on \textit{project-join} trees. +\dpmc applies tree decomposition to the constraint graph of a CNF formula to obtain a project-join tree +and aggregates the weight of the formula with \textit{arithmetic decision diagrams} using dynamic programming. +\dpmc is further extended to a weighted projected model counter \procount~\cite{Dudek2021} +by requiring the projected variables to be placed on top of the non-projected variables in a project-join tree. +Other latest developments of model counting can be found in the report~\cite{MC-COMP2020} of the 2020 Model Counting Competition. \ No newline at end of file