Benchmarks and SAT solver runtimes from the competition

Context and methodology

• This experiment aims to give an answer how various simmetry breaking techniques
  influence the run-time and effectiveness of modern SAT solvers. Symmetry breaking is a
  well-known preprocessing and reasoning strategy that reduces redundant search space
  by identifying and eliminating symmetrical solutions. The research question is the
  following: How much does symmetry breaking improve solver efficiency, and which
  methods – static or dynamic – perform better on different instances? The focus of the
  experiment is to quantify the performance impact of these methods on various
  benchmark instances.
• The third-party dataset was collected from SAT Solver competetions, these datas can be accessed publicly.
• The data during the project is created by python codes running on different CNF benchmark inputs.

Technical details

• The defined naming conventions are the following (only fow the codes and created datas): for codes: [code_name]_[vX].[type] - where X is the version number for datas/plots: [date]_[name].[type] - date format: YYYYMMDD.

• The folder structure of the project:  

  symmetry-breaking-sat-experiment/

  /data                 

  /processed                 

  /raw            

  /code            

  /metadata            

  /results

  LICENSE.txt

  README.md 

• The CSV files are broadly supported, therefore, the software and tools to reuse these datas depend on the methodology of the user.  The CFN files can be reused with the python codes provided in the 'codes' folder. The expected python version and additional dependencies are listed in the README.md file in the corresponding folder.

• There is a matedata describing the whole research project including the subject, data types, language ect.  The project folder also contains metadatas at each file level describing that specific file in the current folder. Each metadata gives a title name for the file and describes the subject of the file and contains all specifications of the file. This will help others to identify, discover and reuse our data.

• The project folder contains a README.md file in each folder, thus every part of the project is documented. This facilitates the data reuse because the user gets an immediate overview of the project structure and content.

Further details

• Legal restrictions on how data is processed and shared are specified in the The restrictions for third-party data are specified in the LICENSE.txt file.. The restrictions relate to datasets R1 (SAT Competition 2023 Main Track Benchmarks). The legal restrictions are based on the following: The 'SAT Competition 2023 Main Track Benchmarks' used for evaluation is a third-party data.Copyright and usage rights for these benchmarks remain with the respective authors and the SAT Competition organizers.

• The data files created for this experiment (CSV, JSON, plots, metadata)
  are released under the Creative Commons Attribution 4.0 (CC-BY 4.0) license.

  The code files created for this experiment (Python) are released under the MIT license.

  External datasets (SAT Competition Benchmarks and Solver Results) retain
  their original licenses and are not covered by this license.