Python code to shuffle a SAT instance in CNF format. Renames the variables, re-orders the clauses, and re-orders the literals in each clause.

shufflecnf.py

from math import copysign
import random
import sys
import os


def shufflecnf(cnffilename, seed, outputfile):
    random.seed(seed)

    numvar, numclauses = None, None
    clauses = []

    with open(cnffilename, "rt") as f:
        for line in f:
            bits = line.split(" ")
            if line.startswith("c "):  # Comments
                continue
            elif line.startswith("p "):
                numvar, numclauses = int(bits[2]), int(bits[3])
            else:  # Clause
                clause = map(int, bits[:-1])  # Exclude the zero
                if clause:
                    clauses.append(clause)

    # Create a mapping of the variable name to some shuffle
    newvarnames = range(1, numvar + 1)
    random.shuffle(newvarnames)
    newvarnames.insert(0, 0)  # Keep 0 as 0

    # Shuffle the order of the clauses
    random.shuffle(clauses)

    outputfile.write("c Shuffled %s with seed %d\n" % (cnffilename, seed))
    outputfile.write("p cnf %d %d\n" % (numvar, numclauses))
    for clause in clauses:
        random.shuffle(clause)  # Shuffle the order of variables in a clause
        # Rename variables while keeping the sign of the literal
        line = [int(copysign(newvarnames[abs(lit)], lit)) for lit in clause]
        outputfile.write(" ".join(map(str, line)))
        outputfile.write(" 0\n")


if __name__ == '__main__':
    if len(sys.argv) not in [3, 4]:
        print >> sys.stderr, \
            "Usage: python %s cnffilename seed [outputfilename]" % sys.argv[0]
        sys.exit(1)

    cnffilename = sys.argv[1]
    seed = int(sys.argv[2])
    if len(sys.argv) == 4:
        outputfilename = sys.argv[3]
        with open(outputfilename, "wt") as f:
            shufflecnf(cnffilename, seed, f)
    else:
        shufflecnf(cnffilename, seed, sys.stdout)