Download public CNF benchmark files with zsh scripts
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
2008_SAT-Race
2009_SAT09-competition
2010_SAT-Race
2011_SAT11_competition
2012_SAT_Challenge
2013_SAT_Competition
2014_SAT_Competition
2015_SAT-Race
2016_SAT_Competition
SATlib
README.adoc
complete-cnf-files-list.txt
duplicate-cnf-files.csv
problematic_files.txt

README.adoc

cnf-files-download

Download public CNF benchmark files with zsh scripts

Remarks

01_download.sh downloads files from an URL asynchronously and checks its SHA1 hashsum. 02_decompress.sh decompresses files such that CNF files can be used by SAT solvers.

  • On UNIX, you can list all CNF files using find . -type f -name '*.cnf' and all non-CNF files using find . -type f ! -name '*.cnf'

  • SAT competition 2014 contains many hidden lzma files. The contained CNF files cannot be decoded correctly and are therefore skipped. Equivalent non-hidden files exist and constitute actual CNF files.

  • It’s kind of awkward but even within a testsuite, duplicate files might occur. One example is Agile/bench_91.smt2.cnf as duplicate of Agile/bench_13367.smt2.cnf in CNF files of SAT 2016 competition.

  • MaxSAT benchmark files are not considered (different goal than simple SAT). The general URL is maxsat.udl.cat

  • I consider empty clauses to yield UNSAT immediately and are therefore pointless. I needed a blacklist.

    • You can find files with empty clauses in the following files of SATlib:

      • ./uuf200-860/UUF200.860.1000/*

      • ./uf100-430/uf100-*

      • ./uf20-91/uf20-*

      • ./uf125-538/ai/hoos/Research/SAT/Formulae/UF125.538.100/*

      • ./uf75-325/ai/hoos/Shortcuts/UF75.325.100/uf75-*

      • ./uuf175-753/UUF175.753.100/uuf175-*

      • ./uuf175-753/UUF175.753.100/uuf125-*

      • ./uuf50-218/UUF50.218.1000/uuf50-*

      • ./uuf100-430/UUF100.430.1000/uuf100-*

      • ./uuf75-325/UUF75.325.100/uuf75-*

      • ./uf250-1065/ai/hoos/Shortcuts/UF250.1065.100/uf250-*

      • ./uf225-960/ai/hoos/Shortcuts/UF225.960.100/uf225-*

      • ./uuf225-960/UUF225.960.100/uuf225-*

      • ./uf50-218/uf50-*

      • ./uf175-753/ai/hoos/Research/SAT/Formulae/UF175.753.100/uf175-*

      • ./uuf150-645/UUF150.645.100/uuf150-*

      • ./uuf250-1065/UUF250.1065.100/uuf250-*

      • ./uf150-645/ai/hoos/Research/SAT/Formulae/UF150.645.100/uf150-*

      • ./uf200-860/uf200-*

    • Be aware that supposedly "%" in an individual line (is not to be ignored but) terminates the CNF file and therefore empty clauses do not occur with this kind of semantics. However, an actual empty clause was found in SAT Race 2010 files:

      • ./software-verification/post/zfcp.cnf at line 695486

  • I couldn’t decompress the following files with my xubuntu/debian software stack in SATlib:

    • gzip: dlx_iq_unsat_2.0/1dlx_c_mc_ex_bp_f_iq33_a.cnf.gz: invalid compressed data—​crc error

    • gzip: dlx_iq_unsat_2.0/1dlx_c_mc_ex_bp_f_iq33_a.cnf.gz: invalid compressed data—​length error

    • gzip: vliw_sat_2.0/9dlx_vliw_at_b_iq6_bug10.cnf.gz: unexpected end of file

  • sc14-app.tar of SAT competition 2014 contains an empty archive sc14-app.tar in itself

best regards, prokls