PLPGEN

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

Installation

``bash
$ npm install plpgen
`

Usage

`js
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.

$3

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):

`js
[
'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):

`js
{
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.

$3

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__

$3

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.

$3

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_).

$3

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__

$3

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.

$3

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.

$3

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_):
`js
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:
`js
-SOLUTION-
++X+
X+++
+++X
+X++
`




$3


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:
`js
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');
``