Tags:Knowledge Compilation, Sentential Decision Diagram and Symmetry breaking

Abstract:

Constraint Programming is a powerful method to solve combinatorial problems, but due to a large search space, solving can be very time consuming. Diagnosis, planning, product configuration are example use cases. These systems are often used in an online format answering queries. Compilation methods were developed to deal with the complexity of solving the problems offline and create a representation that is able to answer queries in polynomial time. Symmetry breaking is the addition of constraints to eliminate symmetries, thus in general speeding up search and reducing the number of solutions. Knowledge compilation looks at finding succinct representations that are also tractable, that is, they support queries and transformations in polytime. Finding the smallest representation is often the bottleneck of compilation methods. Compiled representations are Directed Acyclic Graphs representing the set of all solutions. In this paper we investigate if breaking symmetries, that is representing less solutions, always leads to a smaller compiled representation? We considered four compilers and three highly symmetrical problems. A reduction is observed in all the problems for the compilation size when we break symmetries, with top-down compilers obtaining more reduction.