Two approximate algorithms for model counting

被引：3

作者：

Wang, Jinyan ^{[1
,2
]}

Yin, Minghao ^{[3
]}

Wu, Jingli ^{[1
,2
]}

机构：

[1] Guangxi Normal Univ, Guangxi Key Lab Multisource Informat Min & Secur, Guilin, Peoples R China

[2] Guangxi Normal Univ, Coll Comp Sci & Informat Technol, Guilin, Peoples R China

[3] Northeast Normal Univ, Sch Comp Sci & Informat Technol, Changchun, Peoples R China

来源：

THEORETICAL COMPUTER SCIENCE | 2017年 / 657卷

基金：

中国国家自然科学基金;

关键词：

Propositional satisfiability; Model counting; Resolution principle; Extension rule; INCLUSION-EXCLUSION; NUMBER-SAT;

D O I：

10.1016/j.tcs.2016.04.047

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Model counting is the problem of computing the number of models or satisfying assignments for a given propositional formula, and is #P-complete. Owing to its inherent complexity, approximate model counting is an alternative in practice. Model counting using the extension rule is an exact method, and is considered as an alternative to resolution-based methods for model counting. Based on the exact method, we propose two approximate model counting algorithms, and prove the time complexity of the algorithms. Experimental results show that they have good performance in the accuracy and efficiency. (C) 2016 Elsevier B.V. All rights reserved.

引用

页码：28 / 37

页数：10

共 30 条

[1] Algorithms and complexity results for #SAT and Bayesian inference [J].

Bacchus, F ;

Dalmao, S ;

Pitassi, T .

44TH ANNUAL IEEE SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 2003, :340-351

[2] Solving #SAT and Bayesian Inference with Backtracking Search [J].

Bacchus, Fahiem ;

Dalmao, Shannon ;

Pitassi, Toniann .

JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 2009, 34 :391-442

[3]

Bayardo RJ, 2000, SEVENTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-2001) / TWELFTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE (IAAI-2000), P157

[4]

Beame P., 2004, SAT 2004 7 INT C THE

[5]

Bennett H, 2011, LECT NOTES COMPUT SC, V6695, P362

[6] The good old Davis-Putnam procedure helps counting models [J].

Birnbaum, E ;

Lozinskii, EL .

JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 1999, 10 :457-477

[7] On the utility of landmarks in SAT based planning [J].

Cai, Dunbo ;

Yin, Minghao .

KNOWLEDGE-BASED SYSTEMS, 2012, 36 :146-154

[8] A MACHINE PROGRAM FOR THEOREM-PROVING [J].

DAVIS, M ;

LOGEMANN, G ;

LOVELAND, D .

COMMUNICATIONS OF THE ACM, 1962, 5 (07) :394-397

[9] Probabilistic planning via heuristic forward search and weighted model counting [J].

Domshlak, Carmel ;

Hoffmann, Joerg .

JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 2007, 30 :565-620

[10]

Gogate V., 2007, Proceedings of the 22nd national Conference on Artificial Intelligence, P198

← 1 2 3 →