Dataset of Random Reordered Encodings of Parity Problems

<p>Dataset created and used for the paper:</p> <p><em>Hardness of Random Reordered Encodings of Parity for Resolution and CDCL</em>,&nbsp;Leroy Chew, Alexis de Colnet, Friedrich Slivovsky and Stefan Szeider, AAAI 2023</p> <p>report.rmd is an R Markdown file that can be opened in RStudio and used to generate the figures in the submission</p> <p>_stats file: lists the permutations used<br>.cnf file: DIMACS representation of unsat formulas<br>.gr : DIMACS representation of the Tseitin graph<br>.edges: alternative representation of the Tseitin graph<br>_half: DIMACS representation of the Tseitin graph for G*</p> <p>n: number of input variables<br>p: probability of selection for each variable<br>s: random seed used<br>m: mode number used<br>&nbsp; &nbsp; 0 : uniformly random<br>&nbsp; &nbsp; 1: Mallows(n,q), q= (1/n)^(1/(k*k))<br>&nbsp; &nbsp; 3: performs k number of random adjacent swaps to make the permutation<br>&nbsp; &nbsp; 4: performs 10000000 potential random adjacent swaps but forbids the distance being &gt;k<br>&nbsp; &nbsp; 5: uniformly but rerolls until the maximum permutation distance is k<br>&nbsp; &nbsp; 6: 3 parity constraints<br>k: integer parameter for mode</p>