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<br>"CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving"<br><br>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.<br>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<br>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<br>A subset of the benchmark problems used is available in the directory <b>/subsent_cnfs</b>. All symmetries were computed with two different tools: saucy3 and bliss.<br>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 <b>/sources</b> directory.<br>Instructions for installation and running the included benchmarks are provided in the <b>README</b>.<br>Output from the included benchmarks is include in the file <b>TACAS-QUAD.csv</b>.