gophersat: github.com/crillab/gophersat/solver Index | Examples | Files

package solver

import "github.com/crillab/gophersat/solver"

Package solver gives access to a simple SAT and pseudo-boolean solver. Its input can be either a DIMACS CNF file, a PBS file or a solver.Problem object, containing the set of clauses to be solved. In the last case, the problem can be either a set of propositional clauses, or a set of pseudo-boolean constraints.

No matter the input format, the solver.Solver will then solve the problem and indicate whether the problem is satisfiable or not. In the former case, it will be able to provide a model, i.e a set of bindings for all variables that makes the problem true.

Describing a problem

A problem can be described in several ways:

1. parse a DIMACS stream (io.Reader). If the io.Reader produces the following content:

p cnf 6 7
1 2 3 0
4 5 6 0
-1 -4 0
-2 -5 0
-3 -6 0
-1 -3 0
-4 -6 0

the programmer can create the Problem by doing:

pb, err := solver.ParseCNF(f)

2. create the equivalent list of list of literals. The problem above can be created programatically this way:

clauses := [][]int{
    []int{1, 2, 3},
    []int{4, 5, 6},
    []int{-1, -4},
    []int{-2, -5},
    []int{-3, -6},
    []int{-1, -3},
    []int{-4, -6},
}
pb := solver.ParseSlice(clauses)

3. create a list of cardinality constraints (CardConstr), if the problem to be solved is better represented this way. For instance, the problem stating that at least two literals must be true among the literals 1, 2, 3 and 4 could be described as a set of clauses:

clauses := [][]int{
    []int{1, 2, 3},
    []int{2, 3, 4},
    []int{1, 2, 4},
    []int{1, 3, 4},
}
pb := solver.ParseSlice(clauses)

The number of clauses necessary to describe such a constrain can grow exponentially. Alternatively, it is possible to describe the same this way:

constrs := []CardConstr{
    {Lits: []int{1, 2, 3, 4}, AtLeast: 2},
}
pb := solver.ParseCardConstrs(clauses)

Note that a propositional clause has an implicit cardinality constraint of 1, since at least one of its literals must be true.

4. parse a PBS stream (io.Reader). If the io.Reader contains the following problem:

2 ~x1 +1 x2 +1 x3 >= 3 ;

the programmer can create the Problem by doing:

pb, err := solver.ParsePBS(f)

5. create a list of PBConstr. For instance, the following set of one PBConstrs will generate the same problem as above:

constrs := []PBConstr{GtEq([]int{1, 2, 3}, []int{2, 1, 1}, 3)}
pb := solver.ParsePBConstrs(constrs)

Solving a problem

To solve a problem, one simply creates a solver with said problem. The solve() method then solves the problem and returns the corresponding status: Sat or Unsat.

s := solver.New(pb)
status := s.Solve()

If the status was Sat, the programmer can ask for a model, i.e an assignment that makes all the clauses of the problem true:

m := s.Model()

For the above problem, the status will be Sat and the model can be {false, true, false, true, false, false}.

Alternatively, one can display on stdout the result and model (if any):

s.OutputModel()

For the above problem described in the DIMACS format, the output can be:

SATISFIABLE
-1 2 -3 4 -5 -6

Index

Examples

Package Files

card.go clause.go clause_alloc.go doc.go interface.go lbd.go learn.go parser.go parser_pb.go pb.go preprocess.go problem.go queue.go solver.go sort.go types.go watcher.go

Constants

const (
    // Indet means the problem is not proven sat or unsat yet.
    Indet = Status(iota)
    // Sat means the problem or clause is satisfied.
    Sat
    // Unsat means the problem or clause is unsatisfied.
    Unsat
    // Unit is a constant meaning the clause contains only one unassigned literal.
    Unit
    // Many is a constant meaning the clause contains at least 2 unassigned literals.
    Many
)

type CardConstr Uses

type CardConstr struct {
    Lits    []int
    AtLeast int
}

A CardConstr is a cardinality constraint, i.e a set of literals (represented with integer variables) associated with a minimal number of literals that must be true. A propositional clause (i.e a disjunction of literals) is a cardinality constraint with a minimal cardinality of 1.

func AtLeast1 Uses

func AtLeast1(lits ...int) CardConstr

AtLeast1 returns a cardinality constraint stating that at least one of the given lits must be true. This is the equivalent of a propositional clause.

func AtMost1 Uses

func AtMost1(lits ...int) CardConstr

AtMost1 returns a cardinality constraint stating that at most one of the given lits can be true.

func Exactly1 Uses

func Exactly1(lits ...int) []CardConstr

