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
Index ¶
- Constants
- func NewS() inter.S
- func NewSv() inter.Sv
- func NewSvVars(vs *z.Vars) inter.Sv
- type Gini
- func (g *Gini) Add(m z.Lit)
- func (g *Gini) Assume(ms ...z.Lit)
- func (g *Gini) Copy() *Gini
- 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) Untest() int
- func (g *Gini) Value(m z.Lit) bool
- func (g *Gini) Why(ms []z.Lit) []z.Lit
Constants ¶
const Version = "1.0a"
The version of gini
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) 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)
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) GoSolve ¶
GoSolve provides a connection to a single background solving goroutine, a goroutine which calls Solve()
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.
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
Command bench provides benchmarking tools for sat solvers.
|
Command bench provides benchmarking tools for sat solvers. |
crispd
command
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
command
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. |