A simple DPLL sat solver implemented in Elm.

Note: This repository is maintained at https://gitlab.com/findley/elm-sat and mirrored to https://github.com/tortis/elm-sat.

The Problem type is just an alias for List (List Int). Variables (literals) are represented by integers where a negative integer indicates negation of the literal.

Sat problems must be in CNF form.

import Sat

problem : Sat.Problem
problem = [ [ 1, 2 ], [ 1, 3 ], [ 2, 3 ], [ -1, -2, -3 ], [ 2, 3 ], [ -2, -3 ] ]

solution : Maybe Sat.Solution
solution = Sat.solve problem -- Just [1,2,-3]

The Sat.Utils module exposes fromDimacs which will turn a DIMACS formatted string into a Problem.

Elm Sat performance appears to be worse than MiniSAT compiled to JS. Adding benchmarks and improving performance are areas for future development.

This code is distributed under the MIT license, see the LICENSE file.