Dataset of Random Reordered Encodings of Parity Problems

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