propsat

Propositional Satisfiability Checker

PROPSAT

PROPSAT is a satisfiability checker for propositional or Boolean formulas. There are a number of approaches to checking the satisfiability of propositional formulas. PROPSAT currently offers decision procedures based on Resolution or Tableaux, as well as a procedure based on the Genetic Algorithm (GA) and a WalkSat approach for tackling satisfiable problems.

The Resolution procedure is implemented by runResolution (see below) and 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 runTableaux (see below) and it reports a closed tableaux (in the case of unsatisfiability) or produces a satisfying assignment (in the case of satisfiability). The GA-based and WalkSat procedures are implemented by runGaSat and runWalkSat, respectively.

Note that PROPSAT cannot, nor was it intended to, compete with state-of-the-art satisfiability checkers (written in C or C++). 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.

$ npm install propsat

tests/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 tests/resolution

for usage information.

tests/tableaux.js can be used to execute the Tableaux procedure on a given list of CNF files. Run

$ node tests/tableaux

for usage information.

tests/hybrid.js can be used to execute a hybrid procedure (interleaving Resolution and Tableaux) on a given list of CNF files. Run

$ node tests/hybrid

for usage information.

tests/gasat.js can be used to execute the GA-based procedure on a given list of CNF files. Run

$ node tests/gasat

for usage information.

tests/walksat.js can be used to execute the WalkSat procedure on a given list of CNF files. Run

$ node tests/walksat

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

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

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.

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

var propsat = require('propsat');

Module propsat exports the following functions:

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

See also: unsatisfiedClausesCount

Returns a deep copy of the given propositional formula pf. This function does not accept pf as a string.

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

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.

See also: initialAssignment, nextAssignment, createNextAssignment

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. This initial assignment is a starting point for enumerating all possible assignments using nextAssignment or createNextAssignment.

Checks whether a given propositional formula pf is inconsistent. 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.

The callback function cb should accept at least two arguments, the first one as usual being an error object. If an error occurs, the first argument is the only argument supplied. If no error occurs the first argument is null and the second argument is a Boolean value, where true indicates inconsistency or unsatisfiability, and false indicates satisfiability. In the case of satisfiability a satisfying assignment is supplied as the third argument.

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.

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

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.

See also: propFormToString

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

Converts the given propositional formula pf into a set of clauses. This function is asynchronous and provides the set of clauses via callback cb. The callback should accept two arguments, the first one being an error object and the second one being the clauses. The second parameter is supplied if and only if there is no error, in which case the error object is null.

This is the synchronous version of propFormToClauses that returns the set of clauses.

Converts the given propositional formula pf into a formula in CNF. This function is asynchronous and provides the CNF formula via callback cb. The callback should accept two arguments, the first one being an error object and the second one being the CNF formula. The second parameter is supplied if and only if there is no error, in which case the error object is null.

This is the synchronous version of propFormToCnf that returns the CNF formula.

Converts the given propositional formula into a string using infix notation. This function does not accept pf as a string. 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:

We assume that

var 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

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.

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

Runs a GA-based procedure to find a satisfying assignment for the given set of clauses. Except for the first parameter all parameters are optional. However, the order of the parameters is crucial. That is, no attempt is made to shift parameter positions based on possibly heuristic criteria. So if you omit one or more parameters preceding a parameter you want to supply, supply the omitted parameters as null.

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.

Function runGaSat is asynchronous and returns immediately. The result or an error is reported as usual through a callback function that should have two parameters, namely an error object and a result object. In case of an error or failure, the first parameter is the error object and the second parameter is omitted. Otherwise the first parameter is null and the second parameter holds the result. The result is an object conforming to the following conventions:

  • Property state is always defined. Its value is a string that is equal to one of the following string literals:

    • 'aborted': The GA procedure terminated without finding a satisfying assignment.

    • 'stopped': The GA procedure was stopped. (See section on return value for details on how to stop a running GA procedure.)

    • 'done': The GA procedure terminated successfully, meaning a satisfying assignment for the given set of clauses was found. In this case property assignment holds the assignment found (see below).

  • Property statistics is always defined. Its value is an object that holds statistical data summarizing the search conducted by the GA procedure through the following properties:

    • generations: the total number of generations processed

    • individuals: the total number of individuals processed

    • indiMutations: the number of individuals that had at least one bit mutated (flipped)

    • bitMutations: the total number of bits (across all individuals) that were mutated (flipped)

    • restarts: the number of restarts

    • convDetected: the number of runs terminated on account of premature convergence

  • Property time is always defined. Its value is a human-readable string representing the (wall clock) time elapsed. Use the monitor (see Return Value below) for process.hrtime-style time measurement.

  • Property assignment is available if the GA procedure found an assignment. Its value is that very assignment.

