基于异或约束约简的近似#SAT求解算法研究

发布时间：2021-12-19 05:12

　　模型计数（model counting,#SAT）问题旨在计算给定的公式集合中所有模型的个数,绝大部分计算复杂度为#P的问题均可以在多项式时间内归约为模型计数问题。在人工智能领域,许多计算复杂度高于NP的问题均可转化为模型计数问题进行求解。因此,研究模型计数问题求解技术对可以与模型计数问题相互转化的领域有着重要意义。然而,现有的精确模型计数求解算法对大规模问题求解能力较为低下,而且对于目前的许多问题来说,求出精确的模型数是不必要的,因此近似模型计数求解技术被提出。其中最有潜力的方法之一就是基于异或约束进行近似求解。该求解方法的本质是基于采样的思想,利用平均长度为变量数一半的异或约束对解空间进行削减,待解空间削减到足够小后,利用精确求解技术对其求解从而得到精确模型数,最后通过该解空间与整体解空间的比例关系估算整体解空间的近似模型数。通过对现有的近似求解算法的深入研究,本文提出了一种新的结合有界求解策略与可控随机策略的近似#SAT求解算法。由于异或约束在解空间较小时分割不够精确,有界求解策略通过限制应用异或约束的解空间规模有效地提升了求解算法的精确度。可控随机策略利用骨架变量以及变量之间的... 

【文章来源】：吉林大学吉林省 211工程院校 985工程院校 教育部直属院校

【文章页数】：64 页

【学位级别】：硕士

【部分图文】：

#KiF与#KiF的差异对比

第4章实验结果与分析23步骤1.调用三个算法各自生成异或约束的部分生成异或约束；步骤2.添加到合取范式F中；步骤3.调用SAT求解器对F进行求解；步骤4.重复步骤1-3，直到步骤3出现合取范式F不可满足，重置合取范式F为原始状态，记录当前消耗的时间t(s)，以及添加的异或约束的总数XOR_NUM，则XOR_NUM/t为单位时间内添加的异或约束的数量。以上三个求解器均采用Cryptominisat[37]作为后端的SAT求解器。此外，为消除AMCX_BC中预处理对实验结果的影响，实验也为ApproxMC2和STAC_CNF分别添加了与AMCX_BC相同的预处理策略。在实验中，每个测试样例将重复100次上述过程，所获得的结果为单位时间内添加的异或约束的数量。需要说明的是，预处理的时间消耗没有算在整体时间内。具体实验结果如图4-1所示。图4-1.单位时间内添加的异或约束数量比较图4-1的横坐标代表测试样例，纵坐标代表代为单位时间内添加的异或约束的数量。为便于比较，纵坐标采用对数刻度，120个测试样例按照ApproxMC2withpreprocessing曲线递增排序。从总体上来看，预处理对于单位时间内能够添加的异或约束数量的提升并不明显，主要起作用的应为可控随机策略。针对编号

AMCX_BC,ApproxMC2与STAC_CNF的求解时间比较


本文编号：3543826