README
¶
⊧ Gini: A fast SAT solver.
The Gini sat solver is a fast, clean SAT solver written in Go. It is to our knowledge the first ever performant pure-Go SAT solver made available.
This solver is fully open source, originally developped at IRI France.
Build/Install
For the impatient:
go install github.com/go-air/gini/...@latest
I recommend however building the package github.com/go-air/gini/internal/xo with bounds checking turned off. This package is all about anything-goes performance and is the workhorse behind most of the gini sat solver. It is also extensively tested and well benchmarked, so it should not pose any safety threat to client code. This makes a signficant speed difference (maybe 10%) on long running problems.
The SAT problem in 5 minutes
Usage
Our user guide shows how to solve SAT problems, circuits, do Boolean optimisation, use concurrency, using our distributed CRISP protocol, and more.
Citing Gini
Zenodo DOI based citations and download:
BibText:
@misc{scott_cotton_2019_2553490,
author = {Scott Cotton},
title = {go-air/gini: Sapeur},
month = jan,
year = 2019,
doi = {10.5281/zenodo.2553490},
url = {https://doi.org/10.5281/zenodo.2553490}
}
Documentation
¶
Overview ¶
Package gini provides a fast SAT solver.
Package gini contains both libraries and commands. The libraries include
- A high quality, core single goroutine SAT solver (internal package xo).
- Concurrent solving utilities (gini/ax, ...)
- CRISP-1.0 client and server (gini/crisp)
- Generators (gini/gen)
- benchmarking library (gini/bench)
- scoped assumptions
- logic library ...
The commands include
- gini, a command for solving SAT problems in cnf and icnf formats, and a CRISP-1.0 client.
- bench, a utility for constructing, running, and comparing benchmarks
- crispd, CRISP-1.0 server
Example (Sudoku) ¶
package main
import (
"fmt"
"github.com/go-air/gini"
"github.com/go-air/gini/z"
)
func main() {
g := gini.New()
// 9 rows, 9 cols, 9 boxes, 9 numbers
// one variable for each triple (row, col, n)
// indicating whether or not the number n
// appears in position (row,col).
var lit = func(row, col, num int) z.Lit {
n := num
n += col * 9
n += row * 81
return z.Var(n + 1).Pos()
}
// add a clause stating that every position on the board has a number
for row := 0; row < 9; row++ {
for col := 0; col < 9; col++ {
for n := 0; n < 9; n++ {
m := lit(row, col, n)
g.Add(m)
}
g.Add(0)
}
}
// every row has unique numbers
for n := 0; n < 9; n++ {
for row := 0; row < 9; row++ {
for colA := 0; colA < 9; colA++ {
a := lit(row, colA, n)
for colB := colA + 1; colB < 9; colB++ {
b := lit(row, colB, n)
g.Add(a.Not())
g.Add(b.Not())
g.Add(0)
}
}
}
}
// every column has unique numbers
for n := 0; n < 9; n++ {
for col := 0; col < 9; col++ {
for rowA := 0; rowA < 9; rowA++ {
a := lit(rowA, col, n)
for rowB := rowA + 1; rowB < 9; rowB++ {
b := lit(rowB, col, n)
g.Add(a.Not())
g.Add(b.Not())
g.Add(0)
}
}
}
}
// function adding constraints stating that every box on the board
// rooted at x, y has unique numbers
var box = func(x, y int) {
// all offsets w.r.t. root x,y
offs := []struct{ x, y int }{{0, 0}, {0, 1}, {0, 2}, {1, 0}, {1, 1}, {1, 2}, {2, 0}, {2, 1}, {2, 2}}
// all numbers
for n := 0; n < 9; n++ {
for i, offA := range offs {
a := lit(x+offA.x, y+offA.y, n)
for j := i + 1; j < len(offs); j++ {
offB := offs[j]
b := lit(x+offB.x, y+offB.y, n)
g.Add(a.Not())
g.Add(b.Not())
g.Add(0)
}
}
}
}
// every box has unique numbers
for x := 0; x < 9; x += 3 {
for y := 0; y < 9; y += 3 {
box(x, y)
}
}
if g.Solve() != 1 {
fmt.Printf("error, unsat sudoku.\n")
return
}
for row := 0; row < 9; row++ {
for col := 0; col < 9; col++ {
for n := 0; n < 9; n++ {
if g.Value(lit(row, col, n)) {
fmt.Printf("%d", n+1)
break
}
}
if col != 8 {
fmt.Printf(" ")
}
}
fmt.Printf("\n")
}
}
Output: 5 2 9 1 3 6 7 4 8 4 3 1 7 8 5 2 9 6 8 7 6 4 9 2 1 3 5 1 6 3 2 4 8 5 7 9 2 4 5 9 1 7 8 6 3 7 9 8 5 6 3 4 1 2 6 5 4 3 2 1 9 8 7 3 1 2 8 7 9 6 5 4 9 8 7 6 5 4 3 2 1
Index ¶
- func NewS() inter.S
- func NewSv() inter.Sv
- func NewSvVars(vs *z.Vars) inter.Sv
- type Gini
- func (g *Gini) Activate() (m z.Lit)
- func (g *Gini) ActivateWith(act z.Lit)
- func (g *Gini) ActivationLit() z.Lit
- func (g *Gini) Add(m z.Lit)
- func (g *Gini) Assume(ms ...z.Lit)
- func (g *Gini) Copy() *Gini
- func (g *Gini) Deactivate(m z.Lit)
- func (g *Gini) GoSolve() inter.Solve
- func (g *Gini) Lit() z.Lit
- func (g *Gini) MaxVar() z.Var
- func (g *Gini) Reasons(dst []z.Lit, m z.Lit) []z.Lit
- func (g *Gini) SCopy() inter.S
- func (g *Gini) Solve() int
- func (g *Gini) Test(dst []z.Lit) (res int, out []z.Lit)
- func (g *Gini) Try(dur time.Duration) int
- func (g *Gini) Untest() int
- func (g *Gini) Value(m z.Lit) bool
- func (g *Gini) Why(ms []z.Lit) []z.Lit
- func (g *Gini) Write(dst io.Writer) error
Examples ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
Types ¶
type Gini ¶
type Gini struct {
// contains filtered or unexported fields
}
Gini is a concrete implementation of solver
func NewVc ¶
NewVc creates a new Gini solver with hint for capacity of variables set to vCapHint, and likewise capacity of clauses set cCapHint
func (*Gini) Activate ¶ added in v1.0.2
Create a clause from the last (non 0-terminated, non-empty) sequence of Adds and `m.Not()`. Activate panics if the last sequence of Adds since Add(0) is empty, in other words, don't try to use an activation literal for the empty clause.
Additionally, in this case subsequent behavior of `g` is undefined. The caller should verify a clause is not empty using `g.Value(m)` for all literals in in the clause to activate.
To active the clause, assume `m`.
Example:
if g.Value(a) != false || g.Value(b) != false {
g.Add(a)
g.Add(b)
m := g.Activate() // don't call g.Add(0).
g.Assume(m) // now the clause (a + b) is active
if g.Solve() == 1 {
// do something
}
// now the clause (a+b) is not active.
g.Deactivate(m)
// now `m` can be re-used and the solver can ignore
// clauses with `m`.
}
Activation of all clauses can be used in conjunction with cardinality constraints to easily create a MAXSAT solver.
Activate is an unsupported operation under a test scope and will panic if called under a test scope.
func (*Gini) ActivateWith ¶ added in v1.0.2
ActivateWith allows the caller to specify the activation literal. It is useful when the caller needs to activate many clauses with one literal. However, please note that activation literals are volatile and will be recycled on Deactivate. As with Activate, ActivateWith should not be used to activate the empty clause. In this case, ActivateWith panics and subsequent behavior of g is undefined.
ActivateWith is an unsupported operation under a test scope and will panic if called under a test scope.
func (*Gini) ActivationLit ¶ added in v1.0.2
ActivationLit returns a new literal to be used with ActivateWith().
ActivationLit is an unsupported operation under a test scope and will panic if called under a test scope.
func (*Gini) Add ¶
Add implements inter.S. To add a clause (x + y + z), one calls
g.Add(x) g.Add(y) g.Add(z) g.Add(0)
If Add is called under a test scope, then Add will panic if `m` is 0/LitNull.
func (*Gini) Assume ¶
Assume causes the solver to make the assumption that m is true in the next call to Solve() or the next call to Test().
Solve() always consumes and forgets untested assumptions. tested assumptions are never forgotten, and may be popped with Untest().
func (*Gini) Copy ¶
Copy makes a copy of the Gini g.
every bit of g is copied except
- Statistics for reporting, which are set to 0 instead of copied
- Control mechanisms for Solve's resulting from GoSolve() so the copied gini can make its own calls to GoSolve() (or Solve()) without affecting the original.
func (*Gini) Deactivate ¶ added in v1.0.2
Deactivate deactivates a literal as returned by Activate. Deactivation frees the literal for future Activations and removes all clauses, including learned clauses, which contain `m.Not()`.
Deactivate is an unsupported operation under a test scope and will panic if called under a test scope.
func (*Gini) GoSolve ¶
GoSolve provides a connection to a single background solving goroutine, a goroutine which calls Solve()
func (*Gini) Lit ¶ added in v0.9.0
Lit produces a fresh variable and returns its positive literal, conforming to inter.Liter.
func (*Gini) Reasons ¶
Reasons give a set of literals which imply m by virtue of a single clause.
Reasons only works if m was returned by some call to Test resulting in SAT or UNKNOWN. Otherwise, Reasons is undefined and may panic.
Additionally, Reasons returns a piece of an acyclic implication graph. The entire graph may be reconstructed by calling Reasons for every propagated literal returned by Test. The underlying graph changes on calls to Test and Solve. If the underlying graph does not change, then Reasons guarantees that it is acyclic.
func (*Gini) Solve ¶
Solve solves the constraints. It returns 1 if sat, -1 if unsat, and 0 if canceled.
func (*Gini) Test ¶
Test tests whether the current assumptions are consistent under BCP and opens a scope for future assumptions.
Test returns the result of BCP res
(1: SAT, -1: UNSAT: 0, UNKNOWN)
And any associated data in out. The data tries to use dst for storage if there is space.
The associated data is
- All assigned literals since last test if SAT or UNKNOWN
- Either the literals of a clause which is unsat under BCP or an assumption which is false under BCP, whichever is found first.
When g is under a test scope, many operations are not possible, in particular: {Add,Activate,ActivateWith,Deactivate} are unsupported operations under a test scope.
func (*Gini) Try ¶ added in v1.0.2
Try solves with a timeout. Try returns
1 if sat -1 if unsat 0 if timeout
func (*Gini) Untest ¶
Untest removes a scope opened and sealed by Test, backtracking and removing assumptions.
Untest returns whether the problem is consistent under BCP after removing assumptions from the last Test. It can happen that a given set of assumptions becomes inconsistent under BCP as the underlying solver learns clauses.
func (*Gini) Value ¶
Value returns the truth value of the literal m. The meaning of the returned value is only defined if the previous call to sat was satisfiable. In this case, the returned value is the value of m in a model of of the underlying problem, where that model is determined by the previous call to Solve().
Source Files
Directories
¶
| Path | Synopsis |
|---|---|
|
Package ax supplies an "assumption eXchange".
|
Package ax supplies an "assumption eXchange". |
|
Package bench provides solver benchmarking utilities.
|
Package bench provides solver benchmarking utilities. |
|
Package cmd houses gini command line tools.
|
Package cmd houses gini command line tools. |
|
bench
Command bench provides benchmarking tools for sat solvers.
|
Command bench provides benchmarking tools for sat solvers. |
|
crispd
Command crispd is a command line CRISP-1.0 server crispd is a CRISP-1.0 server.
|
Command crispd is a command line CRISP-1.0 server crispd is a CRISP-1.0 server. |
|
gini
Package main implements the Gini command.
|
Package main implements the Gini command. |
|
Package crisp provides an implementation (client, server) of the compressed incremental sat protocol (CRISP), version 1.0.
|
Package crisp provides an implementation (client, server) of the compressed incremental sat protocol (CRISP), version 1.0. |
|
Package dimacs provides support for reading dimacs cnf files and variants.
|
Package dimacs provides support for reading dimacs cnf files and variants. |
|
Package gen contains generators for common kinds of formulas.
|
Package gen contains generators for common kinds of formulas. |
|
Package inter contains common gini interfaces and functions to map between them.
|
Package inter contains common gini interfaces and functions to map between them. |
|
net
Package net provides gini/inter interface variants adapted to network communications.
|
Package net provides gini/inter interface variants adapted to network communications. |
|
internal
|
|
|
xo
Package xo is the main gini internal package for (single core) sat solving.
|
Package xo is the main gini internal package for (single core) sat solving. |
|
Package logic provides representation of Boolean combinational and sequential logic.
|
Package logic provides representation of Boolean combinational and sequential logic. |
|
aiger
Package aiger implements aiger format version 1.9 ascii and binary readers and writers.
|
Package aiger implements aiger format version 1.9 ascii and binary readers and writers. |
|
Package z provides minimal common interface to lits and vars.
|
Package z provides minimal common interface to lits and vars. |