README.md

Go SAT solver

This isn't the most effective implementation. This code was written as an assignment for a Logic Course at MIM UW (2020). The implementation should be fairly bug-less.

See online (WASM) version

Run using Docker

If you have Docker installed you can run the solver simply using:

    $ docker run -i styczynski/go-sat-solver:1.0.0 < input_formula.txt

Please read the rest of the README to learn how to work with input formats.

Quickstart

You have to install go on your machine

   $ GO111MODULE=on go get -u github.com/styczynski/go-sat-solver
   $ go-sat-solver input.txt # Run the executable

If the shell cannot find the executable you may want to do export PATH=$PATH:/usr/local/go/bin.

Build or Install using make

• make install - adds the binary to $GOPATH/bin
• make build - builds the binary

The Makefile builds the binary and adds the short git commit id and the version to the final build.

Usage

The solver can the executed using go-sat-solver [input files] command. The default input format is haskell-like ADT syntax:

    X := And (X) (X) | Or (X) (X) | Iff (X) (X) | Implies (X) (X) | Not (X) | Var "string" | T | F

Use no parameters or "-" to load from standard input:

    $ go-sat-solver < file.in
    $ cat file.in | go-sat-solver -
    $ go-sat-solver file.in

The presented commands are equivalent.

You may want to load other types of files for example DIMACS CNF:

    $ go-sat-solver -f cnf input.cnf

Or use other solver than the default one (currently cnf and naive options are supported):

    $ go-sat-solver -s naive input.txt

About the solver itself

The solver was firstly a DPLL-style solver but further improvements led to CDCL-like solver. I was using Minisat source code as a reference. The solver supports the following features:

• Unit propagation
• Adaptive VSIDS
• TWL
• Clause learning
• Variable elimination techniques

The learned clauses are not optimized based on adaptive VSIDS, but this feature is planned in the future.

This solver is suitable for any serious application, but you shall consider using other Go solvers, or native C/C++ solvers for a better performance.

Web interface

Solver has its web interface available (this was done using compilation of Go to WASM).

You can compile the frontend in a following way:

    $ make wasm
    $ make build-web

Running tests

You can run testing scripts that examines the solver on inputs from /tests/ directory using the following command:

    $ go run ./cmd/tester/tester.go ./tests