Generates hard satisfiable CNF formulas in DIMACS format with a known solution.
Authors: Jan-Hendrik Lorenz and Florian Wörz.
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
represents the probability of adding a randomly sampled
-clause which has exactly
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
.
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
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 widthof the formula.
-p(float float ... float): Specifies the valuesas 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 ofgenerator.py).
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.
Python3
Open a terminal window in the root folder of the project and type
python -m unittest tests/test_generator.py
to run unit tests on all involved Python scripts.
- 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", 2021
The concealSATgen project has been partially funded by the German Research Foundation (Deutsche Forschungsgemeinschaft DFG).
This project is licensed under the Creative Commons Attribution 4.0 International License - see the LICENSE file for details
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.