Package Exports

sat-solver
sat-solver/index.js

This package does not declare an exports field, so the exports above have been automatically detected and optimized by JSPM instead. If any package subpath is missing, it is recommended to post an issue to the original package (sat-solver) to support the "exports" field. If that is not possible, create a JSPM override to customize the exports field for this package.

Readme

Sat solver

This is a simple SAT solver with a string based interface, built for easy access. It tries to parse many different commenly used syntaxes into a AST and then solves the problem, returning one or all solutions. You may also only use the AST and provide a solver yourself. The built in solver is logic-solver which itself is based on a js MiniSat implementation.

Installation

npm install sat-solver

Usage

Note that biconditional implications are not supported and implications only in one direction. A incomplete list of supported syntaxes can be found below

const { solve } = require('sat-solver');

solve('a | (b & c)').findOne()  // { a: true, b: false, c: false }

solve('a | (b & c)').findAll()  // [
                                //   { a: true, b: false, c: false },
                                //   { a: true, b: false, c: true },
                                //   { a: true, b: true, c: true },
                                //   { a: true, b: true, c: false },
                                //   { a: false, b: true, c: true }
                                // ]

solve('a | (b & c)').getAstTree() // [ 'a', Symbol(or), [ 'b', Symbol(and), 'c' ] ]

// the operators may be found here
const { operators } = require('sat-solver');

// you may also dig into logic-solver to solve it in a differnt way
solve('a | (b & c)').getSolver()

Different syntaxes include (may be mixed)

solve('-a | (b & c)')
solve('!a || (b && c)')
solve('not a or (b and c)')
solve('¬a ∨ (b ∧ c)')

solve("a => b")
solve("a implies b")
solve("a -> b")
solve("a → b")
solve("a ⇒ b")

solve("a xor b")
solve("a ⊻ b")