Initial code commit

README.md

@@ -1,2 +1,2 @@
-# saturday
-A basic SAT solver heavily inspired by MiniSat.
+# Saturday
+A SAT solver modeled after the [MiniSat paper](http://minisat.se/downloads/MiniSat.pdf).

lit/lit.go

@@ -0,0 +1,58 @@
+package lit
+
+import "fmt"
+
+const Undef = Lit(-1)
+
+// Lit is a literal represented by an integer. The sign of the literal is
+// represented by the least significant bit, and the value is obtained by
+// performing a right bit shift. This encoding makes L and ~L adjacent when
+// sorted.
+//
+// An unknown literal is denoted as -1.
+type Lit int
+
+// New returns a new literal given a 0-index variable, v, and whether the
+// literal is negative.
+func New(v int, neg bool) Lit {
+	if neg {
+		return Lit(v + v + 1)
+	}
+	return Lit(v + v)
+}
+
+// NewFromInt returns a new literal with a variable equal to i.
+func NewFromInt(i int) Lit {
+	if i < 0 {
+		return New(-i-1, true)
+	}
+	return New(i-1, false)
+}
+
+// Not negates a literal.
+func (l Lit) Not() Lit {
+	return Lit(l ^ 1)
+}
+
+// Sign returns true if the literal is negative.
+func (l Lit) Sign() bool {
+	return l&1 == 1
+}
+
+// Index returns the literal's index.
+func (l Lit) Index() int {
+	return int(l >> 1)
+}
+
+// Var returns the literal's variable.
+func (l Lit) Var() int {
+	return int(l>>1) + 1
+}
+
+// String implements the Stringer interface.
+func (l Lit) String() string {
+	if l.Sign() {
+		return fmt.Sprintf("~%d", l.Var())
+	}
+	return fmt.Sprintf("%d", l.Var())
+}

lit/lit_queue.go

@@ -0,0 +1,39 @@
+package lit
+
+// Queue for literals. Note that this is not async-safe.
+type Queue struct {
+	items []Lit
+}
+
+// NewQueue returns a new queue.
+func NewQueue() *Queue {
+	return &Queue{
+		items: []Lit{},
+	}
+}
+
+// Insert inserts a new lit into the queue.
+func (q *Queue) Insert(l Lit) {
+	q.items = append(q.items, l)
+}
+
+// Dequeue pops the first lit off the queue.
+func (q *Queue) Dequeue() Lit {
+	if len(q.items) == 0 {
+		return Undef
+	}
+	first := q.items[0]
+	q.items = q.items[1:len(q.items)]
+
+	return first
+}
+
+// Clear clears the queue.
+func (q *Queue) Clear() {
+	q.items = []Lit{}
+}
+
+// Size returns the size of the queue.
+func (q *Queue) Size() int {
+	return len(q.items)
+}

lit/lit_queue_test.go

@@ -0,0 +1,52 @@
+package lit
+
+import "testing"
+
+func TestQueueInsert(t *testing.T) {
+	q := NewQueue()
+
+	if q.Insert(New(0, false)); len(q.items) != 1 {
+		t.Fatalf("TestQueueInsert() failed, got: %d", len(q.items))
+	}
+}
+
+func TestQueueDequeue(t *testing.T) {
+	q := NewQueue()
+	lit1 := New(0, false)
+	lit2 := New(1, false)
+	lit3 := New(2, true)
+
+	q.Insert(lit1)
+	q.Insert(lit2)
+	q.Insert(lit3)
+
+	if o := q.Dequeue(); o != lit1 {
+		t.Fatalf("TestQueueInsert() failed, got: %s", o)
+	}
+	if o := q.Dequeue(); o != lit2 {
+		t.Fatalf("TestQueueInsert() failed, got: %s", o)
+	}
+	if o := q.Dequeue(); o != lit3 {
+		t.Fatalf("TestQueueInsert() failed, got: %s", o)
+	}
+}
+
+func TestQueueClear(t *testing.T) {
+	q := NewQueue()
+	q.Insert(New(0, false))
+	q.Insert(New(1, false))
+
+	if q.Clear(); len(q.items) != 0 {
+		t.Fatalf("TestQueueClear() failed, got: %d", len(q.items))
+	}
+}
+
+func TestQueueSize(t *testing.T) {
+	q := NewQueue()
+	q.Insert(New(0, false))
+	q.Insert(New(1, false))
+
+	if q.Size() != 2 {
+		t.Fatalf("TestQueueSize() failed, got: %d", q.Size())
+	}
+}

lit/lit_test.go

@@ -0,0 +1,36 @@
+package lit
+
+import "testing"
+
+func TestNewFromInt(t *testing.T) {
+	if lit := NewFromInt(12); lit.Var() != 12 {
+		t.Fatalf("TestNewFromInt() failed, got: %d", lit.Var())
+	}
+	if lit := NewFromInt(-12); lit.Var() != 12 {
+		t.Fatalf("TestNewFromInt() failed, got: %d", lit.Var())
+	}
+}
+
+func TestNot(t *testing.T) {
+	if lit := New(12, false).Not(); lit != New(12, true) {
+		t.Fatalf("TestNot() failed, got: %d", lit.Var())
+	}
+}
+
+func TestSign(t *testing.T) {
+	if lit := New(12, true); lit.Sign() != true {
+		t.Fatalf("TestSign() failed, got: %d", lit.Var())
+	}
+	if lit := New(12, false); lit.Sign() != false {
+		t.Fatalf("TestSign() failed, got: %d", lit.Var())
+	}
+}
+
+func TestVar(t *testing.T) {
+	if lit := New(23, false); lit.Var() != 24 {
+		t.Fatalf("TestVar() failed: %d", lit.Var())
+	}
+	if lit := New(23, true); lit.Var() != 24 {
+		t.Fatalf("TestVar() failed: %d", lit.Var())
+	}
+}

main.go

@@ -0,0 +1,35 @@
+package main
+
+import (
+	// "flag"
+	"fmt"
+	"github.com/ericr/saturday/solver"
+	"log"
+	"os"
+)
+
+func main() {
+	printBanner()
+
+	logger := log.New(os.Stdout, "", log.Ldate|log.Ltime)
+
+	sat := solver.New(logger)
+	sat.AddClause([]int{-1, -3, 5})
+	sat.AddClause([]int{-1, -3, -5})
+
+	if sat.Solve([]int{1}) {
+		fmt.Println("\nSAT")
+
+		for i, val := range sat.Answer() {
+			fmt.Printf("%d = %t\n", i, val)
+		}
+	} else {
+		fmt.Println("\nUNSAT")
+	}
+}
+
+func printBanner() {
+	fmt.Printf("Saturday Solver %s\n", solver.Version())
+	fmt.Println("https://ericrafaloff.com/saturday")
+	fmt.Println("")
+}