gini

README

Gini SAT Solver

The Gini sat solver is a fast, clean SAT solver written in go.

Google Group

This solver is fully open source, originally developped at IRI France.

Build/Install

For the impatient who don't mind adding noisy directory structures to package developers lives:

go get github.com/irifrance/gini...

I recommend however building the package github.com/irifrance/gini/internal/xo with bounds checking turned off. This package is all about anything-goes performance and is the workhorse behing 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.

The SAT Problem

The SAT problem is perhaps the most famous NP-complete problem. As such, SAT solvers can be used to try to solve hard problems, such as travelling salesman or RSA cracking. In practice, many SAT problems are quite easy (but not decryption problems...yet). The solvers are used in software verification, hardware verification and testing, AI planning, routing, etc.

The SAT problem is a Boolean problem. All variables can either be true or false, but nothing else. The SAT problem solves systems of Boolean constraints, called clauses. Namely, SAT solvers work on conjunctive normal form problems (CNFs). There are many ways to efficiently code arbitrary logic into CNF, so this is not so much a restricting factor.

CNF

A CNF is a conjunction of clauses

c1 and c2 and ... and cM

Each c[i], i in [1..M], is a clause, which is of the form

m1 or m2 or ... or mN

where each m[i], i in [1..N] is either a Boolean variable (such as x), or the negation of a Boolean variable (such as not(y)). An expression which is either a Boolean variable or its negation is called a "literal".

In the following, we refer to variables simply by integers 1,2,3,...

Clauses are often written in succint form

-3 11 12 14 -257

Numerical negation indicates logical negation, and spaces are disjunctions "or". Sometimes "+" is used for "or".

Conjunctions are just concatenation of clauses. We can parenthesize clauses such as

(1 -2) (2 -3) (3 -4) (4 -1)

which expresses a set of clauses whose satisfying assignments are

{1,2,3,4}
    or
{-1,-2,-3,-4}

Models

A model of a CNF is a value for each of the variables which makes every clause in the CNF true. The SAT problem is determining whether or not a model exists for a given set of clauses.

Proofs

Resolution

Resolution is a form of logical reasoning with conjunctions of clauses. Given 2 clauses of the form

C + v

and

D + -v

We can conclude that

C + D

must be true.

Here, C and D are arbitrary clauses.

Resolution proof of unsatisfiability is a derivation of the empty disjuction (false) by means of resolution. Resolution proofs, even minimally sized ones, can be very large, exponentially larger than the innput problem.

Modern SAT solvers mostly rely on performing operations which correspond to bounded size (in terms of number of variables) number of resolutions. Given this fact together with the fact that the minimal proofs can be exponentially large in the number of variables, some problems can take an exponential amount of time.

Nonetheless, many SAT solvers have heuristics and are optimised so much that even hard problems become tractable. With up to several tens of millions of resolutions happening per second on one modern single core CPU, even problems with known exponential bounds on resolution steps can be solved.

Solving Formulas and Circuits

Gini provides a simple and efficient logic modelling library which supports easy construction of arbitrary Boolean formulas. The library uses and-inverter graphs, structural hashing, constant propagation and can be used for constructing compact formulas with a rich set of Boolean operators. The circuit type implements an interface which makes it plug into a solver automatically. In fact, the circuit type uses the same representation for literals as the solver, so there is no need to map between solver and circuit variables.

Additionally, sequential circuits are supported. The sequential part of the logic library provides memory elements (latches) which are evaluated initially as inputs and take a "next" value which provides input to the next cycle of the circuit. The library supports unrolling sequential circuits for a fixed number of cycles to arrive at a non-sequential formula which can then be checked for satisfiability using solving tools.

Gini also supports cardinality constraints which can constrain how many of a set of Boolean variables are true. Cardinality constraints in turn provide an easy means of doing optimisation. Gini uses sorting networks to code cardinality constraints into clauses. Sorting networks are a good general purpose means of handling cardinality constraints in a problem context which also contains lots of purely Boolean logic (implicitly or not).