Exactly1 returns two cardinality constraints stating that exactly one of the given lits must be true.

type Clause Uses

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

A Clause is a list of Lit, associated with possible data (for learned clauses).

func NewCardClause Uses

func NewCardClause(lits []Lit, card int) *Clause

NewCardClause returns a clause whose lits are given as an argument and for which at least 'card' literals must be true. Note tha NewClause(lits) is equivalent to NewCardClause(lits, 1).

func NewClause Uses

func NewClause(lits []Lit) *Clause

NewClause returns a clause whose lits are given as an argument.

func NewLearnedClause Uses

func NewLearnedClause(lits []Lit) *Clause

NewLearnedClause returns a new clause marked as learned.

func NewPBClause Uses

func NewPBClause(lits []Lit, weights []int, card int) *Clause

NewPBClause returns a pseudo-boolean clause with the given lits, weights and minimal cardinality.

func (*Clause) CNF Uses

func (c *Clause) CNF() string

CNF returns a DIMACS CNF representation of the clause.

func (*Clause) Cardinality Uses

func (c *Clause) Cardinality() int

Cardinality returns the minimum number of literals that must be true to satisfy the clause.

func (*Clause) First Uses

func (c *Clause) First() Lit

First returns the first lit from the clause.

func (*Clause) Get Uses

func (c *Clause) Get(i int) Lit

Get returns the ith literal from the clause.

func (*Clause) Learned Uses

func (c *Clause) Learned() bool

Learned returns true iff c was a learned clause.

func (*Clause) Len Uses

func (c *Clause) Len() int

Len returns the nb of lits in the clause.

func (*Clause) PBString Uses

func (c *Clause) PBString() string

PBString returns a string representation of c as a pseudo-boolean expression.

func (*Clause) PseudoBoolean Uses

func (c *Clause) PseudoBoolean() bool

PseudoBoolean returns true iff c is a pseudo boolean constraint, and not just a propositional clause or cardinality constraint.

func (*Clause) Second Uses

func (c *Clause) Second() Lit

Second returns the second lit from the clause.

func (*Clause) Set Uses

func (c *Clause) Set(i int, l Lit)

Set sets the ith literal of the clause.

func (*Clause) Shrink Uses

func (c *Clause) Shrink(newLen int)

Shrink reduces the length of the clauses, by removing all lits starting from position newLen.

func (*Clause) Weight Uses

func (c *Clause) Weight(i int) int

Weight returns the weight of the ith literal. In a propositional clause or a cardinality constraint, that value will always be 1.

func (*Clause) WeightSum Uses

func (c *Clause) WeightSum() int

WeightSum returns the sum of the PB weights. If c is a propositional clause, the function will return the length of the clause.

type Interface Uses

type Interface interface {
    // Optimal solves or optimizes the problem and returns the best result.
    // If the results chan is non nil, it will write the associated model each time one is found.
    // It will stop as soon as a model of cost 0 is found, or the problem is not satisfiable anymore.
    // The last satisfying model, if any, will be returned with the Sat status.
    // If no model at all could be found, the Unsat status will be returned.
    // If the solver prematurely stopped, the Indet status will be returned.
    // If data is sent to stop, the method may stop prematurely.
    // In any case, results will be closed before the function returns.
    // NOTE: data sent on stop may be ignored by an implementation.
    Optimal(results chan Result, stop chan struct{}) Result
    // Enumerate returns the number of models for the problem.
    // If the models chan is non nil, it will write the associated model each time one is found.
    // If data is sent to stop, the method may stop prematurely.
    // In any case, models will be closed before the function returns.
    // NOTE: data sent on stop may be ignored by an implementation.
    Enumerate(models chan []bool, stop chan struct{}) int
}

Interface is any type implementing a solver. The basic Solver defined in this package implements it. Any solver that uses the basic solver to solve more complex problems (MAXSAT, MUS extraction, etc.) can implement it, too.

type Lit Uses

type Lit int32

Lit start at 0 and are positive ; the sign is the last bit. Thus the CNF literal -3 is encoded as 2 * (3-1) + 1 = 5.

func IntToLit Uses

func IntToLit(i int32) Lit

IntToLit converts a CNF literal to a Lit.

func (Lit) Int Uses

func (l Lit) Int() int32

Int returns the equivalent CNF literal.

func (Lit) IsPositive Uses

func (l Lit) IsPositive() bool

IsPositive is true iff l is > 0

func (Lit) Negation Uses

func (l Lit) Negation() Lit

Negation returns -l, i.e the positive version of l if it is negative, or the negative version otherwise.

