A New Hypergraph Measure for #SAT

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

Structural Tractability of #SAT

The #SAT problem

Given CNF $F$ , return $\#F$ , the number of satisfying assignments.

#P-hard to solve.
Even for very restricted classes: #Mon-2-SAT, #Horn-SAT etc.
NP-hard to (even badly) approximate (see ApproxMC for practical work in this direction).

Same story as SAT: hard problem but useful in practice.

Reasoning on propositionnal knowledge basis.
Solve other counting problems using parcimonious reductions.

When can we solve #SAT more efficiently than bruteforce?

Exploiting clauses-variables interactions

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.

Structure of CNF formulas

$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)$

Structural Tractability

If (primal / incidence) graph of $F$ of size $n$ has treewidth $k$ then $\#F$ can be computed in time $2^{O(k)}n$ . [1]

Tree decomposition of F — Tree decomposition of $F$

Exhaustive DPLL:

$\#F[X \gets \tau] = \#G[X \gets \tau]·\#H[X \gets \tau]$

since $Y \cap Z \subseteq X$

Branch on $2^k$ values $x_1,\dots,x_k$
Recursive calls on $H$ and $G$
Cache subformulas already solved

[1] Samer, Marko, and Stefan Szeider. “Algorithms for propositional model counting.” Journal of Discrete Algorithms 8.1 (2010): 50-64.

Hypergraph Acyclicities

$\alpha$ -acyclicity

Generalize acyclicity to hypergraphs:

Used in databases/CSP (tractable conjunctive queries / CSPs).
Usually defined in terms of tree decompositions of hypergraphs… Not today!

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.

$\alpha$ -leaves

$H=(V,E)$ a hypergraph.
$N(v)$ : neighborhood of $v$

A vertex $v$ in a hypergraph is an $\alpha$ -leave if $N(v) \subseteq e$ for some edge $e$ of $H$

$x_6, \dots, x_1$ is an $\alpha$ -elimination order.
Subgraphs may no be $\alpha$ -acyclic (look, a triangle!)

SAT is hard on $\alpha$ -acyclic hypergraphs

Not a good variable-clause restriction for tractability:

$F$ a CNF formula
$F' = F \wedge (x_1 \vee \dots \vee x_n \vee y)$ is $\alpha$ -acyclic
$F'$ SAT iff $F$ is SAT.

Hard subformulas make the formula hard (this does not happen with conjunctive queries).

Enters the rest of greek alphabet

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 and $\beta$ -acyclicity

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 and $\beta$ -acyclicity

#SAT is easy on $\beta$ -acyclic instances, with classical algorithm [3]:

Exhaustive DPLL following a reversed $\beta$ -elimination order terminates in polynomial time!

Tractable case not captured by bounded treewidth or other existing graph measures
Only works for a very restricted set of instances.

[3] Florent Capelli, Understanding the complexity of #SAT using knowledge compilation, LICS, 2017.

Hyperorder widths

Non acyclic hypergraphs

How do we measure how far we are from acyclicity?

$\alpha$ -acyclicity naturally generalizes to hypertree width: $htw(H) \in \mathbb{N}$ .
Usually defined via tree decomposition.
We give an order based definition.

Width of an elimination order

$H=(V,E)$ , $\pi = (v_1,\dots,v_n)$ order on $V$ .
Iteratively add edge $N(v_i)$ and remove $v_i$
Hyperorder width $how(H,\pi)$ of $\pi = (v_1,\dots,v_n)$ : maximum number of edges from $H$ to cover the neighborhood of $v_i$ in $H_i$ .

$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$

Hyperorder width and Hypertree width

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).$

$how(H) = 1$ iff $H$ is $\alpha$ -acyclic
For how(·), the order is the decomposition.

$\beta$ -Hypertree Width

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…

Problem with $\beta$ -Hypertree Width

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$ …

Bringing Order

For $H$ $\beta$ -acyclic:

$H_1,H_2 \subseteq H$ may have very different tree decompositions.
Tree decomposition is not the right tool here.

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 and $\beta how(H)$

#SAT can be solved in time $n^{O(k)}$ for a formula $F$ of size $n$ and $\beta how(F)=k$ .

Algorithm: exhaustive DPLL following a reversed optimal elimination order.
Generalizes tractability of $\beta$ -acyclic formulas and bounded nest set width [4]
Algorithm implicitly constructs decision-DNNF for FF:
- gives tractable weighted model counting
- tractable direct access
- …

[4] Lanzinger, M.. Tractability beyond β-acyclicity for conjunctive queries with negation and SAT. Theoretical Computer Science, 2023.

Wrapping up

Structural complexity of #SAT:

FPT XP open #P-hard

Where does $\beta$ -how sit in this diagram?
Where is the frontier for SAT?

Postdoc position open at CRIL, Lens!

References