130
W. Wang et al.
detailed study to explain the observed behavior is beyond the scope of this work,
we offer some explanations. As pointed out by Soos and Meel [52], over 99% of
the runtime of ApproxMC is consumed by the underlying SAT solver handling
CNF-XOR formulas. The usage of symmetry breaking predicates for satisfiable
instances typically leads to smaller overheads in runtime in the context of satisfiability queries. As discussed above, the use of symmetry breaking predicates
significantly reduces the number of solutions and thereby leads to the significant
reduction in the number of XORs to be added by ApproxMC. Note that the
number of XORs to be added is logarithmically proportional to the number of
solutions of a formula. The performance of SAT solvers has been observed to be
sensitive to the number of XORs [24] and therefore, we believe that reduction
in the required number of XORs is the primary reason behind the performance
improvements in the context of ApproxMC.
The performance improvement of ProjMC is, however, more surprising since
it is not necessarily the case that reduction in the number of solutions would lead
to reduction in the size of the corresponding d-DNNF (decision-Deterministic Decomposable Negation Normal Form), which represents the trace of the execution
of ProjMC [33]. Furthermore, given the lack of noticable difference in runtime
performance improvement via off-the-shelf symmetry breaking tools, it would
be an interesting direction of future work to understand the difference in the
traces between the formulas generated via Alloy’s default symmetry breaking
and CNF-level symmetry breaking.
6 Conclusions
This paper presented, to the best of our knowledge, the first study of symmetry
breaking and model counting. A goal of the study was to determine what is the
best way to add symmetry breaking predicates (if at all) to obtain precise counts
of non-isomorphic solutions. We studied two model counters from two different
classes and four scenarios of applying symmetry breaking. A key lesson of our
study is that domain-specific symmetry breaking predicates are most effective
at enabling precise computation of model counts up to isomorphism. We believe
the results of our study can provide insights into more effective use of cutting
edge model counters in important domains where the number of unique solutions
up to isomorphism is desired, and also enable developing novel model counting
methods that exploit symmetries.
Acknowledgments
This work was supported in part by the U.S. National Science Foundation Grant
CCF-1718903, and the National Research Foundation Singapore under its AI
Singapore Programme [AISG-RP-2018-005].
W. Wang et al.
detailed study to explain the observed behavior is beyond the scope of this work,
we offer some explanations. As pointed out by Soos and Meel [52], over 99% of
the runtime of ApproxMC is consumed by the underlying SAT solver handling
CNF-XOR formulas. The usage of symmetry breaking predicates for satisfiable
instances typically leads to smaller overheads in runtime in the context of satisfiability queries. As discussed above, the use of symmetry breaking predicates
significantly reduces the number of solutions and thereby leads to the significant
reduction in the number of XORs to be added by ApproxMC. Note that the
number of XORs to be added is logarithmically proportional to the number of
solutions of a formula. The performance of SAT solvers has been observed to be
sensitive to the number of XORs [24] and therefore, we believe that reduction
in the required number of XORs is the primary reason behind the performance
improvements in the context of ApproxMC.
The performance improvement of ProjMC is, however, more surprising since
it is not necessarily the case that reduction in the number of solutions would lead
to reduction in the size of the corresponding d-DNNF (decision-Deterministic Decomposable Negation Normal Form), which represents the trace of the execution
of ProjMC [33]. Furthermore, given the lack of noticable difference in runtime
performance improvement via off-the-shelf symmetry breaking tools, it would
be an interesting direction of future work to understand the difference in the
traces between the formulas generated via Alloy’s default symmetry breaking
and CNF-level symmetry breaking.
6 Conclusions
This paper presented, to the best of our knowledge, the first study of symmetry
breaking and model counting. A goal of the study was to determine what is the
best way to add symmetry breaking predicates (if at all) to obtain precise counts
of non-isomorphic solutions. We studied two model counters from two different
classes and four scenarios of applying symmetry breaking. A key lesson of our
study is that domain-specific symmetry breaking predicates are most effective
at enabling precise computation of model counts up to isomorphism. We believe
the results of our study can provide insights into more effective use of cutting
edge model counters in important domains where the number of unique solutions
up to isomorphism is desired, and also enable developing novel model counting
methods that exploit symmetries.
Acknowledgments
This work was supported in part by the U.S. National Science Foundation Grant
CCF-1718903, and the National Research Foundation Singapore under its AI
Singapore Programme [AISG-RP-2018-005].