Documentation
¶
Overview ¶
Package solver implements a general-purpose solver for boolean constraint satisfiability problems.
Index ¶
- Variables
- type AppliedConstraint
- type Constraint
- type DefaultTracer
- type DuplicateIdentifier
- type Identifier
- type LitMapping
- func (d *LitMapping) AddConstraints(g inter.S)
- func (d *LitMapping) AnchorIdentifiers() []Identifier
- func (d *LitMapping) AssumeConstraints(s inter.S)
- func (d *LitMapping) CardinalityConstrainer(g inter.Adder, ms []z.Lit) *logic.CardSort
- func (d *LitMapping) Conflicts(g inter.Assumable) []AppliedConstraint
- func (d *LitMapping) ConstraintOf(m z.Lit) AppliedConstraint
- func (d *LitMapping) Error() error
- func (d *LitMapping) LitOf(id Identifier) z.Lit
- func (d *LitMapping) Lits(dst []z.Lit) []z.Lit
- func (d *LitMapping) VariableOf(m z.Lit) Variable
- func (d *LitMapping) Variables(g inter.S) []Variable
- type LoggingTracer
- type NotSatisfiable
- type Option
- type SearchPosition
- type Solver
- type Tracer
- type Variable
Constants ¶
This section is empty.
Variables ¶
var ErrIncomplete = errors.New("cancelled before a solution could be found")
Functions ¶
This section is empty.
Types ¶
type AppliedConstraint ¶
type AppliedConstraint struct {
Variable Variable
Constraint Constraint
}
AppliedConstraint values compose a single Constraint with the Variable it applies to.
type Constraint ¶
type Constraint interface {
String(subject Identifier) string
Apply(c *logic.C, lm *LitMapping, subject Identifier) z.Lit
Order() []Identifier
Anchor() bool
}
Constraint implementations limit the circumstances under which a particular Variable can appear in a solution.
func AtMost ¶
func AtMost(n int, ids ...Identifier) Constraint
AtMost returns a Constraint that forbids solutions that contain more than n of the Variables identified by the given Identifiers.
func Conflict ¶
func Conflict(id Identifier) Constraint
Conflict returns a Constraint that will permit solutions containing either the constrained Variable, the Variable identified by the given Identifier, or neither, but not both.
func Dependency ¶
func Dependency(ids ...Identifier) Constraint
Dependency returns a Constraint that will only permit solutions containing a given Variable on the condition that at least one of the Variables identified by the given Identifiers also appears in the solution. Identifiers appearing earlier in the argument list have higher preference than those appearing later.
func Mandatory ¶
func Mandatory() Constraint
Mandatory returns a Constraint that will permit only solutions that contain a particular Variable.
func Prohibited ¶
func Prohibited() Constraint
Prohibited returns a Constraint that will reject any solution that contains a particular Variable. Callers may also decide to omit an Variable from input to Solve rather than Apply such a Constraint.
type DefaultTracer ¶
type DefaultTracer struct{}
type DuplicateIdentifier ¶
type DuplicateIdentifier Identifier
type Identifier ¶
type Identifier string
Identifier values uniquely identify particular Variables within the input to a single call to Solve.
func IdentifierFromString ¶
func IdentifierFromString(s string) Identifier
IdentifierFromString returns an Identifier based on a provided string.
type LitMapping ¶
type LitMapping struct {
// contains filtered or unexported fields
}
LitMapping performs translation between the input and output types of Solve (Constraints, Variables, etc.) and the variables that appear in the SAT formula.
func (*LitMapping) AddConstraints ¶
func (d *LitMapping) AddConstraints(g inter.S)
AddConstraints adds the current constraints encoded in the embedded circuit to the solver g
func (*LitMapping) AnchorIdentifiers ¶
func (d *LitMapping) AnchorIdentifiers() []Identifier
AnchorIdentifiers returns a slice containing the Identifiers of every Variable with at least one "Anchor" constraint, in the Order they appear in the input.
func (*LitMapping) AssumeConstraints ¶
func (d *LitMapping) AssumeConstraints(s inter.S)
func (*LitMapping) CardinalityConstrainer ¶
func (d *LitMapping) CardinalityConstrainer(g inter.Adder, ms []z.Lit) *logic.CardSort
CardinalityConstrainer constructs a sorting network to provide cardinality constraints over the provided slice of literals. Any new clauses and variables are translated to CNF and taught to the given inter.Adder, so this function will panic if it is in a test context.
func (*LitMapping) Conflicts ¶
func (d *LitMapping) Conflicts(g inter.Assumable) []AppliedConstraint
func (*LitMapping) ConstraintOf ¶
func (d *LitMapping) ConstraintOf(m z.Lit) AppliedConstraint
ConstraintOf returns the constraint application corresponding to the provided literal, or a zeroConstraint if no such constraint exists.
func (*LitMapping) Error ¶
func (d *LitMapping) Error() error
Error returns a single error value that is an aggregation of all errors encountered during a LitMapping's lifetime, or nil if there have been no errors. A non-nil return value likely indicates a problem with the solver or constraint implementations.
func (*LitMapping) LitOf ¶
func (d *LitMapping) LitOf(id Identifier) z.Lit
LitOf returns the positive literal corresponding to the Variable with the given Identifier.
func (*LitMapping) VariableOf ¶
func (d *LitMapping) VariableOf(m z.Lit) Variable
VariableOf returns the Variable corresponding to the provided literal, or a zeroVariable if no such Variable exists.
type LoggingTracer ¶
type LoggingTracer struct {
Writer io.Writer
}
type NotSatisfiable ¶
type NotSatisfiable []AppliedConstraint
NotSatisfiable is an error composed of a minimal set of applied constraints that is sufficient to make a solution impossible.
type SearchPosition ¶
type SearchPosition interface {
Variables() []Variable
Conflicts() []AppliedConstraint
}
type Variable ¶
type Variable interface {
// Identifier returns the Identifier that uniquely identifies
// this Variable among all other Variables in a given
// problem.
Identifier() Identifier
// Constraints returns the set of constraints that Apply to
// this Variable.
Constraints() []Constraint
}
Variable values are the basic unit of problems and solutions understood by this package.
Source Files