An object that allows the caller to obtain logging information during the execution of the GA procedure. The logger object should have a property level, an integer number ranging from 0 to 7, that controls the verbosity of logging or the amount of data passed to the second property log, a function that should have one parameter of type string. As usual, a higher level increases the amount of logging. A simple logging scenario is to log to the console through the logger {level: 2, log: console.log}, for instance. Note that starting with log level 4 additional time-consuming computations are carried out to supply the required information which is not inherent to nor required by the GA as such.

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:

  • popSize: the size of the population; default is 100

  • maxGen: the maximal number of generations (for each restart); default is 50

  • crossoverPoints: the number of crossover points; recognizes 1 and 2 for one-point and two-point crossover, respectively; any other value (including no value) results in n-point crossover which also is the default

  • mutationRate: the mutation rate r given as a probability ranging from 0.0 to 1.0 with 0.0 being the default; note that r is used in such a way that for any individual the probability of 0 ≤ n < m mutations is rn(1-r), and the probability of m mutations is rm, where m is the number of propositional variables and hence the number of bits of an individual.

  • restarts: the maximal number of restarts (literal restarts, i.e. not including the first start); default is 0

  • eliteFrac: the fraction of the population that can produce offspring when using elite selection; must be a number between 0.0 and 1.0; default is 0.3

  • retainElite: a flag that when true indicates that the elite should be retained (i.e., become a part of the successor generation, thus reducing the number of offspring that will be produced); default is false

  • useFitPropSel: a flag that when true instructs the GA procedure to use fitness-proportionate selection instead of elite selection (elite selection being the default); when using fitness-proportionate selection all parameters related to elite selection are meaningless and are therefore ignored

  • convCheck: the index of the generation at which checking premature convergence should begin; convergence is never checked unless the index is greater than 0; default is 0. Note that convergence is interpreted as all individuals (i.e., all assignments) being identical, or in other words as genetic diversity being completely gone.

A monitor object is returned that can be used to monitor the progress of the GA procedure, or to stop it. To this end the object returned has the following properties that are functions:

  • stop(): stops the GA procedure

  • getState(): returns the current state of the GA procedure (a string)

  • getElapsedHrtime(): returns the time elapsed (in process.hrtime format) since the start of the GA procedure if it is still running; the return value is undefined if the procedure has not yet been or never was started (due to erroneous or invalid input, for instance); otherwise, if the procedure terminated successfully, returns the time it took until termination.

  • getStatistic(name): returns the value of the statistic specified by its name (a string); a valid name is any of the property names listed as statistical data in the result object passed to the callback (cp. statistics above)

Executes an interleaving resolution and tableaux procedure. That is, the main loops of resolution and tableaux that do not block by splitting iterations using global.setImmediate (or process.nextTick for older Nodejs versions) call the respective other procedure to give it a few iterations. That way, problems that can be solved by either one of the two procedures rather quickly (but pose a serious problem to the other) can be solved by the hybrid almost as quickly.

For details on the parameters and the return value of runHybrid (a monitor object) see runResolution and runTableaux. The options that may be supplied to the hybrid is the union of the resolution and tableaux options. The result reported via callback is either the result of the resolution or the tableaux procedure depending on which one of them terminated first.

Executes the Resolution procedure on the given set of clauses. Except for the first parameter all parameters are optional. However, the order of the parameters is crucial. That is, no attempt is made to shift parameter positions based on possibly heuristic criteria. So if you omit one or more parameters preceding a parameter you want to supply, supply the omitted parameters as null.

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.

