3-SAT - Naive Solver

This repo provides a naive solver for the 3-Sat problem.

The naive solution is based on the following steps:

1. generate all possible interpretations of the expression
2. check if any of the interpretations makes the expression satisfiable

The expression parser, the abstract synthax tree builder and the evaluator are widely inspired by this repo.

Usage

To formulate the expression, you can use:

• the variables: 'a', 'b' and 'c';
• the operations: '&' (and), '|' (or), and '!' (not);
• the parenthesis: '(', ')'

Option 1: online

Using runkit. Simply click here and copy/paste this code:

const { NaiveSat } = require("naive-3-sat");

const expr = '((!a & b) | (b | c)) & (c & !a)';

const nsat = new NaiveSat(expr);

nsat.printSat();

Option 2: use npm

You will need node JS installed.

1. Install the library:

npm install naive-3-sat

2. Run the below command:

node node_modules/naive-3-sat/index.js
>.sat (!a & b) | (c & !c)

        Expression (!a & b) | (c & !c) is satifiable.
        A possible assignment is: {"a":0,"b":1,"c":1}
        Its interpretations is: "(!0 & 1) | (1 & !1)"

Option 3: clone this repo

You will need node JS installed.

You can clone this repo then run:

node index.js
>.sat (!a & b) | (c & !c)

        Expression (!a & b) | (c & !c) is satifiable.
        A possible assignment is: {"a":0,"b":1,"c":1}
        Its interpretations is: "(!0 & 1) | (1 & !1)"