PLPGEN

PLPGEN is a utility for generating propositional problems in the format proposed by DIMACS and used by SATLib.

Installation

$ npm install plpgen

Usage

var plpgen = require('plpgen');

Create Clause Sets

Module plpgen exports the following functions (listed in alphabetical order), all of which either return a set of clauses as a string that conforms to the DIMACS conventions, or optionally write such a string to a file (specified through the optional parameter fileName). In the latter case the return value is undefined. Note that an existing file cannot be overwritten. An error is thrown if the file denoted by fileName exists.

killerSudokuToPL (sudoku, constraints, fileName)

Transforms a Killer Sudoku problem into a set of propositional clauses with the property that the set of clauses is satisfiable if and only if the given Killer Sudoku problem has a solution that complies with the classic Sudoku rules and the given constraints specific to a Killer Sudoku. From an assignment satisfying the set of clauses the solved or completed Sudoku can be created with the help of sudokuFromAssignment.

The Sudoku problem is specified through parameter sudoku. Its value can be either a string or an array. If it is an array, the elements of the array are the rows. The rows can be strings or arrays of characters. If sudoku is a string, the rows may be separated via newline characters, but do not have to be. Without newline characters the first nine characters represent the first row and so on.

Instead of colors or other graphical means, the cages of a Killer Sudoku are denoted by lower and upper case letters from the Latin alphabet, i.e. 'a' through 'z' and 'A' through 'Z', a total of 52 letters, which is sufficient since a cage comprises at least two cells. Here is an example for parameter sudoku given as an array of strings (cp. original):

[
  'aabbbcdef',
  'gghhccdef',
  'ggiicjkkf',
  'lmminjkof',
  'lqqrnjoop',
  'vqsrntuup',
  'vssrwttzz',
  'vxywwAAzz',
  'vxywBBBCC'
]

The sums of the cages are specified through parameter constraints, an object with cage letters as properties and the respective sums as values. For the example the constraints are as follows (cp. again original):

{
  a:3, b:15, c:22, d:4, e:16, f:15,
  g:25, h:17, i:9, j:8, k:20, l:6,
  m:14, n:17, o:17, p:12, q:13,
  r:20, s:6, t:20, u:6, v:27, w:10,
  x:8, y:16, z:14, A:15, B:13, C:17
}

A Killer Sudoku problem is transformed into a set of 10287 + x clauses (each clause drawing its literals from a pool of 729 propositional variables), where x depends on the number of cages and their sums, and in particular on the possible combinations of distinct numbers between 1 and 9 that add up to the respective sums. As an estimate, expect x to be between 1000 and 2000 clauses. Unlike for classic Sudoku these additional clauses are not unit clauses. As a result the satisfiability problems produced from Killer Sudoku are a lot harder than those produced from classic Sudoku.

nQueens (n, fileName)

Creates an instance of the n-Queens Problem, a theoretical chess problem that poses the question whether n queens can be placed on an n by n chess board so that no queen threatens any other queen. The resulting set of clauses is satisfiable for all n except n = 2 and n = 3. The number of propositional variables is the square of n, and the truth value of variable i represents the presence (true) or absence (false) of a queen in row 1 + (i - 1) div n and column 1 + (i - 1) mod n. The number of clauses is n * (5 * n * n - 6 * n + 4) / 3.

See also: nQueensFromAssignment

pigeonHoles (holes, fileName)

Creates an instance of the Pigeon Hole Problem (i.e., the impossibility to fit n + 1 pigeons into n holes when each hole can hold at most one pigeon). The number of holes is specified through parameter holes, which must be an integer greater than or equal to 1. The resulting set of clauses is guaranteed to be unsatisfiable. It consists of (n * n / 2 + 1) * (n + 1) clauses, each clause drawing its literals from n * (n + 1) variables.

rndClause (maxVar, minLits, maxLits)

Creates a random clause. The number of propositional variables from which to draw is specified through maxVar. The number of literals ranges between minLits and maxLits. Parameter maxLits is optional. If omitted or less than minLits the created clause will have minLits literals. The probabilities for negative or positive occurrence of a variable in a clause are the same (0.5).

rndClauseSet (size, maxVar, minLits, maxLits, fileName)

