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