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 stateoftheart satisfiability checkers. It is nonetheless reasonably efficient and robust to deal with nontrivial tasks. As such it could be used for teaching purposes in the shape of webbased 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 Tableauxstyle 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 newline character and
literals separated by a space,
e.g. 'A B\nA\nB'
, or a fullfledged 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, uselogger: 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 byprocess.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 eithertrue
orfalse
) 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 callingrerun
, orrun
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 inprocess.hrtime
format 
timeElapsed
: the time elapsed as a humanreadable 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 humanreadable 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 newline character and
literals separated by a space,
e.g. 'A B\nA\nB'
, or a fullfledged 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, uselogger: 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 inprocess.hrtime
format 
timeElapsed
: the time elapsed as a humanreadable 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{SD}{AL}{ETM}
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 newline 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
.