cnfformula.transformations.shuffle module

Shuffle(cnf, variable_permutation=None, clause_permutation=None, polarity_flip=None)

Reshuffle the given cnf. Returns a formula logically equivalent to the input with the following transformations applied in order:

1. Polarity flips. polarity_flip is a {-1,1}^n vector. If the i-th entry is -1, all the literals with the i-th variable change its sign.

2. Variable permutations. variable_permutation is a permutation of [vars(cnf)]. All the literals with the old i-th variable are replaced with the new i-th variable.

3. Clause permutations. clause_permutation is a permutation of [0..m-1]. The resulting clauses are reordered according to the permutation.

class ShuffleCmd

Shuffle

Methods

setup_command_line
transform_cnf

description = 'Permute variables, clauses and polarity of literals at random'

name = 'shuffle'

static setup_command_line(parser)

static transform_cnf(F, args)