Function runResolution is asynchronous and returns immediately. The result or an error is reported as usual through a callback function that should have two parameters, namely an error object and a result object. In case of an error or failure, the first parameter is the error object and the second parameter is omitted. Otherwise the first parameter is null and the second parameter holds the result. The result is an object conforming to the following conventions:

  • Property state is always defined. Its value is a string that is equal to one of the following string literals:

    • 'aborted': The Resolution procedure was aborted due to insufficient or inappropriate input. (Typically, this state occurs when the initial set of clauses is empty.) Besides property state a second property message is defined in this case. Its value is a detail message (i.e., a string) providing background information.

    • 'stopped': The Resolution procedure was stopped. (See section on return value for details on how to stop a running Resolution procedure.) Besides property state a second property message is defined in this case. Its value is a detail message (i.e., a string) providing additional information.

    • 'done': The Resolution procedure terminated successfully, meaning a proof of unsatisfiability of, or a satisfying assignment for the given set of clauses was found. In this case further properties of the result object contain the relevant data and information. These are explained in what follows.

  • If a proof of inconsistency or unsatisfiability was found the following properties are defined in addition to property state:

    • emptyClause: the empty clause (evidence of unsatisfiability), an object that has three properties that are of particular interest, each of which is a parameterless function:

      • proofLength(): returns the length of the proof

      • proofDepth(): returns the depth of the proof (i.e., the depth of the empty clause)

      • extractProof(): returns an array of strings representing the proof (of the empty clause), each string in the array detailing one step in the proof in a human-readable format

    • resTime: the time it took to find the empty clause (a string including a suitable time unit intended for human eyes); if you are interested in process.hrtime-style time measurement use the monitor (see Return Value).

    • statistics: statistical data regarding the search conducted by the Resolution procedure

  • If a satisfying assignment was found the following properties are defined in addition to property state:

    • assignment: an assignment (one of possibly many more) that satisfies the given set of clauses

    • resTime: the time it took to ascertain satisfiability (a string including a suitable time unit intended for human eyes), not including the time it took to compute a satisfying assignment from the remaining clauses; if you are interested in process.hrtime-style time measurement use the monitor (see Return Value).

    • fndTime: the time it took to compute an assignment (after ascertaining satisfiability through failure to find a proof of unsatisfiability)

    • statistics: statistical data regarding the search conducted by the Resolution procedure

An object that allows the caller to obtain logging information during the execution of the Resolution procedure. The logger object should have a property level, an integer number ranging from 0 to 3, that controls the verbosity of logging or the amount of data passed on to the second property log, a function that should have one parameter of type string. As usual, a higher level increases the amount of logging. A simple logging scenario is to log to the console through the logger {level: 2, log: console.log}, for instance.

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:

  • indexing: a flag indicating whether indexing techniques should be employed (default: no indexing); due to an overhead inherent to indexing techniques problems solved rather quickly may not benefit from indexing and may even be slowed down by it. Furthermore, indexing increases memory usage. However, for long running problems indexing can notably improve performance. Note that indexing can introduce subtle inevitable variations in the order in which clauses are processed (variations in the order of clauses having the same heuristic weight). As a result different proofs may be found and speed-ups or slow-downs can partly be attributed to a more or less efficient search rather than indexing.

  • memLimit: a number specifying the maximal heap size (in bytes) permitted (default: 512MB); exceeding this limit results in calling the callback with an error (an instance of Error); the currently used heap size that serves as the point of reference is obtained through process.memoryUsage().heapUsed.

  • timeout: a number specifying a timeout in milliseconds (default: no timeout); the callback will be called with state stopped if the Resolution procedure did not terminate before the timeout expired. The result of incurring the timeout is not different from a "manual" stop issued through the monitor (see Return Value).

  • weighting: a function computing the (heuristic) weight of a clause (default: literals count); the function should accept one argument, namely a clause. In order to produce a sensible weight for such a clause the internal data structure of clauses must be taken into account (see lib/weight.js for details). You may also use the currently available weighting functions (see weighting exported by main module index.js) and combine them, e.g. as a weighted sum.

A monitor object is returned that can be used to monitor the progress of the Resolution procedure, or to stop it. To this end the object returned has the following properties that are functions:

  • stop(): stops the Resolution procedure

  • getState(): returns the current state of the Resolution procedure (a string)

  • getElapsedHrtime(): returns the time elapsed (in process.hrtime format) since the start of the Resolution procedure if it is still running; the return value is undefined if the procedure has not yet been or never was started (due to erroneous or invalid input, for instance); otherwise, if the procedure terminated successfully, returns the time it took until termination.

  • getStatistic(name): returns the value of the statistic specified by its name (a string); a valid name is any of the property names listed as statistical data in the result object passed to the callback (cp. statistics above and below in the examples)

