Documentation
¶
Overview ¶
Package xo is the main gini internal package for (single core) sat solving.
Sincerest apologies to newcomers, as successfully editing this package for all but simple incidental changes likely requires a fairly deep understanding of CDCL sat solvers; this fact is probablly largely unavoidable.
For an introduction to SAT, see The Handbook of satisfiability.
That said, this solver is organised as follows.
Variables and Literals ¶
Variables (type Var) are uint32, starting at offset 1 ending at 2^30 - 1. Each variable can either have value true or false, represented by sign {+1,-1}, or by an associated literal.
Literals (type Lit) are uint32, starting at 2, ending at 2^31 - 1. Literals are either variables or their negation.
Clauses
Clauses are constraints in the form of disjunctions of literals.
Clauses have a complicated representation for efficiency reasons clauses have an underlying data store, (type CDat in cdat.go), which is one big slice of 32bit values, most of which are Lits. A compact header (32bit, type Chd) contains some metadata for each clause.
- whether the clause is learnt
- the literal block distance of the clause (number of non deterministic branches it spanned when created, if learnt)
- an abstraction of the size of the clause
- "heat", a heuristic score of activity in solving.
Each clause is also associated with a z.C, which is a 32bit offset into the data store slice of lits. This is the identifier for a clause, which can change over time due to clause garbage collection during the solving process.
Each z.C p points to data layed out as follows.
[... Chd lit0 lit1 ... litn LitNull]
p
Solving ¶
Solving is a depth first search over the (exponential) space of variable assignments. As the search takes place the value of the clauses in the assignment stack may imply other values. For example, if we search for an assignment for variables {x,y}, and we guess x=1, and there is a clause (not(x) or not(y)), then not(y) must be part of any extension of the assignment. Identifying such necessary assignment extensions is called (Boolean) constraint propagation / BCP
During BPC, it is possible to find a clause in which every literal is false. Such a clause is called a "conflict". Also the event of identifying such a clause is called a conflict..
Conflicts are resolved by backtracking and choosing a new branch. Additionally, a new clause is derived which prevents the search from arriving at the same partial assignment, irrespective of the order in which the search applies (at least as long as that clause is kept in the solving process...). Such a clause is called a "learnt" clause and the process of adding such clauses is called "learning".
As conflicts are encountered and new clauses are learned, it becomes necessary to remove learned clauses in such a way as to guarantee progress of the search algorithm. This is because lots of clauses can have a high ratio of irrelevant clauses to the future search over time, and the more clauses managed by the solver, the more expensive BCP becomes.
Since BCP is the bottlneck in the algorithm, some balance must be achieved by removing learned clauses. This is where "compaction" or "clause garbage collection" comes into play. This is implemented in cgc.go and is based on some heuristics from the literature.
This depth first search has the following major components, in term of code organisation.
Guess (type Guess, in guess.go) guessing variables and associated values during the search (for example, guessing x=1 in the search above).
Trail manages the assignment stack and propagation of constraints.
Derive learns new clauses whenever the search reaches a point which cannot be extended because some clause is false. The new clauses prune the future search space more than just backtracking.
Constraint propagation ¶
Constraint propagation is the most optimised and difficult to manage part of the code. It uses "watch lists", which associates 2 literals with every clause (except 1 literal clauses). Whenever one of those literals is falsified in the search, the clause is examined to see whether or not it implies a new value for a variable or if it is false.
Important Heuristics ¶
Variable ordering in Guess is extremely important to solving time. Variables are re-ordered dynamically according to an approximation of their proximity to/involvement with conflicts
Clause Garbage Collection is also extremely important. We use a hyper-aggressive strategy which multiplexes the CGC frequency using the luby series and removes approximately half of the learnted clauses in each CGC.
Variable naming ¶
Gini uses regular succint variable naming where possible to aid in readability and succintness
- Lit; m,n,o
- Var: u,v
- z.C: p,q,r
- Watch: w -
- Slices ([]): add an s on the end of underlying type
- Slice indices: i,j,k
- Chd: h
Index ¶
- Constants
- type Active
- type CDat
- func (c *CDat) AddLits(hdr Chd, ms []z.Lit) z.C
- func (c *CDat) Bump(p z.C) bool
- func (c *CDat) Chd(loc z.C) Chd
- func (c *CDat) Compact(rm []z.C) (map[z.C]z.C, int)
- func (c *CDat) CompactReady(nc, nl int) bool
- func (c *CDat) Copy() *CDat
- func (c *CDat) CopyTo(other *CDat)
- func (c *CDat) Decay()
- func (c *CDat) Dimacs(w io.Writer) error
- func (c *CDat) Forall(f func(i int, p z.C, ms []z.Lit))
- func (c *CDat) Load(p z.C, ms []z.Lit) []z.Lit
- func (c *CDat) Next(loc z.C) z.C
- func (c *CDat) SetChd(loc z.C, hd Chd)
- func (c *CDat) String() string
- type Cdb
- func (c *Cdb) Add(m z.Lit) (z.C, z.Lit)
- func (c *Cdb) Bump(p z.C)
- func (c *Cdb) Chd(p z.C) Chd
- func (c *Cdb) CheckModel() []error
- func (c *Cdb) CheckWatches() []error
- func (c *Cdb) CopyWith(ov *Vars) *Cdb
- func (c *Cdb) Decay()
- func (c *Cdb) Forall(f func(p z.C, h Chd, ms []z.Lit))
- func (c *Cdb) ForallAdded(f func(p z.C, h Chd, ms []z.Lit))
- func (c *Cdb) ForallLearnts(f func(p z.C, h Chd, ms []z.Lit))
- func (c *Cdb) ForallSlice(f func(p z.C, h Chd, ms []z.Lit), ps []z.C)
- func (c *Cdb) InUse(o z.C) bool
- func (c *Cdb) IsBinary(p z.C) bool
- func (c *Cdb) IsUnit(p z.C) bool
- func (c *Cdb) Learn(ms []z.Lit, lbd int) z.C
- func (c *Cdb) Lits(p z.C, ms []z.Lit) []z.Lit
- func (c *Cdb) MaybeCompact() (int, int, int)
- func (c *Cdb) Remove(cs ...z.C)
- func (c *Cdb) SetTracer(t Tracer)
- func (c *Cdb) Size(p z.C) int
- func (c *Cdb) String() string
- func (c *Cdb) Unlink(rms []z.C)
- func (c *Cdb) Write(w io.Writer) error
- type Cgc
- type Chd
- type Ctl
- type Derived
- type Deriver
- type DimacsVis
- type Guess
- type Luby
- type S
- func (s *S) Activate() z.Lit
- func (s *S) ActivateWith(act z.Lit)
- func (s *S) ActivationLit() z.Lit
- func (s *S) Add(m z.Lit)
- func (s *S) Assume(ms ...z.Lit)
- func (s *S) Copy() *S
- func (s *S) Deactivate(m z.Lit)
- func (s *S) GoSolve() inter.Solve
- func (s *S) Lit() z.Lit
- func (s *S) MaxVar() z.Var
- func (s *S) ReadStats(st *Stats)
- func (s *S) Reasons(dst []z.Lit, m z.Lit) []z.Lit
- func (s *S) SCopy() inter.S
- func (s *S) Solve() int
- func (s *S) String() string
- func (s *S) Test(ms []z.Lit) (res int, ns []z.Lit)
- func (s *S) Try(dur time.Duration) int
- func (s *S) Untest() int
- func (s *S) Value(m z.Lit) bool
- func (s *S) Who() string
- func (s *S) Why(ms []z.Lit) []z.Lit
- type Stats
- type StatsResult
- type Tracer
- type Trail
- type Vars
- type Watch
Constants ¶
const ( CNull z.C = 0 CInf = 0xffffffff )
const ( // for each Solve() call don't restart until this many conflicts. // good for incremental solving. RestartAfter uint = 1000 RestartFactor = 768 PropTick int64 = 20000 CancelTicks int64 = 1 )
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type CDat ¶
type CDat struct {
D []z.Lit // contains Chds as well, same underlying type
Len int
Cap int
ClsLen int
// contains filtered or unexported fields
}
Type CDat: basic operations for storing all the literals (and Chds) in a CNF
func NewCDat ¶
The Layout is as follows
Each clause is indexed by a z.C, which is a uint32 index into CDat.D. The location is the beginning of the list of literals in the clause, which is terminated by z.LitNull. Each location is preceded by a Chd giving clause metadata. Since the underlying type of Chd and z.Lit are uint32, this is fine. Rather than allocate lots of bits in the Chd to the size, we only allocate 5 bits (max size of 31). For each actual size s, we store s & 31 To find the end of a clause at a given location, we iterate through the possible sizes with the same modulus, which is usually 1 operation.
func (*CDat) AddLits ¶
func AddLits adds literals to the underlying data. The clause header hdr must be consistent.
func (*CDat) Compact ¶
Compact the storage by removing clauses with locations in rm pre: rm is sorted in ascending z.C order
this just compacts the data and returns a map of the locations which need to be remapped in higher level data structures (watch lists, etc).
the returned map behaves as follows:
1. remap every removed clause in rm to CNull 2. remap every moved clause
func (*CDat) CompactReady ¶
ComactReady returns whether a compaction of the data is ready.
type Cdb ¶
type Cdb struct {
Vars *Vars
Active *Active
CDat CDat
AddLits []z.Lit
AddVals []int8
Bot z.C
Added []z.C
Learnts []z.C
Tracer Tracer
// contains filtered or unexported fields
}
Type Cdb is the main interface to clauses.
func (*Cdb) CheckModel ¶
by default, called when sat as a sanity check.
func (*Cdb) CheckWatches ¶
Debug self check code, not used in any production entrypoint.
func (*Cdb) CopyWith ¶
NB also Active is copied in S.Copy and placed in resulting copied cdb, so we don't copy Active here.
type Cgc ¶
type Cgc struct {
// contains filtered or unexported fields
}
Type Cgc encapsulates clause compaction/garbage collection.
This is separate from, and sometimes calls CDat compaction which is another issue.
func (*Cgc) Compact ¶
Compact runs a clause gc, which in turn sometimes compacts the underlying CDat. Compact returns
(num clauses removed, num clauses cdat removed, num freed uint32s)
func (*Cgc) CompactCDat ¶
NB this is only from cgc.Compact
type Ctl ¶
type Ctl struct {
// contains filtered or unexported fields
}
Type Ctl encapsulates low level asynchronous control over a Solve. Ctl is used to implement inter.S and concur.U and concur.S
func (*Ctl) Pause ¶
Pause tries to pause the underlying Solve(). If not sucessfule, it returns the result of Solve() together with false. If successful, it returns (0, true).
When successful, Pause should always be followed by Unpause before any other usage of c. Pause is not re-entrant, Pausing a paused Solve will block indefinitely. This is in line with the not-safe for multiple goroutines nature of the Solve API.
func (*Ctl) Stop ¶
Stop stops the current call to solve and returns the solve result.
Stop should not be called more than once, and if it is called, then Test should not be called subsequently.
func (*Ctl) Test ¶
Test tests whether a result is a available and returns it together with whether the underlying Solve() has terminated. Test returns
- 1 for SAT
- -1 for UNSAT
- 0 for UNKNOWN
func (*Ctl) Tick ¶
Tick checks if the solver must stop or pause and if it must stop, it stops it and returns false otherwise, if the solver was paused, then tick blocks until unpause and returns true otherwise it just returns true.
func (*Ctl) Try ¶
Try tries to get the result within d time, returning 0 by default if no result is available within d time.
func (*Ctl) TryStats ¶
func (c *Ctl) TryStats(timeout, stFreq time.Duration) <-chan StatsResult
TryStats outputs stats and result for at most timeout duration with stat requests occuring every stFreq.
type Deriver ¶
type DimacsVis ¶
type DimacsVis struct {
// contains filtered or unexported fields
}
Type DimacsVis implements dimacs.Vis for constructing solvers from dimacs cnf files.
type Guess ¶
type Guess struct {
// contains filtered or unexported fields
}
func NewGuessCdb ¶
type S ¶
type S struct {
Vars *Vars
Cdb *Cdb
Trail *Trail
Guess *Guess
Driver *Deriver
Active *Active
// contains filtered or unexported fields
}
Solver implements a CDCL like solver with some performance bells and whistles
func NewSDimacs ¶
NewSDimacs creates a new S from a dimacs file.
func NewSVc ¶
NewSVc creates a new solver using specified capacity hints for number of variables (vCapHint) and number of clauses (cCapHint).
func (*S) ActivateWith ¶ added in v1.1.0
func (*S) ActivationLit ¶ added in v1.1.0
func (*S) Assume ¶
Assume causes the solver to Assume the literal m to be true for the next call to Solve() or Test().
This may be called multiple times, indicating to make multiple assumptions. The assumptions hold for the next call to Solve() or Test(). Afterwards, if the result is unsat, then s.Why() gives a subset of inconsistent assumptions.
When used with sequences of Test/Untest and Solves, S makes a distinction between tested and untested assumptions. Solve always forgets/consumes untested assumptions; but Solve never forgets/consumes tested assumptions. Forgetting tested assumptions is accomplished with s.Untest().
func (*S) Deactivate ¶ added in v1.1.0
func (*S) ReadStats ¶
ReadStats reads data from the solver into st. The solver values are reset if they are cumulative. The duration and start time attributes of st are not touched.
func (*S) Reasons ¶
Reasons returns the Reasons for a propagated literal returned from test.
Reasons takes 2 arguments,
dst a z.Lit slice in which to place the reasons m the literal for which to supply reasons.
Reasons returns the reasons for m appended to dst.
If m is not a propagated literal returned from Test() (without Untest() in between), the result is undefined and may panic.
func (*S) Solve ¶
Method Solve solves the problem added to the solver under assumptions specified by Assume.
Solve returns -1 if unsat and 1 if sat
func (*S) Test ¶
Test checks if the solver is consistent under unit propagation for the current assumptions and clauses and Test opens a scope for subsequent assumptions. Test takes one argument, which is a slice of literals in which to put propagated literals or failed assumptions.
Test returns a pair
(res, ns)
where
- If res == 1, then the problem is SAT and a full model is found.
- If res == 0, then the problem is unknown (but consistent under unit propagation).
- If res == -1 then the problem is UNSAT.
Additionally if ns is not nil, then
- If res in {0,1}, then ns contains all literals assigned under BCP since last Test(), including assumptions.
- If res = -1, then ns contains the literals in a clause which is false under unit propagation, or an assumed false literal, whichever we happen upon first. (This is distinct from Why which gives failed literals).
- ns is stored in ms if possible
Test operates under the following caveat.
If Test() or Solve() returns unsat, then Test() should not be called subsequently until Untest() is called and returns 0. Note That it can be that Untest() will never return 0 if the problem is unsat without assumptions.
If this does not hold, Test panics.
func (*S) Untest ¶
Untest removes assumptions since last test and returns -1 if the solver is inconsistent under unit propagation after removing assumptions, 0 otherwise. If Untest is called and there is no corresponding Test(), then Untest panics.
Note that when interleaving Solve,Test,and Untest, the following sequences are possible:
Assume(A1) Test() -> 0, [] Assume(A2) Test() -> 0 Assume(A3) Solve() -1 Untest() -> -1, [] // problem is unsat with A1 and A2 Untest() -> -1, [] // problem is unsat with A1 under BCP, even though it wasn't before Assume(A1) Test() -> 0, [...] Solve() -> -1 // unsat under A1 Untest() -> 0 Assume(A2) -> Test() -> 1 // sat under A2 Untest() -> 0 Assume(A1) Test() -> -1, [] // problem is unsat with A1 under BCP, even though it wasn't before
type Stats ¶
type Stats struct {
Start time.Time
Dur time.Duration
Vars int
Added int64
AddedLits int64
AddedUnits int64
AddedBinary int64
AddedTernary int64
Props int64
Sat int64
Unsat int64
Ended int64
Assumptions int64
Failed int64
Guesses int64
GuessRescales int64
Conflicts int64
Learnts int
LearntLits int64
MinLits int64
Restarts int64
Compactions int64
Removed int64
RemovedLits int64
CDatGcs int64
CHeatRescales int64
AddedBig int64
MaxTrail int
Pinned int
IncPinned int
}
func (*Stats) Accumulate ¶
type StatsResult ¶
Type StatsResult encapsulates a pair of stats and a solve result.
type Trail ¶
type Vars ¶
type Watch ¶
type Watch uint64
Watch holds other blocking literal, clause location ( and 1 bit for whether binary
func MakeWatch ¶
MakeWatch creates a watch object for clause location loc blocking literal o, and isBin indicating whether the referred to clause is binary (comprised of 2 literals)
Source Files