A simple SAT solver that utilizes an iterative algorithm. The algorithm uses a watchlist to keep track of all the assignments.

Most of the code is based on the Python implementation by sahands, which can be downloaded here. Some checking was done utilizing another port found here.

The primary motivation for this port was to create a code base that could support the future work and requirements of ZPS while also maintaining a generic interface that others may find useful.

go get github.com/fezz-io/sat

import (
	"github.com/fezz-io/sat"
)

variableA := NewVariable("A")
variableB := NewVariable("B")

solver := NewSolver()
solver.AddClause(variableA, variableB)

satisfiable, solutions := solver.Satisfiable()

fmt.Printf("Satisfiable?: %t\nSolutions:", satisfiable)
for i, soln := range solutions {
	fmt.Printf("\n%d:\n", i)
	soln.Print()
}