基于格局检测的模型计数方法

• 作者: 刘磊 吕帅 牛当当 王强 贺甫霖
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模型计数 局部搜索 格局检测
• 年，卷（期）: 2020,（2）
• 所属期刊栏目: 模式识别与人工智能
• 页码范围: 395-405
• 页数: 11页
• 分类号: TP18
• 字数: 8906字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005642

摘要

模型计数是指求出给定命题公式的模型数,是SAT问题的泛化.模型计数在人工智能领域取得了广泛应用,彳艮多现实问题都可以规约为模型计数进行求解.目前,常用的模型计数求解器主要有Cachet与sharpSAT,它们均采用完备方法且具有高效的求解能力,但其求解效率对模型数不敏感.有理由猜测:当给定问题的模型较少时,不完备算法可能发挥其效率优势而更适合模型计数.局部搜索是求解SAT问题的高效不完备方法,Cai等人提出了格局检测策略,并将其应用到局部搜索方法中,提出了SWcc算法,具有很高的求解效率.对SWcc算法进行扩充,分别得到了迭代法与优化后的增量法两种效率较高的不完备模型计数方法,给出了两种方法的思路和具体实现.最后给出了大量测试样例的实验结果,以验证当给定合取范式的模型较少时,该迭代法与优化后的增量法的求解效率有所提升.