CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving

This dataset includes source code, benchmarks and dependencies to reproduce the work presented in the TACAS 18 paper entitled
"CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving"

Boolean satisfiability (SAT) is an area of active research with numerous applications. Increasingly, the development of approaches that can treat increasingly complex SAT problems has become a focus. This dataset and the related paper introduce a novel method of dynamically exploiting symmetries to speed up the solving of SAT problems.
This new approach is implemented as a C++ library called cosy. cosy can be interfaced with virtually any conflict-driven clauses learning (CDCL) SAT solver. In this instance it has been integrated with the SAT solver MiniSAT, termed MiniSym
MiniSym is evaluated against 3 existing SAT solvers: - MiniSAT, as a reference without symmetry handling- Shatter, a symmetry breaking pre-processor coupled with MiniSAT- breakID, another symmetry breaking pre-processory also coupled with MiniSAT
A subset of the benchmark problems used is available in the directory /subsent_cnfs. All symmetries were computed with two different tools: saucy3 and bliss.
Source code for all 3 solvers, including the cosy + Mini SAT implementation, as well as both the saucy3 and bliss tools, are provided in the /sources directory.
Instructions for installation and running the included benchmarks are provided in the README.
Output from the included benchmarks is include in the file TACAS-QUAD.csv.