Native-sat-solver-package NPM

NPM Package: `Native-Sat-Solver-Package`

Native-Sat-Solver-Addon is a SAT Solver npm addon, written in C++ to complex Boolean satisfiability problems. This addon utilizes Tseitin's transformation, a transformation technique that efficiently converts logical formulas into Conjunctive Normal Form (CNF), a standard format for SAT solving. Once a formula is in CNF, it can then be efficiently solved using the DPLL (Davis-Putnam-Logemann-Loveland) algorithm. The goal of this addon is to provide a fast and efficient tool for solving satisfiability problems in popular JavaScript frameworks.

Note: Underly SAT Solver is based on another one of my repositories which can be found here

Dependencies

The addon is dependent on node-gyp which results in the following dependencies:

Linux & MacOS

Python v3.7, v3.8, v3.9, or v3.10

Windows

Python v3.7, v3.8, v3.9, or v3.10
Install Visual C++ Build Environment: Visual Studio Build Tools (using "Visual C++ build tools" workload) or Visual Studio Community (using the "Desktop development with C++" workload)

More Info

For more info see the node-gyp dependencies (click here))

Installation

Use the package manager npm to install native-sat-solver-package.

npm i native-sat-solver-package

Usage

The SAT Solver will accept strings as input. These input strings are representative of boolean formulas and must adhere to the following rules.

Rules

Operators

*: represents the boolean AND operator
+: represents the boolean OR operator
-: represents the boolean NOT operator

Order of Operations

The order of operations will be enforeced as follows with 1 being the higest order and 4 being the lowest order. 1. ( or ) (Paranthesis) 2. - (NOT) 3. * (AND) 4. + (OR)

Grammar Rules

Variable names must start with a character of the alphabet (uppercase or lowercase)
Variable names can consist of letters and digits
Variable length must be less than 11 characters
Can use arbitrary amounts of whitespace between terms of the grammar

Example Input Strings

Here are some examples input strings:

a+c
a*---a
 ( (-a)+(a*b)) * a * (c + -b) *-c
(a+b+c)*(a+b+-c)*(-b+a +c)*(-a*-c)
(a+b+c)*(a+b+-c)*(-b+a +c)*(a+-b+-c)*(-a+b+c)*(-a+b+-c)*(-a+-b+c)*(-a+-c+-c)
(a+b+c)*(a+b+-c)*(-b+a +c)*(a+-b+-c)*(-a+b+c)*(-a+b+-c)*(-a+-b+c)*(-a+-c+-b)
(a+b+c)*(a+b+-c)*(-b+a +c)*(a+-b+-c)*(-a+b+c)*(-a+b+-c)*(-a+-b+c)
VAr1 * -VAr1
VAr1 + -VAr1
 -((A*  B)+ C)
 (A+-B+C) * (B+C) * (-A+ C) * (B +-C) * -               (C)
(a1)*(-a1+a2) * (-a2+a3) *(-a3)
  (-B*-C * D) + (-B * -  D) + (C *D) + (B)         
(B+C+-D)  *(D+B)*(-C+-D)* (-B)

Using the Addon

const SAT = require('native-sat-solver-package')

// returns 'sat'
console.log(SAT.solve('Var1 + -Var1'))

// returns 'usat'
console.log(SAT.solve('a*---a'))

// returns 'unsat'
console.log(SAT.solve('(B+C+-D)*(D+B)*(-C+-D)*(-B)'))