Source code and benchmarks for the paper "Investigating the Existence of Holey Latin Squares via Satisfiability Testing".
The benchmarks we used include holey Latin squares (HLSs) of 39 different hole types. For each hole type, instances satisfying the identity (1) to (7) were generated respectively, resulting in a total of 273 instances.
A specific HLS instances can be generated using the following command:
python hls_to_sat.py --order {order} --cat {identity} --amo {amo_type} --holes {hole_type} --postfix {hole_type_str}| Parameter | Range | Description | Example |
|---|---|---|---|
| order | int | The order of the HLS | 7 |
| identity | {0,1,2,...,7} | The identity that needs to be satisfied (use 0 if no identity) | 1 |
| amo_type | {"pairwise","binary","ladder"} | The type of at-most-one encoding | pairwise |
| hole_type | string | Specify the hole sets using 2d-array format | "[[0],[1],[2],[3],[4],[5,6]]" |
| hole_type_str | string | Describe the hole type | "1^5_2^1" |
The generated instances will be saved in the current directory with the filename hls_{order}_{identity}_{hole_type_str}_{amo_type} by default.
For convenience, we also provide a script to generate all instances, which can be executed by running sh gen_cnf.sh {amo_type}.
A specific HLS instances for MiniZinc can be generated using the following command:
python hls_to_cp.py {order} {identity} {hole_type} {hole_type_str}| Parameter | Range | Description | Example |
|---|---|---|---|
| order | int | The order of the HLS | 7 |
| identity | {0,1,2,...,7} | The identity that needs to be satisfied (use 0 if no identity) | 1 |
| hole_type | string | Specify the hole sets using 2d-array format | "[[0],[1],[2],[3],[4],[5,6]]" |
| hole_type_str | string | Describe the hole type | "1^5_2^1" |
Similarly, instances in the corresponding formats can also be generated by calling hls_to_mace4.py (for Mace4) and hls_to_smt2.py (for Z3).
The generated instances will be saved in the current directory with the filename hls_{order}_{identity}_{hole_type_str} by default.
For convenience, we also provide scripts to generate all instances, which can be executed by running sh gen_mzn.sh, sh gen_mace4.sh or sh gen_smt2.sh.
To download all the instances generated by the above scripts, please visit the following link: [Google Drive].
To generate SAT instances after the POHLS reduction, please uncomment the code in L296 of hls_to_sat.py.
The automatic symmetry breaking tools we used are available at the following links: [Shatter], [BreakID].
Welcome to use this generator to investigate the existence of more HLS instances other than these 39 hole types. If it is helpful to you, please consider citing our paper.