Florent Capelli
CRIL, Université d’Artois
Dagstuhl Seminar 24421
October 17, 2024
Loosely based on Direct Access for Conjunctive Queries with Negation with Oliver Irwin, ICDT 24
Given CNF $F$, return $\#F$, the number of satisfying assignments.
Same story as SAT: hard problem but useful in practice.
When can we solve #SAT more efficiently than bruteforce?
Tractability of #SAT arises from restricted clauses-variables interactions.
If $X \cap Y = \emptyset$ and $F(X,z_1,z_2,Y) \equiv G(X,z_1,z_2) \wedge H(Y,z_1,z_2)$:
$\#F = \sum_{a,b \in \{0,1\}^2}\#G[z_1=a,z_2=b] · \#H[z_1=a,z_2=b]$
If we can recursively decompose the formula this way, we can count efficiently.
$F =$ $(x_1 \vee \neg x_2 \vee x_3)$ $\wedge$ $(x_3 \vee x_4 \vee x_5)$ $\wedge$ $(x_1 \vee \neg x_5 \vee \neg x_6)$ $\wedge$ $(x_1 \vee x_3 \vee x_5 \vee x_7)$
If (primal / incidence) graph of $F$ of size $n$ has treewidth $k$ then $\#F$ can be computed in time $2^{O(k)}n$. [1]
Exhaustive DPLL:
$\#F[X \gets \tau] = \#G[X \gets \tau]·\#H[X \gets \tau]$
since $Y \cap Z \subseteq X$
[1] Samer, Marko, and Stefan Szeider. “Algorithms for propositional model counting.” Journal of Discrete Algorithms 8.1 (2010): 50-64.
Generalize acyclicity to hypergraphs:
A hypergraph is $\alpha$-acyclic if and only if we can obtained the empty graph by iteratively removing $\alpha$- leaves.
We call such vertex ordering: $\alpha$-elimination order.
A vertex $v$ in a hypergraph is an $\alpha$-leave if $N(v) \subseteq e$ for some edge $e$ of $H$
Not a good variable-clause restriction for tractability:
Hard subformulas make the formula hard (this does not happen with conjunctive queries).
A hypergraph $H$ is $\beta$-acyclic if and only if every $H' \subseteq H$ is $\alpha$-acyclic.
How can we use it algorithmically?
A hypergraph $H$ is $\beta$-acyclic if and only if there exists an order on $V$ that is an $\alpha$-elimination order for every $H' \subseteq H$.
We call such ordering a $\beta$-elimination order.
Side note: this is not how $\beta$-elimination order is usually defined.
SAT is easy on $\beta$-acyclic instances, with a classical algorithm [2]:
Davis-Putnam resolution following a $\beta$-elimination order terminates in polynomial time!
[2] Ordyniak, Sebastian, Daniël Paulusma, and Stefan Szeider. “Satisfiability of acyclic and almost acyclic CNF formulas.” Theoretical Computer Science, 2013.
#SAT is easy on $\beta$-acyclic instances, with classical algorithm [3]:
Exhaustive DPLL following a reversed $\beta$-elimination order terminates in polynomial time!
[3] Florent Capelli, Understanding the complexity of #SAT using knowledge compilation, LICS, 2017.
How do we measure how far we are from acyclicity?
$N(x_1)$ covered by $2$ edges of $H$
$N(x_2)$ covered by $3$ edges of $H$
$N(x_3)$ covered by $3$ edges of $H$
$N(x_4)$ covered by $3$ edges of $H$
$N(x_5)$ covered by $2$ edges of $H$
$how(H,(x_1,\dots,x_6)) = 3$
$how(H,(x_6,\dots,x_1)) = 1$
Hypertree width of $H$ : $htw(H) = \min_T htw(H,T)$ where $T$ is a tree decomposition
Hyperorder width of $H$ : $how(H) = \min_\pi how(H,\pi)$ where $\pi$ is an elimination order.
$how(H) = htw(H).$
Sometimes, there is $H' \subseteq H$ st $htw(H')>htw(H)$.
Same trick as before:
$\beta htw(H) = \max_{H' \subseteq H} htw(H')$
How can we use it algorithmically?
We do not know…
Expanding the definition:
$\beta htw(H) = \max_{H' \subseteq H} \min_T htw(H',T)$
Problem: a different decomposition can be used for different subhypergraphs…
Swap quantifiers!
$\beta' htw(H) = \min_T \max_{H' \subseteq H} htw(H',T)$
Problem: $\beta'htw(S_n) = n$…
For $H$ $\beta$-acyclic:
A hypergraph $H$ is $\beta$-acyclic if and only if there exists an order on $V$ that is an $\alpha$-elimination order for every $H' \subseteq H$.
$\begin{align} \beta htw(H) & = \max_{H' \subseteq H} \min_T htw(H',T)\\ & = \max_{H' \subseteq H} \min_\pi how(H',\pi) \end{align}$
Swap quantifier in the second equality:
$\beta how(H) = \min_\pi \max_{H' \subseteq H} how(H',\pi)$
#SAT can be solved in time $n^{O(k)}$ for a formula $F$ of size $n$ and $\beta how(F)=k$.
[4] Lanzinger, M.. Tractability beyond β-acyclicity for conjunctive queries with negation and SAT. Theoretical Computer Science, 2023.
Structural complexity of #SAT:
FPT XP open #P-hard
Postdoc position open at CRIL, Lens!
[1] Samer, Marko, and Stefan Szeider. “Algorithms for propositional model counting.” Journal of Discrete Algorithms 8.1 (2010): 50-64.
[2] Ordyniak, Sebastian, Daniël Paulusma, and Stefan Szeider. “Satisfiability of acyclic and almost acyclic CNF formulas.” Theoretical Computer Science, 2013.
[3] Florent Capelli, “Understanding the complexity of #SAT using knowledge compilation”, LICS, 2017.
[4] Lanzinger Matthias. “Tractability beyond β-acyclicity for conjunctive queries with negation and SAT”. Theoretical Computer Science, 2023.