Skip to content

Commit

Permalink
Add discussion of DPMC and ProCount
Browse files Browse the repository at this point in the history 
- In slides: move the SSAT-encoding table back to related work
  • Loading branch information
nianze committed May 24, 2021
1 parent 42308cc commit 57f6812
Show file tree
Hide file tree
Showing 7 changed files with 355 additions and 270 deletions.
319 changes: 151 additions & 168 deletions Talks/oral_defense/background/ssat.tex
View file

Large diffs are not rendered by default.

142 changes: 72 additions & 70 deletions Talks/oral_defense/preamble.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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}
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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}
}
24 changes: 24 additions & 0 deletions Talks/oral_defense/prob.bib
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
81 changes: 53 additions & 28 deletions Talks/oral_defense/related-work/counting.tex
View file
Original file line number Diff line number Diff line change
@@ -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}
2 changes: 2 additions & 0 deletions paper/preamble.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
42 changes: 42 additions & 0 deletions paper/prob.bib
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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},
Expand Down Expand Up @@ -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,
Expand Down
Loading

0 comments on commit 57f6812

Please sign in to comment.