`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.

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)

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

- Constants
- type CardConstr
- func AtLeast1(lits ...int) CardConstr
- func AtMost1(lits ...int) CardConstr
- func Exactly1(lits ...int) []CardConstr
- type Clause
- func NewCardClause(lits []Lit, card int) *Clause
- func NewClause(lits []Lit) *Clause
- func NewLearnedClause(lits []Lit) *Clause
- func NewPBClause(lits []Lit, weights []int, card int) *Clause
- func (c *Clause) CNF() string
- func (c *Clause) Cardinality() int
- func (c *Clause) First() Lit
- func (c *Clause) Get(i int) Lit
- func (c *Clause) Learned() bool
- func (c *Clause) Len() int
- func (c *Clause) PBString() string
- func (c *Clause) PseudoBoolean() bool
- func (c *Clause) Second() Lit
- func (c *Clause) Set(i int, l Lit)
- func (c *Clause) Shrink(newLen int)
- func (c *Clause) Weight(i int) int
- func (c *Clause) WeightSum() int
- type Interface
- type Lit
- func IntToLit(i int32) Lit
- func (l Lit) Int() int32
- func (l Lit) IsPositive() bool
- func (l Lit) Negation() Lit
- func (l Lit) Var() Var
- type Model
- type PBConstr
- func AtLeast(lits []int, n int) PBConstr
- func AtMost(lits []int, n int) PBConstr
- func Eq(lits []int, weights []int, n int) []PBConstr
- func GtEq(lits []int, weights []int, n int) PBConstr
- func LtEq(lits []int, weights []int, n int) PBConstr
- func PropClause(lits ...int) PBConstr
- func (c PBConstr) Clause() *Clause
- func (c PBConstr) WeightSum() int
- type Problem
- func ParseCNF(f io.Reader) (*Problem, error)
- func ParseCardConstrs(constrs []CardConstr) *Problem
- func ParseOPB(f io.Reader) (*Problem, error)
- func ParsePBConstrs(constrs []PBConstr) *Problem
- func ParseSlice(cnf [][]int) *Problem
- func (pb *Problem) CNF() string
- func (pb *Problem) Optim() bool
- func (pb *Problem) PBString() string
- func (pb *Problem) SetCostFunc(lits []Lit, weights []int)
- type Result
- type Solver
- func New(problem *Problem) *Solver
- func (s *Solver) AppendClause(clause *Clause)
- func (s *Solver) CountModels() int
- func (s *Solver) Enumerate(models chan []bool, stop chan struct{}) int
- func (s *Solver) Minimize() int
- func (s *Solver) Model() []bool
- func (s *Solver) Optim() bool
- func (s *Solver) Optimal(results chan Result, stop chan struct{}) (res Result)
- func (s *Solver) OutputModel()
- func (s *Solver) PBString() string
- func (s *Solver) Solve() Status
- type Stats
- type Status
- type Var

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

❖

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 )

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(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(lits ...int) CardConstr

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

❖

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

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

❖

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

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

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

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

NewLearnedClause returns a new clause marked as learned.

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

CNF returns a DIMACS CNF representation of the clause.

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

First returns the first lit from the clause.

Get returns the ith literal from the clause.

Learned returns true iff c was a learned clause.

Len returns the nb of lits in the clause.

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

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

Second returns the second lit from the clause.

Set sets the ith literal of the clause.

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

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

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

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.

IntToLit converts a CNF literal to a Lit.

Int returns the equivalent CNF literal.

IsPositive is true iff l is > 0

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

Var returns the variable of l.

❖

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.

❖

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.

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

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

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

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

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

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.

Clause returns the clause associated with the given constraint.

WeightSum returns the sum of the weight of all terms.

❖

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.

ParseCNF parses a CNF file and returns the corresponding Problem.

❖

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

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

ParsePBConstrs parses and returns a PB problem from PBConstr values.

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

CNF returns a DIMACS CNF representation of the problem.

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.

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

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

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

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.

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

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

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.

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

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

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

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.

OutputModel outputs the model for the problem on stdout.

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

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

❖

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.

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

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

IntToVar converts a CNF variable to a Var.

Lit returns the positive Lit associated to v.

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.