A New Hypergraph Measure for #SAT

The #SAT problem

• #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).

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

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

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.

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

$\alpha$-leaves

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

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.

Enters the rest of greek alphabet

How can we use it algorithmically?

SAT and $\beta$-acyclicity

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

#SAT and $\beta$-acyclicity

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

Non acyclic hypergraphs

• $\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) = 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?

Problem with $\beta$-Hypertree Width

Expanding the definition:

$$\beta htw(H) = \max_{H' \subseteq H} \min_T 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.

#SAT and $\beta how(H)$

• 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 $F$:
  • gives tractable weighted model counting
  • tractable direct access
  • …

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?

Ad

References

[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.