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

$ 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

$ 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<n>.cnf for number of holes <n> equal to 5 or greater.)

Essential Data Structures

Assignment

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.

Clauses

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.

Formula

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

const propsat = require('propsat');

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

clausesSatisfiedBy (clauses, assignment)

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

See also: unsatisfiedClausesCount

copyPropForm (pf)

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.

craigInterpolation (pf1, pf2)

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.

createNextAssignment (assignment)

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

createResolver (clauses, options)

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

createTableaux (clauses, options)

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.

evalPropForm (pf, assignment)

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

followsFromAxioms (axioms, goal, useTableaux)

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.

initialAssignment (pf)

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.

isPropFormInconsistent (pf, useTableaux)

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.

isPropFormTautology (pf, useTableaux)

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

nextAssignment (assignment)

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

propFormPrefixToString (pf)

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

propFormsEqual (pf1, pf2)

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

propFormToClauses (pf)

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

propFormToCnf (pf)

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

propFormToString (pf, opPadding, style)

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

let pf = propsat.stringToPropForm('!((A->B)&(B->A)) | (A<->B)');

With

propsat.propFormToString(pf);

we obtain

'-((A->B)*(B->A))+(A<->B)'

With

propsat.propFormToString(pf, true);

we obtain

'-((A -> B) * (B -> A)) + (A <-> B)'

With

propsat.propFormToString(pf, false, 'asciiDAE');

we obtain

'!((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

propsat.propFormToString(pf, true, 'asciiSLT');

we obtain

'~((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

readClausesFromFile (fileName, cb)

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.

readClausesFromFileSync (fileName)

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

simplifyPropForm (pf)

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.

stringToPropForm (pfAsString)

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.

unsatisfiedClausesCount (clauses, assignment)

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

See also: clausesSatisfiedBy

writeClausesToFile (clauses, fileName, cb)

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.

writeClausesToFileSync (clauses, fileName)

This is the synchronous version of writeClausesToFile.