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().
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. |