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.