A Parallel Extension Rule-Based Algorithm for #SAT Problem Using Model-Counting Tree

Abstract

The #SAT problem, which is also called model counting, is one of the most important problems in artificial intelligence and is challenging to the researchers. The model counting based on extension rule (CER) algorithm is an exact algorithm for model counting. The weak point of the algorithm is the high computational complexity which adds to the running time. We introduce parallel CER, an algorithm that parallelizes the model counting algorithm CER. The CER algorithm is based on the extension rule. We propose a notion of MC-Tree for describing the computing procedure. We implemented the algorithm on a quad-core machine using OpenMP to measure the performance. Our experimental results on simulated data show that: 1) with the increase of the number of processors, the running time of our parallel algorithm reduces in inverse proportion, and furthermore, the algorithm is more efficient in case of using each number of processors when the complementary factor is higher and 2) the scalability of the algorithm is linear for all instances, and the efficiency is evident.