Creates a set of random clauses using rndClause. The number of clauses is specified through size, the number of propositional variables through maxVar. The optional parameters minLits and maxLits specify the minimal and maximal number of literals per clause, respectively. If omitted or invalid minLits will be 3. maxLits will be equal to minLits if omitted or invalid or less than minLits.

Note that the set of random clauses created with this function may contain duplicates, but guarantees to have exactly the given size.

See also: rndClauseSetNoDuplicates

rndClauseSetNoDuplicates (size, maxVar, minLits, maxLits, fileName)

Creates a set of random clauses like rndClauseSet, but guarantees that no clause occurs more than once. The final set of clauses will contain less clauses than desired if (and only if) the number of distinct clauses is less than the given size.

Note that neither function for creating random sets of clauses guarantees that the set of clauses is free of redundancies in terms of one clause subsuming another. (This function does guarantee that only if minLits is equal to maxLits.) Furthermore, both functions may produce satisfiable or unsatisfiable sets of clauses.

sudokuToPL (sudoku, fileName)

Transforms a classic Sudoku problem into a set of propositional clauses with the property that the set of clauses is satisfiable if and only if the given Sudoku problem has a solution that complies with the Sudoku rules. From an assignment satisfying the set of clauses the solved or completed Sudoku can be created with the help of sudokuFromAssignment.

The Sudoku problem is specified through parameter sudoku. Its value can be either a string or an array. If it is an array, the elements of the array are the rows. These can again be either strings or arrays of characters. If sudoku is a string, the rows may be separated via newline characters, but do not have to be. Without newline characters the first nine characters represent the first row and so on. The characters (or numbers) '1' through '9' obviously represent cells occupied with the respective number. All other characters represent an empty cell and are replaced with '*'.

A Sudoku problem is transformed into a set of 10287 + n clauses, where n is the number of non-empty cells, each clause drawing its literals from a pool of 729 propositional variables. Not surprisingly (given the backtracking nature of Sudoku problems) Tableaux-based methods are the weapon of choice for tackling such a set of clauses.

Convenience Functions

Module plpgen also exports the following convenience functions to interpret or visualize results (assignments) obtained for certain clause sets.

nQueensFromAssignment (assignment)

Transforms the given assignment (i.e., associations of propositional variables with the value true or false) into a chess board represented by an array of strings. Each string is a row and consists of characters '+' (empty square) and 'X' (square occupied by a queen).

The assignment must be an object with properties named 1 through n * n, where n is the number of queens as well as the dimensions of the chess board (see nQueens).

Example:

Assuming that module propsat has been installed, the following code can be used to solve the n-Queens problem (in this case for n=4):

var assignment = require('propsat').createTableaux(plpgen.nQueens(4)).run().assignment;
if (assignment)
  console.log(plpgen.nQueensFromAssignment(assignment).join('\n'));
else
  console.log('No solution');

The output of this particular run would be:

-SOLUTION-
++X+
X+++
+++X
+X++

sudokuFromAssignment (assignment)

Transforms the given assignment (i.e., associations of propositional variables with the value true or false) into a completed Sudoku. The return value is an array of strings. Each string represents a row and hence has length 9. (The array naturally also has length 9.) The assignment must be an object with properties named 1 through 729 (i.e., the propositional variables used when transforming a Sudoku into a set of clauses in DIMACS format; see sudokuToPL or killerSudokuToPL). The values should be either true or false, although anything that evaluates to the desired Boolean value is accepted.

Note that this method does not check compliance with Sudoku rules other than that each cell is assigned one number and one number only. However, if the given assignment is legit in that it satisfies the clauses produced by sudokuToPL or killerSudokuToPL the completed Sudoku will comply with all Sudoku rules.

Typically you would present a system capable of finding an assignment for a given set of propositional clauses with the clauses produced by sudokuToPL or killerSudokuToPL, and then use sudokuFromAssignment to create the completed or solved Sudoku.

Example:

Assuming that module propsat has been installed and that variable sudoku holds a classic Sudoku problem as described in connection with sudokuToPL, the following code can be used to solve classic Sudoku problems:

var assignment = require('propsat').createTableaux(plpgen.sudokuToPL(sudoku)).run().assignment;
if (assignment)
{
  console.log('-SOLUTION-');
  console.log(plpgen.sudokuFromAssignment(assignment).join('\n'));
}
else
  console.log('INVALID');