A Study of Symmetry Breaking Predicates and Model Counting
A Study of Symmetry Breaking Predicates and Model Counting
复制标题
DOI：
10.1007/978-3-030-45190-5_7
复制
发表时间：
2020-03-13
期刊：
影响因子：
--
通讯作者：
Khurshid S
中科院分区：
文献类型：
--
作者：
Wang W;Usman M;Almaawi A;Wang K;Meel KS;Khurshid S
命题模型计数是一个经典的问题，最近见证了许多技术进步和新的应用。虽然基本模型计数问题需要计算给定公式的所有解的数量，但在一些重要的应用场景中，所需的计数不是所有解的数量，而是直到同构的所有唯一解的数量。在这种情况下，用户自己必须尝试使用模型计数器返回的完整计数来计算直到同构的计数，或者确保模型计数器的输入公式充分捕获对称破缺谓词，以便它可以直接报告她想要的计数。我们研究了CNF级和域级对称破缺谓词的使用，特别是领先的近似模型计数器ApproxMC和最近推出的精确模型计数器ProjMC。作为基准，我们使用了一系列的问题，包括结构复杂的软件系统和约束满足问题的规格。结果表明，虽然有时使用模型计数器计算的全计数来计算模型计数直到同构是可行的，但是这样做的可扩展性较差。对称破缺谓词的添加实质上有助于模型计数器。特定于域的谓词特别有用，并且在许多情况下可以提供完全的对称性破缺，以实现高效的模型同构计数。我们希望我们的研究能够激发新的研究，设计直接考虑对称性的模型计数器，以促进模型计数的进一步应用。
Propositional model counting is a classic problem that has recently witnessed many technical advances and novel applications. While the basic model counting problem requires computing the number of all solutions to the given formula, in some important application scenarios, the desired count is not of all solutions, but instead, of all unique solutions up to isomorphism. In such a scenario, the user herself must try to either use the full count that the model counter returns to compute the count up to isomorphism, or ensure that the input formula to the model counter adequately captures the symmetry breaking predicates so it can directly report the count she desires. We study the use of CNF-level and domain-level symmetry breaking predicates in the context of the state-of-the-art in model counting, specifically the leading approximate model counter ApproxMC and the recently introduced exact model counter ProjMC. As benchmarks, we use a range of problems, including structurally complex specifications of software systems and constraint satisfaction problems. The results show that while it is sometimes feasible to compute the model counts up to isomorphism using the full counts that are computed by the model counters, doing so suffers from poor scalability. The addition of symmetry breaking predicates substantially assists model counters. Domain-specific predicates are particularly useful, and in many cases can provide full symmetry breaking to enable highly efficient model counting up to isomorphism. We hope our study motivates new research on designing model counters that directly account for symmetries to facilitate further applications of model counting.
登录
查看更多内容
影响因子：
7.4
作者：
Galeotti, Juan P.;Rosner, Nicolas;Frias, Marcelo F.
通讯作者：
Frias, Marcelo F.
DOI：
10.1007/978-3-540-24605-3_37
发表时间：
2004-01-01
期刊：
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
影响因子：
--
作者：
Eén, N;Sörensson, N
通讯作者：
Sörensson, N
影响因子：
--
作者：
Borges, Mateus;Filieri, Antonio;Visser, Willem
通讯作者：
Visser, Willem
影响因子：
1
作者：
Bagheri, Hamid;Kang, Eunsuk;Jackson, Daniel
通讯作者：
Jackson, Daniel
影响因子：
5
作者：
Darwiche, A;Marquis, P
通讯作者：
Marquis, P