Skip to content

Commit

Permalink
Further documentation improvements and version patch bump
Browse files Browse the repository at this point in the history
  • Loading branch information
wkschwartz committed Jan 30, 2014
1 parent 19e6f1c commit 4a5c6a9
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 36 deletions.
37 changes: 2 additions & 35 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ source files are included in this repository. Go's
finds, but I can't figure out how to get it to work. So you'll have to compile
PicoSAT first. For this reason, PiGoSAT is not `go get`able. The following
commands should be sufficient to compile `libpicosat` on most Unix systems. (If
know how to compile PiGoSAT on Windows, please submit instructions and I will
add them; see the "Contributing" section).
you know how to compile PiGoSAT on Windows, please submit instructions and I
will add them; see the "Contributing" section).

```bash
$ cd picosat
Expand All @@ -42,39 +42,6 @@ tests and if they pass, installs PiGoSAT. (Ensure your
$ go test && go install
```

Use
---

After completing the building and installation steps above, importation should
work as usual. Create a `Pigosat` object `p` and use its methods. Even though
PicoSAT is written in C, PiGoSAT manages memory for you using
`runtime.SetFinalizer`. (If you reset a `Pigosat` instance `p`'s finalizer, you
will have to call `p.Delete` explicitly, which is best done with `defer` right
after reseting the finalizer; most users will not need to worry about this.)

Designing your model is beyond the scope of this document, but Googling
"satisfiability problem", "conjunctive normal form", and "DIMACS" are good
places to start. Once you have your model, number its variables from 1 to
_n_. Construct clauses as slices of `int32`s giving the index of each
variable. Negate each variable's index if the model's literal is negated. Add
the clauses with `Pigosat.AddClauses`. Solve the formula with
`Pigosat.Solve`. See each method's godoc comment for more information.


```go
package main
import "pigosat"
func main() {
p := pigosat.NewPigosat(0)
p.AddClauses([][]int32{{1, 2}, {-2}})
status, solution := p.Solve()
// Now status should equal pigosat.Satisfiable and solution should be
// such that solution[1] == true and solution[2] == false. solution[0]
// is always ignored.
}
```


Contributing
------------

Expand Down
8 changes: 7 additions & 1 deletion pigosat.go
Original file line number Diff line number Diff line change
@@ -1,6 +1,12 @@
// Copyright William Schwartz 2014. See the LICENSE file for more information.

// Package pigosat is a Go binding for the PicoSAT satisfiability solver.
//
// Designing your model is beyond the scope of this document, but Googling
// "satisfiability problem", "conjunctive normal form", and "DIMACS" are good
// places to start. Once you have your model, create a Pigosat instance p with
// pigosat.NewPigosat, add the model to the instance with p.AddClauses, and
// solve with p.Solve.
package pigosat

// picosat/libpicosat.a must exist to build this file. See README.md.
Expand All @@ -14,7 +20,7 @@ import "runtime"
import "sync"
import "time"

var Version = SemanticVersion{0, 2, 1, "", 0}
var Version = SemanticVersion{0, 2, 2, "", 0}

// PicosatVersion returns the version string from the underlying Picosat
// library.
Expand Down

0 comments on commit 4a5c6a9

Please sign in to comment.