Most SAT use cases use a front end for modelling arbitrary formulas. When formats are needed for interchange, Gini supports the following.

Aiger

Gini supports aiger version 1.9 in conjunction with its logic library. The logic.C and logic.S circuit types can be stored, exchanged, read and written in aiger ascii and binary formats.

Dimacs

CNF Dimacs files, which are an ancient widely used format for representing CNF formulas. Dimacs files are usually used for benchmarking solvers, to eliminate the formula representation layer. The fact that the format is more or less universally supported amongst SAT solvers leads some SAT users to use this format, even though there is I/O, CNF translation, and parsing overhead by comparison to using a logic library.

Optimisation

With Cardinality constraints, optimisation is easy

import "github.com/irifrance/gini"
import "github.com/irifrance/gini/logic"

s := gini.New()
c := logic.NewC()


// suppose we encode package dependency constraints in the circuit c
// and we have a slice of packages each of which has a literal
// associated with whether or not multiple versions are needed in a 
// build

multiVersions := make([]z.Lit, 1<<23)
for _, p := range pkgs {
    multiVersions = append(multiVersions, p.needsMulti)
}

// make a cardinality constraints object
cards := logic.NewCardSort(multiVersions, s)

// loop through the constraints (note a linear search
// can be faster in this case because the underlying solver
// often has locality of logic cache w.r.t. cardinality constraints)
minMultiVersions := -1
for i := range multiVersions {
    s.Assume(cards.Leq(i))
    if s.Solve() == 1 {
        minMultiVersions = i
        break
    }
}

// use the model from s to propose a build

Performance

In applications, SAT problems normally have an exponential tail runtime distribution with a strong bias towards bigger problems populating the longer runtime part of the distribution. So in practice, a good rule of thumb is 1 in N problems will on average take longer than time alotted to solve it for a problem of a given size, and then one measures N experimentally. Very often, despite the NP nature of SAT, an application can be designed to use a SAT solver in a way that problems almost never take too long. Additionally, the hardest known hand-crafted problems for CDCL solvers which take significant time involve at least a few hundred variables. So if you're application has only a few hundred variables, you're probably not going to have any performance problems at all with any solver.

As in almost every solver, the core CDCL solver in Gini is the workhorse and is a good general purpose solver. Some specific applications do benefit from pre- or in-processing, and some some applications may not be useable with such techniques. Other solvers provide more and better pre- or in-processing than Gini and help is welcome in adding such solving techniques to Gini.

The core CDCL solver in Gini has been compared with that in MiniSAT and PicoSAT, two standard such solvers on randomly chosen SAT competition problems. In this evaluation, Gini out performed PicoSAT and was neck-in-neck with MiniSAT. The core CDCL solver in Gini also measures up to PicoSAT and MiniSAT in terms of "propagations per second", indicating the core routines are themselves competitive with these solvers, not only the heuristics. This level of performance has not to our knowledge been achieved by other sat solvers in Go, such as go-sat or gophersat.

While the above evaluation casts a fairly wide net over application domains and problem difficulty, the performance of sat solvers and underlying algorithms are fundamentally hard to predict in any rigorous way. So your experience may differ, but we are confident Gini's core solver is a well positioned alternative to standard high-performance CDCL solvers in C/C++. We encourage you to give it a try and welcome any comparisons.

Concurrency

Gini is written in Go and uses several goroutines by default for garbage collection and system call scheduling. There is a "core" single-goroutine solver, xo, which is in an internal package for gutsy low level SAT hackers.

Connections to solving processes

Gini provides safe connections to solving processes which are guaranteed to not lose any solution found, can pause and resume, run with a timeout, test without solving, etc.

Solve-time copyable solvers.

Gini provides copyable solvers, which can be safely copied at solvetime during a pause.

Ax

