PROPSAT

PROPSAT is a satisfiability checker for propositional or _Boolean_ formulas.
There are a number of approaches aimed at checking the satisfiability of propositional formulas.
PROPSAT offers the two classic decision procedures based on _Resolution_ or _Tableaux_.

The Resolution procedure is implemented by ``createResolver().run()` (see below). It
features proof extraction (in the case of unsatisfiability) as well as the computation of a satisfying assignment
(in the case of satisfiability).
The Tableaux procedure is implemented by `createTableaux().run()`
(see below). It reports a closed tableaux (in the
case of unsatisfiability) or produces a satisfying assignment (in the case of satisfiability).

Note that PROPSAT cannot, nor was it intended to, compete with state-of-the-art satisfiability checkers.
It is nonetheless reasonably efficient and robust to deal with non-trivial tasks.
As such it could be used for teaching purposes in the shape of web-based tutorials,
for instance. Apart from that PROPSAT demonstrates that _Javascript_ or _Node.js_ can be a suitable approach to tackle AI
scenarios in that it allows us to quickly implement experimental systems or prototypes and share them with a huge
community, for both publication and collaboration purposes.

Quick Run


`run_resolution.js` can be used to execute the Resolution procedure on a given list of CNF files (files
containing a set of clauses in CNF). Run
`bash
$ node run_resolution
`
for usage information.

`run_tableaux.js` can be used to execute the Tableaux procedure on a given list of CNF files. Run
`bash
$ node run_tableaux
`
for usage information.

A selection of CNF files can be found in `samples/sat` (satisfiable sets of clauses) and `samples/unsat`
(unsatisfiable sets of clauses). The samples were partly taken from
SATLIB - Benchmark Problems, and partly generated using
generators provided by plpgen.
Some of these problems pose a challenge to resolution, but not so much to
Tableaux, and vice versa. Note that Tableaux-style ATP usually never runs out of memory (when applied
to propositional problems), whereas for resolution exceeding memory limits is a rather common scenario.
(See, for instance, the _Pigeon Hole_ problems `samples/unsat/hole.cnf`
for number of holes `` equal to 5 or greater.)

Essential Data Structures

$3


An assignment is an object with propositional variable names as properties and
_Boolean_ `false` or `true` as values.
Note that any propositional variable not occurring as a property is effectively assigned `false`.

$3

Some of the functions explained in section _Usage_ accept clauses (i.e., a set of clauses).
Such a set of clauses is an array supplying each clause as an array of literals,
e.g. `[['-A', 'B'], ['A'], ['-B']]`.
A literal (i.e., a propositional variable that may or may not be negated, with negation indicated by a preceding `-`)
can be any string or number other than the string or number `0`.
Thus, `[[-1, 2], [1], [-2]]` is also a valid CNF. Typically clauses are read from a file and are therefore provided through one of the read methods.

$3

There are a number of functions that handle propositional formulas. Initially the formulas are given as strings
and then parsed and that way transformed into an internal representation (a tree).
See function __stringToPropForm__ described below. The syntax is standard infix
notation with propositional variables beginning with `a..z` or `A..Z` or `_`. Additional characters
may also be `0..9`. `T` and `F` are not propositional variables, but constants for _true_ and _false_,
respectively.

The precedence of the (binary) logical operators is as usual, with logical _and_ having highest precedence,
followed by logical _or_, _exclusive or_ (_xor_), _implication_, and finally _equivalence_. The logical negation
operator can be one of the following ASCII characters: `!`, `-`, `~`.
(As usual, negation binds more strongly
than any of the binary operators.) For the binary operators, the following choices exist:

_and_: ``, `&`, `&&`
* _or_: `+`, `|`, `||`
* _xor_: `^`
* _implication_: `->`, `=>`
* _equivalence_: `<->`, `<=>`

__Example__: `!(x1 + x2) <-> !x1 * !x2`

Usage


`js
const propsat = require('propsat');
`

Module `propsat` exports the following functions (listed in alphabetical order):

$3


Checks whether the given assignment satisfies all the given clauses. Returns `true` if all clauses are
satisfied, `false` otherwise.

_See also_: __unsatisfiedClausesCount__

$3

Returns a deep copy of the given propositional formula `pf`. This function does
not accept `pf` as a `string`.
Use __stringToPropForm__ to convert the string into the required internal representation.

$3

Returns a propositional formula `pf` that is the result of performing
Craig Interpolation
on the two input formulas `pf1` and `pf2`. That is, `pf` contains only propositional
variables that occur both in `pf1` and `pf2`, and assuming that `pf1` implies `pf2`
(which is _not_ checked), `pf1` implies `pf` and `pf` implies `pf2`.

$3

Returns the successor of the given assignment without modifying the given assignment.
This function returns `null` if the given assignment is the last of the enumeration.

_See also_: __initialAssignment__, __nextAssignment__

$3

Creates a prover based on Resolution
(for propositional logic). The prover can be used to find a satisfying assignment or a proof
for the unsatisfiability of the given set of clauses, respectively.

The first parameter is mandatory and should provide the set of clauses.
The second parameter is optional, providing options to overwrite default values.

#### Parameter _clauses_
This parameter can be either a string holding clauses separated by a new-line character and
literals separated by a space,
e.g. `'-A B\nA\n-B'`, or a full-fledged DIMACS formatted string with `0`-terminated clauses
(see also __readClausesFromFile__), or an array as described above in section _Essential Data Structures_.

#### Parameter _options_
The options object provides options through properties and their values.
Omitting any of these properties triggers the default behavior.
The following properties are supported:

* `logger`: a function used for logging. The function should accept one (string) argument. For instance,
use `logger: console.log` to log activities to the console. The degree of detail of the logged information
depends on the log level. The default is no logger.

* `logLevel`: the log level that defines the degree of logging details, or in other words the amount
of data passed to the logger. The log level should be an integer in the range 0..4. As usual higher numbers
translate to more data passed to the logger. The default is 0 (no logging at all).

* `memLimit`: the maximal heap used (as returned by `process.memoryUsage().heapUsed`). It can be given
as a number or a string. When given as a string the heap limit may be specified using the units K, M, or G,
representing kilobytes, megabytes, or gigabytes, respectively. For instance, use
`{memLimit:'100M'}` for a 100 megabytes heap limit. Default is 512 megabytes. When the heap usage
exceeds the heap limit the prover stops and enters state `'stopped'`.
Note that checking the limit does incur a notable performance penalty.
Checking the limit can be disabled through a limit of 0.

* `indexing`: a flag (with a value of either `true` or `false`) that indicates whether an
indexing technique should be employed to speed up basic operations of the proof procedure. Note that using
or not using this technique may alter the search by deriving clauses in a slightly different order.
By default indexing is switched on.

#### Return Value
The return value is an object that allows to run, resume, or rerun the prover,
as well as to obtain its current state through the following functions:

* `getState()`: get the state of the prover as a string. The state will be either `'created'`, `'done'`,
or `'stopped'`, indicating a freshly created prover that never ran, a successfully completed run, or
a stopped run, respectively.

* `run(options)`: run or resume a previously stopped run

* `rerun(options)`: start a new run from scratch, i.e. do _not_ resume from where a previous run left off

Both `run` and `rerun` have an optional parameter `options`. If provided it must be an object
that allows to change settings through the following properties (and their values):

* `logger`: see description of options for __createResolver__ above. A previously set logger will be overwritten.

* `logLevel`: see description of options for __createResolver__ above. A previously set level will be overwritten.

* `indexing`: see description of options for __createResolver__ above. A previously set value will be overwritten only when calling `rerun`,
or `run` on a prover that has never been run. In other words this option is ignored when resuming a run.

* `timeout`: the timeout in milliseconds given as a number; default is no timeout.
When the running time exceeds the timeout the prover stops and enters state `'stopped'`.

The return value of `run` as well as `rerun` is an object with the following properties:

* `state`: the state of the prover. The state will be either `'done'` or `'stopped'`.

* `message`: a message that indicates the reason for the current state. For state `'done'` the
message will be either `'unsatisfiable'` or `'satisfiable'`. For state `'stopped'` the message will
be either `'timeout'` or `'out of memory'`.

* `info`: additional information that may not always be available. Currently only in the case of
running out of memory this property contains information (a string) providing further details.

* `hrtimeElapsed`: the time elapsed in `process.hrtime` format

* `timeElapsed`: the time elapsed as a human-readable string

* `statistics`: an object providing statistical information on the run through its properties and values

* `assignment`: an assignment satisfying the set of clauses if such an assignment was found. Otherwise
this property is undefined.

* `emptyClause`: the empty clause if the set of clauses could be proved to be unsatisfiable. Otherwise this
property is undefined.

The value of `emptyClause` (if it is defined) is an object that offers the following functions
regarding the proof found:

* `extractProof()`: the proof in human-readable form. It is returned as an array of strings, each
such string representing one step in the proof.

* `proofDepth()`: the depth of the proof, or in other words the maximal distance between the empty
clause and axioms (viewing the proof as a directed graph)

* `proofLength()`: the length of the proof, or in other words the number of axioms and clauses derived
by means of resolution involved in the derivation of the empty clause

$3

Creates a prover based on Analytic Tableaux
(for propositional logic). The prover can be used to find a satisfying assignment or a proof
for the unsatisfiability of the given set of clauses, respectively.

The first parameter is mandatory and should provide the set of clauses.
The second parameter is optional, providing options to overwrite default values.

#### Parameter __clauses__
This parameter can be either a string holding clauses separated by a new-line character and
literals separated by a space,
e.g. `'-A B\nA\n-B'`, or a full-fledged DIMACS formatted string with `0`-terminated clauses
(see also __readClausesFromFile__), or an array as described above in section _Essential Data Structures_.

#### Parameter __options__
The options object provides options through properties and their values.
Omitting any of these properties triggers the default behavior.
Currently, the following properties are supported:

* `logger`: a function used for logging. The function should accept one (string) argument. For instance,
use `logger: console.log` to log activities to the console. The degree of detail of the logged information
depends on the log level. The default is no logger.

* `logLevel`: the log level that defines the degree of logging details, or in other words the amount
of data passed to the logger. The log level should be an integer in the range 0..3. As usual higher numbers
translate to more data passed to the logger. The default is 0 (no logging at all).

#### Return Value
The return value is an object that allows to run, resume, or rerun the prover,
as well as to obtain its current state through the following functions:

* `getState()`: get the state of the prover as a string. The state will be either `'created'`, `'done'`,
or `'stopped'`, indicating a freshly created prover that never ran, a successfully completed run, or
a stopped run, respectively.

* `run(options)`: run or resume a previously stopped run

* `rerun(options)`: start a new run from scratch, i.e. do _not_ resume from where a previous run left off

Both `run` and `rerun` have an optional parameter `options`. If provided it must be an object
that allows to change default settings through the following properties (and their values):

* `logger`: see description of options for __createTableaux__ above. A previously set logger will be overwritten.

* `logLevel`: see description of options for __createTableaux__ above. A previously set level will be overwritten.

* `timeout`: the timeout in milliseconds; default is no timeout. When the running time exceeds the timeout
the prover stops and enters state `'stopped'`.

The return value of `run` as well as `rerun` is an object with the following properties:

* `state`: the state of the prover. The state will be either `'done'` or `'stopped'`.

* `message`: a message that indicates the reason for the current state. For state `'done'` the
message will be either `'unsatisfiable'` or `'satisfiable'`. For state `'stopped'` the message will
be `'timeout'`.

* `info`: additional information that may not always be available. Currently only in the case of
the empty clause being a member of the initial set of clauses this property contains information
(a string) to that effect.

* `hrtimeElapsed`: the time elapsed in `process.hrtime` format

* `timeElapsed`: the time elapsed as a human-readable string

* `statistics`: an object providing statistical information on the run through its properties and values

* `assignment`: an assignment satisfying the set of clauses if such an assignment was found. Otherwise
this property is undefined.

$3


Evaluates the given propositional formula `pf` for the given assignment. Returns
`true` if the assignment satisfies the formula (i.e., the formula evaluates to
`true` using the given assignment), `false` otherwise. This function does not
accept `pf` as a `string`.
Use __stringToPropForm__ to convert the string into the required internal representation.

_See also_: __initialAssignment__, __nextAssignment__, __createNextAssignment__

$3

Checks whether the given goal follows from the given axioms. This is a convenience function that
creates the conjunction of the axioms and the negated goal and checks inconsistency of the resulting
conjunction using `isPropFormInconsistent`. (See `isPropFormInconsistent` for details on
parameter `useTableaux`.)

The goal must be a propositional formula, and the axioms must either be a single propositional formula
or an array of such formulas.

$3

Returns an initial assignment for the given propositional formula or clauses that assigns `false` to
all variables occurring in `pf`. This function does not accept `pf` as a `string`.
Use __stringToPropForm__ to convert the string into the required internal representation.
This initial assignment is a starting point for enumerating all possible assignments using
`nextAssignment` or `createNextAssignment`.

$3

Checks whether a given propositional formula `pf` is inconsistent by returning `true` for
inconsistency (i.e., unsatisfiablility) and `false` otherwise (i.e., satisfiability).

The Resolution procedure is employed to
determine inconsistency (i.e., unsatisfiability) unless parameter `useTableaux` is provided and evaluates
to `true`. In that latter case the Tableaux method is employed.

$3


Checks whether a given propositional formula `pf` is a tautology. This is a convenience function that
negates the given formula and checks inconsistency using function `isPropFormInconsistent`. It
returns `true` if the formula is a tautology, `false` otherwise.
(See `isPropFormInconsistent` for details on parameter `useTableaux`.)

$3

Modifies the given assignment to become its successor.
This function returns `false` if the given assignment is the last of the enumeration.
(In that case the assignment becomes the initial assignment again.) Otherwise the function returns `true`.

_See also_: __initialAssignment__, __createNextAssignment__

$3

Converts the given propositional formula into a string using prefix notation. The logical operators
_equivalence_, _implication_, _exclusive or_, _or_, _and_, and _not_ are represented by `equiv`,
`impl`, `xor`, `or`, `and`, and `not`, respectively.
This function does not accept `pf` as a `string`.
Use __stringToPropForm__ to convert the string into the required internal representation.

_See also_: __propFormToString__

$3

Checks whether the given propositional formulas are syntactically equal (modulo renaming variables).
It returns `true` if that is the case and `false` otherwise.

__Example__: `x -> (y -> x)` and `A -> (B -> A)` are syntactically equal (module renaming variables),
but `x -> y` and `!x | y` are not (although both formulas are logically equivalent).

$3


Converts the given propositional formula `pf` into a set of clauses.
The return value is that set of clauses.

$3

Converts the given propositional formula `pf` into a formula in CNF.
The return value is that formula in CNF.

$3

Converts the given propositional formula into a string using infix notation.
This function does not accept `pf` as a `string`.
Use __stringToPropForm__ to convert the string into the required internal representation.
An optional flag `opPadding` indicates whether binary operator symbols should be preceded and followed by
a space character (if the value of this parameter is `true`) or not (for any other value). The third
(optional) parameter defines the style to be used. If no style is specified the default style is used, which
means that the logical operators
_equivalence_, _implication_, _exclusive or_, _or_, _and_, and _not_ are represented by `<->`,
`->`, `^`, `+`, `*`, and `-`, respectively. The style can be changed as shown in the
following examples:

#### _Examples_:
We assume that
`js
let pf = propsat.stringToPropForm('!((A->B)&(B->A)) | (A<->B)');
`
With
`js
propsat.propFormToString(pf);
`
we obtain
`js
'-((A->B)*(B->A))+(A<->B)'
`
With
`js
propsat.propFormToString(pf, true);
`
we obtain
`js
'-((A -> B) * (B -> A)) + (A <-> B)'
`
With
`js
propsat.propFormToString(pf, false, 'asciiDAE');
`
we obtain
`js
'!((A=>B)*(B=>A))+(A<=>B)'
`
The general structure of the string defining an ASCII style is `ascii{S|D}{A|L}{E|T|M}`
where

* `S`, `D`: single or double line equivalence or implication

* `A`, `L`: arithmetic or logic operators for _and_ and _or_

* `E`, `T`, `M`: _not_ represented by exclamation mark, tilde, or minus sign

Thus, with
`js
propsat.propFormToString(pf, true, 'asciiSLT');
`
we obtain
`js
'~((A -> B) & (B -> A)) | (A <-> B)'
`
On top of the twelve ASCII variants there are two unicode styles `'unicode1'` and `'unicode2'`
that represent logical operators with unicode symbols.

_See also_: __propFormPrefixToString__

$3


Reads clauses from a file with name `fileName` asynchronously. The accepted file format is the CNF format
proposed by DIMACS and used by
SATLib
(see folders `samples/sat` or `samples/unsat` for examples).
The outcome of reading the file is passed to
the callback function `cb`. The callback function should as usual have two arguments, the first being an error
object and the second one being the set of clauses read. The set of clauses is not supplied in case of an error. If the
clauses could be read successfully, the error argument is `null`.

The set of clauses is an array containing the clauses as its elements (see also
_Essential Data Structures_ above). Furthermore, the array may have the
property `comments`. This property is an array of strings (comments), one element for each line starting
with `c` in the given file.

Note that this function does not strictly follow the DIMACS format in that it accepts literals that do not
consist of digits only. Also, the problem specification line `p cnf n m`, where _n_ is the number
of variables and _m_ is the number of clauses, is not required. However, if it is given, an `Error` is thrown
if an inconsistency is detected. Furthermore, clauses
do not have to be `0`-terminated. If none of the lines containing literals have any occurrence of the
termination indicator `0`, clauses are assumed to be terminated by the new-line character.

$3


This is the synchronous version of `readClausesFromFile`. It returns the set of clauses.

$3

Returns a simplified version of the given propositional formula `pf`.
Simplification consists in double negation elimination as well as
eliminating occurrences of `T` and `F`. This function does not accept `pf`
as a `string`. Use __stringToPropForm__ to convert the string into the required internal representation.

$3

Converts the given string representing a propositional formula into an object representing that same formula. Some functions require the object representation, while others also
accept the string representation (tacitly converting the string into the object
representation with this very function). For performance reasons it may make
sense to explicitly convert a string into its object representation, in particular if
the same formula is passed to a function repeatedly.

$3

Returns the number of clauses among the given clauses that are not satisfied by the given assignment.

_See also_: __clausesSatisfiedBy__

$3

Writes the given clauses to file `fileName` asynchronously, thereby following the
DIMACS
format (see also __readClausesFromFile__).
The callback function `cb` should follow the same principles as function `writeFile` of
the standard module `fs`.

`clauses` can be a string, in which case it is saved as is. (In this case whoever or whatever
created the string is responsible for the format. That is, the proper or near DIMACS format is not
guaranteed when saving a set of clauses this way.)

Otherwise `clauses` should be an array adhering to the structure
explained above (see _Essential Data Structures_).
In the latter case if `clauses.comments` exists and is an array its elements are written to the
file as comments (i.e., preceded by `c` and a space) before any of the clauses are written.
Furthermore the problem specification `p cnf n m` is written after any comments and before
the clauses with _n_ and _m_ representing the number of variables and clauses, respectively.

$3


This is the synchronous version of `writeClausesToFile``.