A Study of Symmetry Breaking Predicates and Model Counting
125
each model counting problem, we list the primary variables in the input CNF file
as a comment as required by ApproxMC. For exact model counting, we use the
latest public release of ProjMC [40] (http://www.cril.univ-artois.fr/kc/
projmc.html). For each model counting problem, we list the primary variables
in a separate file as required by ProjMC.
4.2 Benchmarks
Base formulas. We use four sources of base formulas.
(1) Alloy specs. We consider all Alloy specifications in the standard distribution [1]; each command in an Alloy spec defines a constraint solving problem
and provides a scope; we use the given scope. We remove unsatisfiable problems
since their model count is 0 (regardless of symmetry breaking), and our focus
in this study is on satisfiable problems. We also remove all “easy” cases that
complete within 1 second for both tools and all symmetry settings. This creates
a set of 47 base problems derived from Alloy specifications.
(2) Kodkod problems. We consider all Kodkod programs in the standard distribution [5]. Once again, we remove the unsatisfiable problems and “easy” cases.
In addition, we remove problems that do not admit symmetry breaking, i.e.,
where Kodkod does not add any symmetry breaking by default (e.g., when there
is a given partial solution, which prevents Kodkod’s greedy base partitioning [57]
from having an effect). Some of the Kodkod programs are parameterized over
integer bounds and input files. We manually create those inputs in the appropriate format. This gives us a total of 13 base problems derived from Kodkod
programs.
(3) n-Queens. We use 2 common variations of the n-Queens problem: 1) k queens
are placed on a k × k board (1 ≤ k ≤ 12); 2) 3 queens are placed on a k × k
board (1 ≤ k ≤ 12). This gives us a total of 24 base problems derived from the
n-Queens problem
5 .
(4) Complex data structures. We use 6 complex data structures: (1) singly-linked
lists; (2) sorted lists; (3) doubly-linked lists; (4) binary trees; (5) binary search
trees; and (6) red-black trees. For each structure, we bound the number of nodes
to be between 6 and 9 (inclusive). This gives us a total of 24 base problems based
on structural invariants.
Model counting benchmarks. For each base formula f , we create 3 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 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 the same arguments as in the SATRACE’15 competition [3]; and 3) f with
symmetry breaking predicates added at the problem domain level, which we create by having Alloy’s default symmetry breaking turned on. Moreover, for data
5 Unfortunately, we were not able to get the results for majority of the n-Queens
benchmarks with ProjMC due to an unknown issue with the tool, so we do not
use the n-Queens benchmarks for experiments with ProjMC; we have requested the
ProjMC team to look into the issue.
125
each model counting problem, we list the primary variables in the input CNF file
as a comment as required by ApproxMC. For exact model counting, we use the
latest public release of ProjMC [40] (http://www.cril.univ-artois.fr/kc/
projmc.html). For each model counting problem, we list the primary variables
in a separate file as required by ProjMC.
4.2 Benchmarks
Base formulas. We use four sources of base formulas.
(1) Alloy specs. We consider all Alloy specifications in the standard distribution [1]; each command in an Alloy spec defines a constraint solving problem
and provides a scope; we use the given scope. We remove unsatisfiable problems
since their model count is 0 (regardless of symmetry breaking), and our focus
in this study is on satisfiable problems. We also remove all “easy” cases that
complete within 1 second for both tools and all symmetry settings. This creates
a set of 47 base problems derived from Alloy specifications.
(2) Kodkod problems. We consider all Kodkod programs in the standard distribution [5]. Once again, we remove the unsatisfiable problems and “easy” cases.
In addition, we remove problems that do not admit symmetry breaking, i.e.,
where Kodkod does not add any symmetry breaking by default (e.g., when there
is a given partial solution, which prevents Kodkod’s greedy base partitioning [57]
from having an effect). Some of the Kodkod programs are parameterized over
integer bounds and input files. We manually create those inputs in the appropriate format. This gives us a total of 13 base problems derived from Kodkod
programs.
(3) n-Queens. We use 2 common variations of the n-Queens problem: 1) k queens
are placed on a k × k board (1 ≤ k ≤ 12); 2) 3 queens are placed on a k × k
board (1 ≤ k ≤ 12). This gives us a total of 24 base problems derived from the
n-Queens problem
5 .
(4) Complex data structures. We use 6 complex data structures: (1) singly-linked
lists; (2) sorted lists; (3) doubly-linked lists; (4) binary trees; (5) binary search
trees; and (6) red-black trees. For each structure, we bound the number of nodes
to be between 6 and 9 (inclusive). This gives us a total of 24 base problems based
on structural invariants.
Model counting benchmarks. For each base formula f , we create 3 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 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 the same arguments as in the SATRACE’15 competition [3]; and 3) f with
symmetry breaking predicates added at the problem domain level, which we create by having Alloy’s default symmetry breaking turned on. Moreover, for data
5 Unfortunately, we were not able to get the results for majority of the n-Queens
benchmarks with ProjMC due to an unknown issue with the tool, so we do not
use the n-Queens benchmarks for experiments with ProjMC; we have requested the
ProjMC team to look into the issue.