A Study of Symmetry Breaking Predicates and Model Counting
117
ProjMC embody very different algorithms for model counting and provide us
a diverse set of tools for the study. ApproxMC employs novel approximation
methods to efficiently predict highly accurate model counts with formal guarantees, and is now in its third generation (called ApproxMC3 [52]). ProjMC uses
a recursive algorithm and employs a disjunctive decomposition method together
with a search for disjoint components, and just had its first public release.
As benchmark formulas, we use a range of problems, including structurally
complex specifications of software systems [34] and constraint satisfaction problems [45]. To create the benchmark formulas, we employ the Alloy toolset [34]
and its Kodkod backend [58]. Alloy allows writing formulas in relational first
order logic with transitive closure, and has been used in academia and industry for design and specification of systems [11, 18, 35, 37, 65, 67, 70] as well as
for various forms of analyses of code [27, 32, 36, 42, 48, 69]. The Alloy analyzer
translates Alloy formulas with respect to a scope, i.e., bound on the universe of
discourse, into propositional logic to create CNF problems that are solved using
off-the-shelf SAT solvers [25]. Alloy supports fully automatic (partial) symmetry
breaking at the level of Alloy specifications [51,57] by adapting Crawford’s symmetry breaking predicates [20], which are statically added to the formula before
the solvers solve it. Alloy provides an ideal vehicle for evaluating the different
approaches to symmetry breaking that are our focus in this study.
Similar to other techniques that use CNF-based backends, the Alloy analyzer translates problems from a higher-level (Alloy) to a lower-level (CNF).
This translation often introduces new boolean variables in the resulting formula,
which are not essential for creating the CNF formula but are required for a
compact (feasible) encoding in CNF [60]. As a result, the translated formula
is equisatisfiable to the original formula but may not be equivalent to it, and
hence it may be the case that the model count for the CNF formula is very
different from the original formula. Several modern model counters [16, 40, 50]
readily handle this case by providing support for projected model counting [10],
i.e., computing the model count with respect to a subset of all the variables. For
Alloy, the subset is the primary variables, i.e., all boolean variables that directly
correspond to the variables in the Alloy specification.
For each benchmark formula f , we create three model counting problems
using automatic tools: 1) f with no symmetry breaking, which we create by
setting Alloy’s default symmetry breaking to off ; 2) f with symmetry breaking predicates added at the problem domain level, which we create by having
Alloy’s default symmetry breaking turned on; and 3) f with symmetry breaking predicates added at the CNF level, which we create by first using Alloy to
create a CNF formula with no domain-level symmetry breaking, and then using the BreakID [23] tool to add CNF-level symmetry breaking predicates using
its default settings. In addition, for select benchmarks we create formulas with
manually added domain-specific symmetry breaking predicates, which we write
in Alloy following previous work [38].
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
117
ProjMC embody very different algorithms for model counting and provide us
a diverse set of tools for the study. ApproxMC employs novel approximation
methods to efficiently predict highly accurate model counts with formal guarantees, and is now in its third generation (called ApproxMC3 [52]). ProjMC uses
a recursive algorithm and employs a disjunctive decomposition method together
with a search for disjoint components, and just had its first public release.
As benchmark formulas, we use a range of problems, including structurally
complex specifications of software systems [34] and constraint satisfaction problems [45]. To create the benchmark formulas, we employ the Alloy toolset [34]
and its Kodkod backend [58]. Alloy allows writing formulas in relational first
order logic with transitive closure, and has been used in academia and industry for design and specification of systems [11, 18, 35, 37, 65, 67, 70] as well as
for various forms of analyses of code [27, 32, 36, 42, 48, 69]. The Alloy analyzer
translates Alloy formulas with respect to a scope, i.e., bound on the universe of
discourse, into propositional logic to create CNF problems that are solved using
off-the-shelf SAT solvers [25]. Alloy supports fully automatic (partial) symmetry
breaking at the level of Alloy specifications [51,57] by adapting Crawford’s symmetry breaking predicates [20], which are statically added to the formula before
the solvers solve it. Alloy provides an ideal vehicle for evaluating the different
approaches to symmetry breaking that are our focus in this study.
Similar to other techniques that use CNF-based backends, the Alloy analyzer translates problems from a higher-level (Alloy) to a lower-level (CNF).
This translation often introduces new boolean variables in the resulting formula,
which are not essential for creating the CNF formula but are required for a
compact (feasible) encoding in CNF [60]. As a result, the translated formula
is equisatisfiable to the original formula but may not be equivalent to it, and
hence it may be the case that the model count for the CNF formula is very
different from the original formula. Several modern model counters [16, 40, 50]
readily handle this case by providing support for projected model counting [10],
i.e., computing the model count with respect to a subset of all the variables. For
Alloy, the subset is the primary variables, i.e., all boolean variables that directly
correspond to the variables in the Alloy specification.
For each benchmark formula f , we create three model counting problems
using automatic tools: 1) f with no symmetry breaking, which we create by
setting Alloy’s default symmetry breaking to off ; 2) f with symmetry breaking predicates added at the problem domain level, which we create by having
Alloy’s default symmetry breaking turned on; and 3) f with symmetry breaking predicates added at the CNF level, which we create by first using Alloy to
create a CNF formula with no domain-level symmetry breaking, and then using the BreakID [23] tool to add CNF-level symmetry breaking predicates using
its default settings. In addition, for select benchmarks we create formulas with
manually added domain-specific symmetry breaking predicates, which we write
in Alloy following previous work [38].
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