bigbug / concealsatgen

Generates hard satisfiable CNF formulas in DIMACS format with a known solution. Authors: Jan-Hendrik Lorenz and Florian Wörz.

concealSATgen

Generates hard satisfiable CNF formulas in DIMACS format with a known solution.

Authors: Jan-Hendrik Lorenz and Florian Wörz.

About

concealSATgen is a tool written in Python that allows the generation of hard satisfiable CNF formulas in DIMACS format with a known solution. The tool implements the clause distribution control (CDC) algorithm proposed by [Barthel et al. 2002] and further elaborated in [Balyo & Chrpa 2018].

Let denote the width of the wanted clauses. Furthermore let denote the clause-to-variable ratio. Let be a given solution that one wants to hide in the generated formula. For the parameter represent the probability of adding a randomly sampled -clause which has exactely satisfied literals under .

A popular way to choose the parameters is the -hidden algorithm of [Jia, Moore & Strain 2005] that defines for a given parameter .

Getting Started

Example

To generate a 3-CNF formula with 10 variables and 4 clauses according to the above model, call

python3 generator.py -n 10 -m 4

The generated output file gen_n10_m4_k3SAT_seed42.cnf might look something like this:

c This file was generated by concealSATgen
c Created by python3 generator.py -n 10 -m 4
c Hidden solution: 1 2 4 5 6 7 8 10
c p-values 1.00 1.00 1.00
p cnf 10 4
-9 6 -3 0
2 8 -4 0
2 -7 10 0
-1 -9 5 0

Parameters

After python3 generator.py you can specify the following flags:

• -n (int): Specifies the number of variables in the formula.
• -m (int): Specifies the number of clauses in the formula.
• -k (int): Specifies the width of the formula.
• -p (float float ... float): Specifies the values as described above.
• -s (int): The seed to initialize the random number generator.
• -F (str): The path to the file with contains the wanted hidden solution.
• -o (str): The output-path to save the generated cnf-file.

The parameters n and m are required.

If the other parameters are not specified, the program will use the following default values:

• .
• for all .
• .
• A random hidden solution will be generated according to the given seed.
• o = './' (that is the cnf-file will be generated in the directory of generator.py).

Limitations

Important Note: The generator does as of now not really check whether the given parameters can yield a formula. E.g. calling

python3 generator.py -n 10 -m 3

does not terminate (quickly) as there cannot be a 3 CNF formula with 10 variables but only 3 clauses.

Prerequisites

Python3

Running the tests

Open a terminal window in the root folder of the project and type

./test_all_python_scripts.sh

to run unit tests on all involved Python scripts.

Authors

• Jan-Hendrik Lorenz - Florian Wörz (Institute of Theoretical Computer Science, Ulm University, Germany)

If you use concealSATgen in scientific work, please cite:

• Jan-Hendrik Lorenz, and Florian Wörz. "concealSATgen", 2020

Acknowledgments

The concealSATgen project has been partially funded by the German Research Foundation (Deutsche Forschungsgemeinschaft DFG).

License

This project is licensed under the Creative Commons Attribution 4.0 International License - see the LICENSE file for details

References

Balyo T.; Chrpa, L. 2018. Using Algorithm Configuration Tools to Generate Hard SAT Benchmarks. Proceedings of the SAT Competition 2018 - Solver and Benchmark Descriptions. The Eleventh International Symposium on Combinatorial Search (SoCS 2018).

Barthel, W.; Hartmann, A. K.; Leone, M.; Ricci-Tersenghi, F.; Weigt, M.; and Zecchina, R. 2002. Hiding solutions in random satisfiability problems: A statistical mechanics approach. Physical review letters 88(18):188701.

Jia, H.; Moore, C.; and Strain, D. 2005. Generating hard satisfiable formulas by hiding solutions deceptively. In Proceedings of the National Conference on Artificial Intelligence, volume 20, 384.