func (Lit) Var Uses

func (l Lit) Var() Var

Var returns the variable of l.

type Model Uses

type Model []decLevel

A Model is a binding for several variables. It can be totally bound (i.e all vars have a true or false binding) or only partially (i.e some vars have no binding yet or their binding has no impact). Each var, in order, is associated with a binding. Binding are implemented as decision levels: - a 0 value means the variable is free, - a positive value means the variable was set to true at the given decLevel, - a negative value means the variable was set to false at the given decLevel.

func (Model) String Uses

func (m Model) String() string

type PBConstr Uses

type PBConstr struct {
    Lits    []int // List of literals, designed with integer values. A positive value means the literal is true, a negative one it is false.
    Weights []int // Weight of each lit from Lits. If nil, all lits == 1
    AtLeast int   // Sum of all lits must be at least this value
}

A PBConstr is a Pseudo-Boolean constraint.

func AtLeast Uses

func AtLeast(lits []int, n int) PBConstr

AtLeast returns a PB constraint stating that at least n literals must be true. It takes ownership of lits.

func AtMost Uses

func AtMost(lits []int, n int) PBConstr

AtMost returns a PB constraint stating that at most n literals can be true. It takes ownership of lits.

func Eq Uses

func Eq(lits []int, weights []int, n int) []PBConstr

Eq returns a set of PB constraints stating that the sum of all literals multiplied by their weight must be exactly n. Will panic if len(weights) != len(lits).

func GtEq Uses

func GtEq(lits []int, weights []int, n int) PBConstr

GtEq returns a PB constraint stating that the sum of all literals multiplied by their weight must be at least n. Will panic if len(weights) != len(lits).

func LtEq Uses

func LtEq(lits []int, weights []int, n int) PBConstr

LtEq returns a PB constraint stating that the sum of all literals multiplied by their weight must be at most n. Will panic if len(weights) != len(lits).

func PropClause Uses

func PropClause(lits ...int) PBConstr

PropClause returns a PB constraint equivalent to a propositional clause: at least one of the given literals must be true. It takes ownership of lits.

func (PBConstr) Clause Uses

func (c PBConstr) Clause() *Clause

Clause returns the clause associated with the given constraint.

func (PBConstr) WeightSum Uses

func (c PBConstr) WeightSum() int

WeightSum returns the sum of the weight of all terms.

type Problem Uses

type Problem struct {
    NbVars  int        // Total nb of vars
    Clauses []*Clause  // List of non-empty, non-unit clauses
    Status  Status     // Status of the problem. Can be trivially UNSAT (if empty clause was met or inferred by UP) or Indet.
    Units   []Lit      // List of unit literal found in the problem.
    Model   []decLevel // For each var, its inferred binding. 0 means unbound, 1 means bound to true, -1 means bound to false.
    // contains filtered or unexported fields
}

A Problem is a list of clauses & a nb of vars.

func ParseCNF Uses

func ParseCNF(f io.Reader) (*Problem, error)

ParseCNF parses a CNF file and returns the corresponding Problem.

func ParseCardConstrs Uses

func ParseCardConstrs(constrs []CardConstr) *Problem

ParseCardConstrs parses the given cardinality constraints. Will panic if a zero value appears in the literals.

Code:

clauses := []CardConstr{
    {Lits: []int{1, 2, 3}, AtLeast: 3},
    {Lits: []int{2, 3, -4}, AtLeast: 2},
    AtLeast1(-1, -4),
    AtLeast1(-2, -3, 4),
}
pb := ParseCardConstrs(clauses)
s := New(pb)
if status := s.Solve(); status == Unsat {
    fmt.Println("Problem is not satisfiable")
} else {
    fmt.Printf("Model found: %v\n", s.Model())
}

Output:

Problem is not satisfiable

func ParseOPB Uses

func ParseOPB(f io.Reader) (*Problem, error)

ParseOPB parses a file corresponding to the OPB syntax. See http://www.cril.univ-artois.fr/PB16/format.pdf for more details.

func ParsePBConstrs Uses

func ParsePBConstrs(constrs []PBConstr) *Problem

ParsePBConstrs parses and returns a PB problem from PBConstr values.

func ParseSlice Uses

func ParseSlice(cnf [][]int) *Problem

ParseSlice parse a slice of slice of lits and returns the equivalent problem. The argument is supposed to be a well-formed CNF.

func (*Problem) CNF Uses

func (pb *Problem) CNF() string

CNF returns a DIMACS CNF representation of the problem.

func (*Problem) Optim Uses

func (pb *Problem) Optim() bool

