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>.

本数据集包含用于复现发表于TACAS 2018会议、题为《CDCLSym：在SAT求解中引入有效对称性破缺》的论文相关工作的源代码、基准测试集与依赖库。

布尔可满足性（Boolean Satisfiability，简称SAT）是当前活跃的研究领域，应用场景广泛。针对日益复杂的SAT问题的求解方法研发，已成为该领域的核心关注点。本数据集与相关论文提出了一种全新的动态对称性利用方法，用以加速SAT问题的求解过程。

该新方法被实现为一个名为cosy的C++库。cosy几乎可与任意冲突驱动子句学习（conflict-driven clauses learning，CDCL）SAT求解器对接，本工作中它已与SAT求解器MiniSAT集成，集成后的版本被称为MiniSym。

研究人员将MiniSym与三款现有SAT求解器进行对比评估：
- 未搭载对称性处理模块的基准求解器MiniSAT；
- 与MiniSAT联用的对称性破缺预处理器Shatter；
- 另一款与MiniSAT联用的对称性破缺预处理器breakID。

所用基准测试集的子集可在目录<b>/subsent_cnfs</b>中获取。所有对称性均通过两款不同工具计算得到：saucy3与bliss。

三款求解器（包括cosy与MiniSAT的集成实现）以及saucy3、bliss两款工具的源代码，均存放于<b>/sources</b>目录中。

安装并运行本数据集附带的基准测试集的操作说明，详见<b>README</b>文件。

附带基准测试集的运行结果已存储于文件<b>TACAS-QUAD.csv</b>中。