propsat

Propositional Satisfiability Checker

npm install propsat
28 downloads in the last week
32 downloads in the last month

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

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.

Installation

$ npm install propsat

Quick Run

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

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

Essential Data Structures

Assignment

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.

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

var propsat = require('propsat');

Module propsat exports the following functions:

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.

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

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.

See also: initialAssignment, nextAssignment, createNextAssignment

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

isPropFormInconsistent (pf, cb)

Checks whether a given propositional formula pf is inconsistent. The Resolution procedure is employed to determine inconsistency (i.e., unsatisfiability). 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.

isPropFormTautology (pf, cb)

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.

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.

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, cb)

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.

propFormToClausesSync (pf)

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

propFormToCnf (pf, cb)

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.

propFormToCnfSync (pf)

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

propFormToString (pf, opPadding, style)

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:

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

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.

runGaSat (clauses, callback, logger, options)

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.

Note that the current implementation is limited to elite selection with n-point crossover. Future versions will introduce fitness-proportionate selection and one-point (and possibly two-point) crossover as well as mutation.

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.

callback

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

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

logger

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.

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:

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

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

  • 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

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

Return Value

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; returns 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)

runResolution (clauses, callback, logger, options)

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.

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.

callback

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

logger

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.

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:

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

Return Value

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; returns 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)

Example:

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

runTableaux (clauses, callback, logger, options)

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.

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.

callback

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 the string literal 'unsatisfiable'

    • 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

logger

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.

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:

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

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; returns 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)

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.

stringToPropform (propForm)

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.

npm loves you