Published May 24, 2024
| Version v1
Other
Open
supplementary material for paper 'Small unsatisfiable k-CNFs with bounded literal occurrence'
Description
This is the supplementary material for the paper 'Small unsatisfiable k-CNFs with bounded literal occurrence'. You will find
- `qcir-gen.py`: a Python script for generating the various SAT encodings we used in the paper. For more information on the parameters, type `python qcir-gen.py --help`. To run it, it is required to have the PySAT package installed.
- `parseQCIR.py`: a Python script from converting a QCIR formula into a format that SMS understands and pass it on to SMS.
- `two_doms`, `two_doms_models`: additional file for cubing assuming there are at least two dominating clauses. Please keep under the same directory as `qcir-gen.py`.
- `unique_models_10`, `unique_models_11`, `unique_models_12`: additional file for cubing assuming there is a unique dominating clause. Please keep under the same directory as 'qcir-gen.py'.
- `saturation-algorithm-main.zip`: a C++ implementation of a saturation algorithm that gives the size of the smallest minimally unsatisfiable (k,p,q)-formula which has 1 less variable than the number of clauses.
Download SMS from `https://github.com/markirch/sat-modulo-symmetries`, and follow the installation instructions.
To run SMS on a QCIR formula generated by 'qcir-gen.py', do `python parseQCIR.py -f name_of_file --vertices 2n+m --args-SMS '--initial-partition 2n m`. The exact initial partition to start SMS with might differ depending on the parameters used when generating the QCIR formula. Please refer to the paper for the initial partition to use in each situation.
Files
supplementary_material_smallest_k_CNF.zip
Files
(102.8 kB)
| Name | Size | Download all |
|---|---|---|
|
md5:a98d3544d736ccf3f23b9922100d468e
|
102.8 kB | Preview Download |