The following piece of code:

var propsat = require('propsat');
var result;
var monitor = propsat.run('-A B\nA\n-B', function(err, res) { result = res; }, {level: 3, log: console.log});

will produce the following output on the console:

INITIAL SET OF CLAUSES (3):
  A
  -B
  B -A
Given Clause [1]: A
Given Clause [1]: -B
Given Clause [2]: B -A
Derived Clause [1]: B (from B -A and A by resolving upon A)
Derived Clause [0]: 0 (from B and -B by resolving upon B)
The empty clause was derived
Time elapsed: 2ms
STATISTICS:
        Initial Clauses: 3
       Inactive Clauses: 1
         Active Clauses: 3
          Given Clauses: 3
        Derived Clauses: 2
      Activated Clauses: 5
    Parent Subsumptions: 0
   Forward Subsumptions: 0
  Backward Subsumptions: 1
          Links Created: 3
            Proof Depth: 2
  Clauses Used In Proof: 5
      Search Efficiency: 1.00

Note that a number in brackets is the weight of the respective clause which simply is the number of literals in this case.

Furthermore, result.state is 'done', result.statistics is

{ initialClauses: 3,
  forwardSubsumptions: 0,
  backwardSubsumptions: 1,
  parentSubsumptions: 0,
  derivedClauses: 2,
  givenClauses: 3,
  activatedClauses: 5,
  inactiveClauses: 1,
  activeClauses: 3,
  linksCreated: 3 }

Moreover, result.emptyClause.proofLength() returns 5, result.emptyClause.proofDepth() returns 2, and result.emptyClause.extractProof() returns:

[ '[1] B -A (given)',
  '[2] A (given)',
  '[3] B from [1] and [2] by resolving upon A',
  '[4] -B (given)',
  '[5] 0 from [3] and [4] by resolving upon B' ]

(Note that 0 represents the empty clause.)

The monitor object is not particularly useful for such a trivial set of clauses, but it can be used to obtain the elapsed time in its raw form. That is, monitor.getElapsedHrtime() returns [ 0, 1737848 ] (which may of course vary).

When dropping the third clause -B from the set of clauses, the set of clauses becomes consistent (satisfiable) and then result.assignment is defined and has the value { A: true, B: true }.

Executes a Tableaux-based procedure on the given set of clauses. Except for the first parameter all parameters are optional. However, the order of the parameters is crucial. That is, no attempt is made to shift parameter positions based on possibly heuristic criteria. So if you omit one or more parameters preceding a parameter you want to supply, supply the omitted parameters as null.

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.

Function runTableaux is asynchronous and returns immediately. The result or an error is reported as usual through a callback function that should have two parameters, namely an error object and a result object. In case of an error or failure, the first parameter is the error object and the second parameter is omitted. Otherwise the first parameter is null and the second parameter holds the result. The result is an object conforming to the following conventions:

  • Property state is always defined. Its value is a string that is equal to one of the following string literals:

    • 'aborted': The Tableaux procedure was aborted due to insufficient or inappropriate input. (Typically, this state occurs when the initial set of clauses is empty.) Besides property state a second property message is defined in this case. Its value is a detail message (i.e., a string) providing background information.

    • 'stopped': The Tableaux procedure was stopped. (See section on return value for details on how to stop a running Tableaux procedure.) Besides property state a second property message is defined in this case. Its value is a detail message (i.e., a string) providing additional information.

    • 'done': The Tableaux procedure terminated successfully, meaning the tableaux was closed, or a satisfying assignment for the given set of clauses was found. In this case further properties of the result object contain the relevant data and information. These are explained in what follows.

  • If a proof of inconsistency or unsatisfiability was found the following properties are defined in addition to property state:

    • time: the time it took to close the tableaux (a string including a suitable time unit intended for human eyes); if you are interested in process.hrtime-style time measurement use the monitor (see Return Value).

    • message: its value is a message (a string) providing additional information

    • statistics: statistical data regarding the search conducted by the Tableaux procedure

  • If a satisfying assignment was found the following properties are defined in addition to property state:

    • assignment: an assignment (one of possibly many more) that satisfies the given set of clauses

    • time: the time it took to ascertain satisfiability (a string including a suitable time unit intended for human eyes); if you are interested in process.hrtime-style time measurement use the monitor (see Return Value).

    • statistics: statistical data regarding the search conducted by the Tableaux procedure

