用于命题模型计数的学习分支启发式算法
Learning Branching Heuristics for Propositional Model Counting
摘要：
命题模型计数（Propositional Model Counting），或#SAT，是计算布尔公式的满意赋值的数量的问题。来自不同应用领域的许多问题，包括许多离散概率推理问题，可以转化为模型计数问题，由#SAT求解器来解决。然而，精确的#SAT求解器通常不能扩展到工业规模的实例。在本文中，我们提出了Neuro#，一种用于学习分支算法的方法，以提高给定问题族实例上的精确SAT求解器的性能。我们的实验表明，我们的方法减少了类似的分布式举行了实例的步骤数，并推广到更大的实例，从同一个问题的家庭。它是能够实现这些结果对一些不同的问题家庭具有非常不同的结构。除了步数改进之外，Neuro#还可以在某些问题族中的较大实例上实现比vanilla求解器高出几个数量级的挂钟加速，尽管查询模型的运行时开销很大。
英文摘要：
Propositional model counting, or #SAT, is the problem of computing the number of satisfying assignments of a Boolean formula. Many problems from different application areas, including many discrete probabilistic inference problems, can be translated into model counting problems to be solved by #SAT solvers. Exact #SAT solvers, however, are often not scalable to industrial size instances. In this paper, we present Neuro#, an approach for learning branching heuristics to improve the performance of exact #SAT solvers on instances from a given family of problems. We experimentally show that our method reduces the step count on similarly distributed held-out instances and generalizes to much larger instances from the same problem family. It is able to achieve these results on a number of different problem families having very different structures. In addition to step count improvements, Neuro# can also achieve orders of magnitude wall-clock speedups over the vanilla solver on larger instances in some problem families, despite the runtime overhead of querying the model.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