Gini provides an "Assumption eXchange" package for deploying solves under different sets of assumptions to the same set of underlying constraints in parallel. This can give linear speed up in tasks, such as PDR/IC3, which generate lots of assumptions.

Distributed and CRISP

Gini provides a definition and reference implementation for CRISP-1.0, the compressed incremental SAT protocol. The protocol is a client-server wire protocol which can dispatch an incremental sat solver with very little overhead as compared to direct API calls. The advantage of using a protocol is that it allows arbitrary tools to implement the solving on arbitrary hardware without affecting the client.

Many SAT applications are incremental and easily solve huge numbers of problems while only a few problems are hard. CRISP facilitates pulling out the big guns for the hard problems while not affecting performance for easy problems. Big guns tend to be harder to integrate into applications because of compilation issues, hardware requirements, size and complexity of the code base, etc. Applications that use CRISP can truly isolate themselves from the woes of integrating big guns while benefiting on hard problems.

CRISP also allows language independent incremental SAT solving. The applications and solvers can be readily implemented without the headache of synchronizing programming language, compilers, or coding style.

We are planning on implementing some CRISP extensions, namely the multiplexing interface which will enable (possibly remote) clients to control programmatically partitioning or queuing of related SAT problems.

The CRISP protocol provides a basis for distributed solving. Gini implements a CRISP-1.0 client and server.

A command, crispd, is supplied for the CRISP server.

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 New() *Gini
  • func NewDimacs(r io.Reader) (*Gini, error)
  • func NewV(capHint int) *Gini
  • func NewVc(vCapHint, cCapHint int) *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

Functions

func NewS

func NewS() inter.S

NewS creates a new solver, which is the Gini implementation of inter.S.

func NewSv

func NewSv() inter.Sv

NewSv creates an Sv implementation

func NewSvVars

func NewSvVars(vs *z.Vars) inter.Sv

NewSvVars creates an Sv implementation with the specified set of vars.

Types

type Gini

type Gini struct {
	// contains filtered or unexported fields
}

Gini is a concrete implementation of solver

func New

func New() *Gini

New creates a new gini solver.

func NewDimacs

func NewDimacs(r io.Reader) (*Gini, error)

NewDimacs create a new gini solver from dimacs formatted input.

func NewV

func NewV(capHint int) *Gini

NewV creates a new Gini solver with hint for capacity of variables set to capHint.

func NewVc

func NewVc(vCapHint, cCapHint int) *Gini

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

func (g *Gini) Add(m z.Lit)

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

func (g *Gini) Assume(ms ...z.Lit)

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

func (g *Gini) Copy() *Gini

Copy makes a copy of the Gini g.

every bit of g is copied except

1. Statistics for reporting, which are set to 0 instead of copied
2. 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

func (g *Gini) GoSolve() inter.Solve

GoSolve provides a connection to a single background solving goroutine, a goroutine which calls Solve()

func (*Gini) Lit

func (g *Gini) Lit() z.Lit

Var produces a fresh variable.

func (*Gini) MaxVar

func (g *Gini) MaxVar() z.Var

MaxVar returns the variable whose id is max.

func (*Gini) Reasons

func (g *Gini) Reasons(dst []z.Lit, m z.Lit) []z.Lit

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) SCopy

func (g *Gini) SCopy() inter.S

SCopy implements inter.S

func (*Gini) Solve

func (g *Gini) Solve() int

Solve solves the constraints. It returns 1 if sat, -1 if unsat, and 0 if canceled.

func (*Gini) Test

func (g *Gini) Test(dst []z.Lit) (res int, out []z.Lit)

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

func (g *Gini) Untest() int

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

func (g *Gini) Value(m z.Lit) bool

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

func (*Gini) Why

func (g *Gini) Why(ms []z.Lit) []z.Lit

Why returns the slice of failed assumptions, a minimized set of assumptions which are sufficient for the last UNSAT result (from a call to Test() or Solve()).

Why tries to store the failed assumptions in ms, if there is sufficient space.