CNF Symmetry Breaking Options in Conflict Driven SAT Solving

Many CNF formulas representing real-world problems exhibit symmetries. Various efforts have been made to deal with these symmetries efficiently. After Crawford et al [2], which gives a theoretical framework for detecting and exploiting symmetries, different suggestions have been posed to prevent the exponential blow up of overhead costs which shows up performing so-called full symmetry breaking. Aloul et al [1] give an overview of these preprocessing methods and they present a new device (Shatter) which tries to eliminate the costs of overhead substantially. We propose an alternative way of symmetry breaking in cases where conflict-clause driven Sat solvers are used in solving the CNF at hand. Instead of preprocessing the formula involved we investigate the effect of applying permutations of the symmetry group on the emerging conflict-clauses only and to add them to the conflict-clause list additionally. We use random graph k-colourings in this experimental study, first because difficult examples can be generated easily and second because of the fact that the size of the full symmetry group grows exponentially in k. In doing so we are able to obtain a clear picture of the trade-off between costs of overhead and gains of dealing with smaller search trees. We compare our results with the Shatter preprocessing option and we selected the conflict driven zChaff Sat solver [3] as a standard representative of the family of conflict driven solvers.