• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
A Study of Symmetry Breaking Predicates and Model Counting.
Wenxi Wang, Muhammad Usman, Alyas Almaawi, Kaiyuan Wang, Kuldeep S. Meel and Sarfraz Khurshid.
In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), April 2020.
Propositional model counting is a classic problem that hasrecently witnessed many technical advances and novel applications. Whilethe basic model counting problem requires computing the number of allsolutions to the given formula, in some important application scenarios,the desired count is not of all solutions, but instead, of all unique solutionsup to isomorphism. In such a scenario, the user herself must try toeither use the full count that the model counter returns to compute thecount up to isomorphism, or ensure that the input formula to the modelcounter adequately captures the symmetry breaking predicates so it candirectly report the count she desires.We study the use of CNF-level and domain-level symmetry breakingpredicates in the context of the state-of-the-art in model counting, specificallythe leading approximate model counter ApproxMC and the recentlyintroduced exact model counter ProjMC. As benchmarks, we usea range of problems, including structurally complex specifications of softwaresystems and constraint satisfaction problems. The results show thatwhile it is sometimes feasible to compute the model counts up to isomorphismusing the full counts that are computed by the model counters,doing so suffers from poor scalability. The addition of symmetry breakingpredicates substantially assists model counters. Domain-specific predicatesare particularly useful, and in many cases can provide full symmetrybreaking to enable highly efficient model counting up to isomorphism.We hope our study motivates new research on designing model countersthat directly account for symmetries to facilitate further applications ofmodel counting.
@inproceedings{WUAWMK20,
title={A Study of Symmetry Breaking Predicates and Model Counting},
author={Wang, Wenxi and Usman, Muhammad and Almaawi, Alyas and Wang, Kaiyuan and Meel, Kuldeep S. and Khurshid, Sarfraz},
booktitle=TACAS,
month=apr,
year={2020},
bib2html_rescat={Counting},
bib2html_pubtype={Refereed Conference},
bib2html_dl_pdf={../Papers/tacas20.pdf},
abstract={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.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51