116
W. Wang et al.
probabilistic analyses [13, 26, 28], check and repair string manipulation code [9,
41], and estimate information leakage using quantified information flow [19, 44].
While the basic model counting problem requires computing the number
of all solutions, in some important application scenarios, the desired count is
not of all solutions, but instead, of all unique solutions up to isomorphism, i.e.,
non-isomorphic (also called non-symmetric) solutions. For example, consider the
context of software reliability analysis [26] where a goal is to find the number of
inputs that can lead to an assertion violation, or bounded exhaustive testing [14,
42, 62, 68] where the goal is to estimate the total number of inputs that exist for
a certain bound on the input size to decide what bound to use to stay within
the testing budget. The desired counts in these cases are of non-isomorphic
inputs, which are non-equivalent with respect to behaviors that a program can
have because two inputs that are equivalent (and possibly not identical) produce
the same output [66]. As another example, consider computing the number of
solutions to a constraint satisfaction problem (CSP) [45], e.g., the number of
unique ways 8 queens can be arranged on a fixed chess board such that no queen
is under attack [6]. Once again, one is typically interested in the number of
non-symmetric solutions because the indistinguishability of queens implies that
a user does not consider two solutions obtained by swapping positions of queens
to be unique.
In such scenarios, the user has two basic options. One option is to compute
the full count using the model counter, and then use mathematical reasoning
about symmetries to project the full count to the desired count. Doing so is
straightforward in some cases, e.g., if each solution consists of n indistinguishable
objects of the same type and the composition of each solution implies that each
permutation of those n objects leads to a distinct (albeit isomorphic) solution,
dividing the full count by n! gives the count for non-isomorphic solutions; doing
so is however, not always easy, for example when different solutions have different
number of objects that can be permuted to form non-identical solutions. The
other option is to ensure the formula that is input to the model counter includes
symmetry breaking predicates [20, 21], i.e., additional constraints that only allow
canonical solutions from each isomorphism class, so the model counter can report
the desired count.
Symmetry breaking predicates can be added using three basic approaches [29].
Perhaps the most common approach is to add them at the CNF-level by using
an off-the-shelf tool [8,23], which takes as input a CNF formula and creates symmetry breaking predicates for it. Another common approach is to create them at
the problem domain level using a domain-specific tool [58], and then translate
the formula and predicates together to CNF. A third approach is to add them
manually at the problem domain level [38, 59], and then translate to CNF.
A goal of our work is to study what is the best way to add symmetry breaking predicates (if at all) to obtain precise counts of non-isomorphic solutions.
We conduct the study in the context of the state-of-the-art in model counting, specifically the leading approximate model counter ApproxMC [16, 17, 52]
and the recently introduced exact model counter ProjMC [40]. ApproxMC and
W. Wang et al.
probabilistic analyses [13, 26, 28], check and repair string manipulation code [9,
41], and estimate information leakage using quantified information flow [19, 44].
While the basic model counting problem requires computing the number
of all solutions, in some important application scenarios, the desired count is
not of all solutions, but instead, of all unique solutions up to isomorphism, i.e.,
non-isomorphic (also called non-symmetric) solutions. For example, consider the
context of software reliability analysis [26] where a goal is to find the number of
inputs that can lead to an assertion violation, or bounded exhaustive testing [14,
42, 62, 68] where the goal is to estimate the total number of inputs that exist for
a certain bound on the input size to decide what bound to use to stay within
the testing budget. The desired counts in these cases are of non-isomorphic
inputs, which are non-equivalent with respect to behaviors that a program can
have because two inputs that are equivalent (and possibly not identical) produce
the same output [66]. As another example, consider computing the number of
solutions to a constraint satisfaction problem (CSP) [45], e.g., the number of
unique ways 8 queens can be arranged on a fixed chess board such that no queen
is under attack [6]. Once again, one is typically interested in the number of
non-symmetric solutions because the indistinguishability of queens implies that
a user does not consider two solutions obtained by swapping positions of queens
to be unique.
In such scenarios, the user has two basic options. One option is to compute
the full count using the model counter, and then use mathematical reasoning
about symmetries to project the full count to the desired count. Doing so is
straightforward in some cases, e.g., if each solution consists of n indistinguishable
objects of the same type and the composition of each solution implies that each
permutation of those n objects leads to a distinct (albeit isomorphic) solution,
dividing the full count by n! gives the count for non-isomorphic solutions; doing
so is however, not always easy, for example when different solutions have different
number of objects that can be permuted to form non-identical solutions. The
other option is to ensure the formula that is input to the model counter includes
symmetry breaking predicates [20, 21], i.e., additional constraints that only allow
canonical solutions from each isomorphism class, so the model counter can report
the desired count.
Symmetry breaking predicates can be added using three basic approaches [29].
Perhaps the most common approach is to add them at the CNF-level by using
an off-the-shelf tool [8,23], which takes as input a CNF formula and creates symmetry breaking predicates for it. Another common approach is to create them at
the problem domain level using a domain-specific tool [58], and then translate
the formula and predicates together to CNF. A third approach is to add them
manually at the problem domain level [38, 59], and then translate to CNF.
A goal of our work is to study what is the best way to add symmetry breaking predicates (if at all) to obtain precise counts of non-isomorphic solutions.
We conduct the study in the context of the state-of-the-art in model counting, specifically the leading approximate model counter ApproxMC [16, 17, 52]
and the recently introduced exact model counter ProjMC [40]. ApproxMC and