A bottom-up algorithm for solving ♯2SAT. (5th May 2020)

• Record Type: Journal Article
• Authors: De Ita, Guillermo; Marcial-Romero, J Raymundo; HernÁndez-ServÍn, J A
• Is Part Of: Logic journal of the IGPL. Volume 28:Number 6(2020)
• Page Start: 1130
• Page End: 1140
• Publication Date: 2020-05-05
• Subjects: ♯Sat -- counting models -- enumerative algorithm -- graph decomposition; Logic, Symbolic and mathematical -- Periodicals; 511.3
• DOI: 10.1093/jigpal/jzaa009
• Languages: English
• ISSNs: 1367-0751

Abstract

Abstract: Counting models for a two conjunctive formula (2-CF) $F$, a problem known as $\sharp $ 2Sat, is a classic $\sharp $ P complete problem. Given a 2-CF $F$ as input, its constraint graph $G$ is built. If $G$ is acyclic, then $\sharp $ 2Sat ($F$ ) can be computed efficiently. In this paper, we address the case when $G$ has cycles. When $G$ is cyclic, we propose a decomposition on the constraint graph $G$ that allows the computation of $\sharp $ 2Sat ($F$ ) in incremental way. Let $T$ be a cactus graph of $G$ containing a maximal number of independent cycles, and let $\overline{T}=(E(G)-E(T))$ be a subset of frond edges from $G$ . The clauses in $\overline{T}$ are ordered in connected components $\{K_1, \ldots, K_r\}$ . Each $(G \cup K_i), i=1, \ldots, r$ is a knot (a set of intersected cycles) of the graph. The arrangement of the clauses of $\overline{T}$ allows the decomposition of $G$ in knots and provides a way of computing $\sharp $ 2Sat (F) in an incremental way. Our procedure has a bottom-up orientation for the computation of $\sharp $ 2Sat ($F$ ). It begins with $F_0 = T$ . In each iteration of the procedure, a new clause $C_i \in \overline{T}$ is considered in order to form $F_i = (F_{i-1} \wedge C_i)$ and then to compute $\sharp $ 2Sat $(F_i)$ based on the computation of $\sharp $ 2Sat $(F_{i-1})$ .