Effective Preprocessing in ＃SAT

摘要：

Preprocessing ＃SAT instances can reduce their size considerably and decrease the solving time. In this paper we investigate the use of the hyper-binary resolution and equality reduction to preprocess the ＃SAT instances. And a preprocessing algorithm PreprocessMC is presented, which combines the unit propagation, the hyper-binary resolution, and the equality reduction together. The experiment shows that these excellent technologies not only reduce the size of the ＃SAT formula, but also improve the ability of the model counters to solve ＃SAT problems.

关键词： preprocess model counting USAT equality reduction hyper-binary resolution

作者: Qin Guo Juan Sang Yongmei He

作者单位: Information College Jilin University of Finance and Economics Changchun, China

会议类型: 国际会议

会议名称: 2010 International Conference on Software and Computing Technology(2010年软件与计算机技术国际会议 ICSCT 2010)

会议地点: 昆明

会议语种:英文

页码: 693-696

在线出版日期: 2010-10-17（万方平台首次上网日期，不代表论文的发表时间）