An object that allows the caller to obtain logging information during the execution of the Tableaux procedure. The logger object should have a property level, an integer number ranging from 0 to 3, that controls the verbosity of logging or the amount of data passed on to the second property log, a function that should have one parameter of type string. As usual, a higher level increases the amount of logging. A simple logging scenario is to log to the console through the logger {level: 2, log: console.log}, for instance.

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:

  • timeout: a number specifying a timeout in milliseconds (default: no timeout); the callback will be called with state stopped if the Tableaux procedure did not terminate before the timeout expired. The result of incurring the timeout is not different from a "manual" stop issued through the monitor (see Return Value).

A monitor object is returned that can be used to monitor the progress of the Tableaux procedure, or to stop it. To this end the object returned has the following properties that are functions:

  • stop(): stops the Tableaux procedure

  • getState(): returns the current state of the Tableaux procedure (a string)

  • getElapsedHrtime(): returns the time elapsed (in process.hrtime format) since the start of the Tableaux procedure if it is still running; the return value is undefined if the procedure has not yet been or never was started (due to erroneous or invalid input, for instance); otherwise, if the procedure terminated successfully, returns the time it took until termination.

  • getStatistic(name): returns the value of the statistic specified by its name (a string); a valid name is any of the property names listed as statistical data in the result object passed to the callback (cp. statistics above)

Runs the WalkSat procedure to find a satisfying assignment for the given set of clauses. Except for the first parameter all parameters are optional. However, the order of the parameters is crucial. That is, no attempt is made to shift parameter positions based on possibly heuristic criteria. So if you omit one or more parameters preceding a parameter you want to supply, supply the omitted parameters as null.

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.

Function runWalkSat is asynchronous and returns immediately. The result or an error is reported as usual through a callback function that should have two parameters, namely an error object and a result object. In case of an error or failure, the first parameter is the error object and the second parameter is omitted. Otherwise the first parameter is null and the second parameter holds the result. The result is an object conforming to the following conventions:

  • Property state is always defined. Its value is a string that is equal to one of the following string literals:

    • 'aborted': The WalkSat procedure terminated without finding a satisfying assignment.

    • 'stopped': The WalkSat procedure was stopped. (See section on return value for details on how to stop a running WalkSat procedure.)

    • 'done': The WalkSat procedure terminated successfully, meaning a satisfying assignment for the given set of clauses was found. In this case property assignment holds the assignment found (see below).

  • Property statistics is always defined. Its value is an object that holds statistical data summarizing the search conducted by the WalkSat procedure through the following properties:

    • starts: the total number of starts (i.e., random assignments from which a climb was initiated)

    • steps: the total number of steps or assignments visited

  • Property time is always defined. Its value is a human-readable string representing the (wall clock) time elapsed. Use the monitor (see Return Value below) for process.hrtime-style time measurement.

  • Property assignment is available if the WalkSat procedure found an assignment. Its value is that very assignment.

An object that allows the caller to obtain logging information during the execution of the WalkSat procedure. The logger object should have a property level, an integer number ranging from 0 to 2, that controls the verbosity of logging or the amount of data passed to the second property log, a function that should have one parameter of type string. As usual, a higher level increases the amount of logging. A simple logging scenario is to log to the console through the logger {level: 1, log: console.log}, for instance.

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:

  • starts: the maximal number of starts (i.e., random assignments from which to start climbing); default is 100

  • ascent: the ascent type; use one of the following string values: 'min', 'max', 'rnd' for lowest, steepest, and random ascent, respectively; default is random

A monitor object is returned that can be used to monitor the progress of the WalkSat procedure, or to stop it. To this end the object returned has the following properties that are functions:

  • stop(): stops the WalkSat procedure

  • getState(): returns the current state of the WalkSat procedure (a string)

  • getElapsedHrtime(): returns the time elapsed (in process.hrtime format) since the start of the Walksat procedure if it is still running; the return value is undefined if the procedure has not yet been or never was started (due to erroneous or invalid input, for instance); otherwise, if the procedure terminated successfully, returns the time it took until termination.

  • getStatistic(name): returns the value of the statistic specified by its name (a string); a valid name is any of the property names listed as statistical data in the result object passed to the callback (cp. statistics above)

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.

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.

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

See also: clausesSatisfiedBy

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.

This is the synchronous version of writeClausesToFile.