Model counting of monotone conjunctive normal form formulas with Spectra

Vaisman, Radislav, Strichman, Ofer and Gertsbakh, Ilya (2015) Model counting of monotone conjunctive normal form formulas with Spectra. INFORMS Journal On Computing, 27 2: 406-415. doi:10.1287/ijoc.2014.0633


Author Vaisman, Radislav
Strichman, Ofer
Gertsbakh, Ilya
Title Model counting of monotone conjunctive normal form formulas with Spectra
Journal name INFORMS Journal On Computing   Check publisher's open access policy
ISSN 1091-9856
1526-5528
Publication date 2015-03
Year available 2015
Sub-type Article (original research)
DOI 10.1287/ijoc.2014.0633
Open Access Status Not Open Access
Volume 27
Issue 2
Start page 406
End page 415
Total pages 10
Place of publication Catonsville, MD United States
Publisher Institute for Operations Research and the Management Sciences (INFORMS)
Collection year 2016
Language eng
Formatted abstract
Model counting is the #P problem of counting the number of satisfying solutions of a given propositional formula. Here we focus on a restricted variant of this problem, where the input formula is monotone (i.e., there are no negations). A monotone conjunctive normal form (CNF) formula is sufficient for modeling various graph problems, e.g., the vertex covers of a graph. Even for this restricted case, there is no known efficient approximation scheme. We show that the classical Spectra technique that is widely used in network reliability can be adapted for counting monotone CNF formulas. We prove that the proposed algorithm is logarithmically efficient for random monotone 2-CNF instances. Although we do not prove the efficiency of Spectra for k-CNF where k > 2, our experiments show that it is effective in practice for such formulas.
Keyword Simulation
Counting
Monte Carlo
Monotone CNF
Random graphs
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

Document type: Journal Article
Sub-type: Article (original research)
Collections: School of Mathematics and Physics
Official 2016 Collection
 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Sun, 21 Jun 2015, 01:19:31 EST by System User on behalf of School of Mathematics & Physics