BIRD: Engineering an Efficient CNF-XOR SAT Solver and Its Applications to Approximate Model Counting
BIRD: Engineering an Efficient CNF-XOR SAT Solver and Its Applications to Approximate Model Counting
复制标题
BIRD：设计高效的 CNF-XOR SAT 求解器及其在近似模型计数中的应用
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Kuldeep S. Meel
中科院分区：
文献类型：
--
作者：
M. Soos;Kuldeep S. Meel
给定一个布尔公式φ，模型计数问题（也称为#SAT）就是计算φ的解的个数。模型计数是人工智能中的一个基本问题，在概率推理、不确定决策、量化信息流等方面有着广泛的应用。由于SAT求解器的成功，在过去十年中，人们对基于哈希的近似模型计数技术的设计产生了浓厚的兴趣。我们分析了最先进的近似模型计数器ApproxMC2，并观察到超过99.99%的时间被底层SAT求解器CryptoMiniSat所消耗。这一观察结果激发了我们的疑问：我们能否设计一个有效的底层CNF-XOR SAT求解器，利用基于哈希算法的结构，这是否会导致一个有效的近似模型计数器？
Given a Boolean formula φ, the problem of model counting, also referred to as #SAT is to compute the number of solutions of φ. Model counting is a fundamental problem in artificial intelligence with a wide range of applications including probabilistic reasoning, decision making under uncertainty, quantified information flow, and the like. Motivated by the success of SAT solvers, there has been surge of interest in the design of hashing-based techniques for approximate model counting for the past decade. We profiled the state of the art approximate model counter ApproxMC2 and observed that over 99.99% of time is consumed by the underlying SAT solver, CryptoMiniSat. This observation motivated us to ask: Can we design an efficient underlying CNF-XOR SAT solver that can take advantage of the structure of hashing-based algorithms and would this lead to an efficient approximate model counter?
The primary contribution of this paper is an affirmative answer to the above question. We present a novel architecture, called BIRD, to handle CNF-XOR formulas arising from hashingbased techniques. The resulting hashing-based approximate model counter, called ApproxMC3, employs the BIRD framework in its underlying SAT solver, CryptoMiniSat. To the best of our knowledge, we conducted the most comprehensive study of evaluation performance of counting algorithms involving 1896 benchmarks with computational effort totaling 86400 computational hours. Our experimental evaluation demonstrates significant runtime performance improvement for ApproxMC3 over ApproxMC2. In particular, we solve 648 benchmarks more than ApproxMC2, the state of the art approximate model counter and for all the formulas where both ApproxMC2 and ApproxMC3 did not timeout and took more than 1 seconds, the mean speedup is 284.40 – more than two orders of magnitude.