Optim returns true iff pb is an optimisation problem, ie a problem for which we not only want to find a model, but also the best possible model according to an optimization constraint.

func (*Problem) PBString Uses

func (pb *Problem) PBString() string

PBString returns a representation of the problem as a pseudo-boolean problem.

func (*Problem) SetCostFunc Uses

func (pb *Problem) SetCostFunc(lits []Lit, weights []int)

SetCostFunc sets the function to minimize when optimizing the problem. If all weights are 1, weights can be nil. In all other cases, len(lits) must be the same as len(weights).

type Result Uses

type Result struct {
    Status Status
    Model  []bool
    Weight int
}

A Result is a status, either Sat, Unsat or Indet. If the status is Sat, the Result also associates a ModelMap with an integer value. This value is typically used in optimization processes. If the weight is 0, that means all constraints could be solved. By definition, in decision problems, the cost will always be 0.

type Solver Uses

type Solver struct {
    Verbose bool // Indicates whether the solver should display information during solving or not. False by default

    Stats Stats // Statistics about the solving process.
    // contains filtered or unexported fields
}

A Solver solves a given problem. It is the main data structure.

func New Uses

func New(problem *Problem) *Solver

New makes a solver, given a number of variables and a set of clauses. nbVars should be consistent with the content of clauses, i.e. the biggest variable in clauses should be >= nbVars.

func (*Solver) AppendClause Uses

func (s *Solver) AppendClause(clause *Clause)

AppendClause appends a new clause to the set of clauses. This is not a learned clause, but a clause that is part of the problem added afterwards (during model counting, for instance).

func (*Solver) CountModels Uses

func (s *Solver) CountModels() int

CountModels returns the total number of models for the given problem.

func (*Solver) Enumerate Uses

func (s *Solver) Enumerate(models chan []bool, stop chan struct{}) int

Enumerate returns the total number of models for the given problems. if "models" is non-nil, it will write models on it as soon as it discovers them. models will be closed at the end of the method.

func (*Solver) Minimize Uses

func (s *Solver) Minimize() int

Minimize tries to find a model that minimizes the weight of the clause defined as the optimisation clause in the problem. If no model can be found, it will return a cost of -1. Otherwise, calling s.Model() afterwards will return the model that satisfy the formula, such that no other model with a smaller cost exists. If this function is called on a non-optimization problem, it will either return -1, or a cost of 0 associated with a satisfying model (ie any model is an optimal model).

func (*Solver) Model Uses

func (s *Solver) Model() []bool

Model returns a slice that associates, to each variable, its binding. If s's status is not Sat, the method will panic.

func (*Solver) Optim Uses

func (s *Solver) Optim() bool

Optim returns true iff the underlying problem is an optimization problem (rather than a satisfaction one).

func (*Solver) Optimal Uses

func (s *Solver) Optimal(results chan Result, stop chan struct{}) (res Result)

Optimal returns the optimal solution, if any. If results is non-nil, all solutions will be written to it. In any case, results will be closed at the end of the call.

func (*Solver) OutputModel Uses

func (s *Solver) OutputModel()

OutputModel outputs the model for the problem on stdout.

func (*Solver) PBString Uses

func (s *Solver) PBString() string

PBString returns a representation of the solver's state as a pseudo-boolean problem.

func (*Solver) Solve Uses

func (s *Solver) Solve() Status

Solve solves the problem associated with the solver and returns the appropriate status.

type Stats Uses

type Stats struct {
    NbRestarts      int
    NbConflicts     int
    NbDecisions     int
    NbUnitLearned   int // How many unit clauses were learned
    NbBinaryLearned int // How many binary clauses were learned
    NbLearned       int // How many clauses were learned
    NbDeleted       int // How many clauses were deleted
}

Stats are statistics about the resolution of the problem. They are provided for information purpose only.

type Status Uses

type Status byte

Status is the status of a given problem or clause at a given moment.

func (Status) String Uses

func (s Status) String() string

type Var Uses

type Var int32

Var start at 0 ; thus the CNF variable 1 is encoded as the Var 0.

func IntToVar Uses

func IntToVar(i int32) Var

IntToVar converts a CNF variable to a Var.

func (Var) Lit Uses

func (v Var) Lit() Lit

Lit returns the positive Lit associated to v.

func (Var) SignedLit Uses

func (v Var) SignedLit(signed bool) Lit

SignedLit returns the Lit associated to v, negated if 'signed', positive else.

Package solver imports 7 packages (graph) and is imported by 4 packages. Updated 2019-07-19. Refresh now. Tools for package owners.