Executables for min-cost sat utilities
-
apply_permutation - applies a given permutation to the
rows and columns of an instance in cnf format; used primarily by the
improveOrder script.
Usage: apply_permutation C/R input permutation output
C means column permutation, R means row.
input and output are files in cnf(x) format.
permutation contains a list of numbers [1,n],
where n is the number of rows/columns.
-
morph - applies random permutations to rows and columns
of an instance in cnf or cnfx format; originally used for sat
instances as well, where it was appropriate to randomly negate
variables -- hence the many options.
Usage: morph flags input
seed(3 ints) output
where flags is a string consisting of the letters
C, L, R, and X in
some order,
input and output are paths to the original
(reference) and transformed files, respectively,
and seed consists of three unsigned short integers.
The letter codes denote the following transformations:
C - apply a random permutation to the columns
(variables)
L - apply a random permutation independently
(locally) to each row (clause), i.e. permute literals in each clause.
R - apply a random permutation to the rows (clauses)
X - complement a random subset of the variables
To preserve original comments, add the letter o.
To get a general comment with the seed information, add the letter
s.
If trace information about the morphism is desired in the output
file, add the letter t (lower case) after the
transformation to be traced. For example CtRX permutes
both rows and columns, and complements variables, but only the
column permutation is documented in a header comment.
-
new_seed - creates a new seed using the IEEE-48 standard;
this is used by some of the scripts to jump around in the pseudorandom
sequence, thus making it unlikely that two successive constructions have
the same outcome, but still maintaining repeatability.
Usage: new_seed iterations < input > output
where both input and output are a single string of 3 comma-separated
16-bit unsigned integers (unsigned short); iterations is the number of
random numbers in the IEEE-48 sequence to skip
-
verify - verifies the solution to an instance in cnf format
(only verifies feasibility, not weight).
Usage: verify input solution
where input is the path to a cnf input file and
solution is the path to a file containing a string of 0's,
1's, and 2's (the bit vector; 2's mean don't care), leftmost bit first;
for convenience, the file may contain arbitrary white space between
successive bits.
Prints an error message and returns an exit code of -1 if the given
solution does not satisfy the formula, is silent with a 0 exit
otherwise.
Matthias F. (Matt) Stallmann,
http://people.engr.ncsu.edu/mfms
(
Matt_Stallmann AT ncsu.edu)
Last modified: Wed Jun 6 11:38:19 2007