Documentation
¶
Overview ¶
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 ¶
- Constants
- type CardConstr
- type 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) SimplifyPB() (units []Lit, c2 *Clause, ok bool)
- func (c *Clause) Weight(i int) int
- func (c *Clause) WeightSum() int
- type Interface
- type Lit
- type Model
- type PBConstr
- type Problem
- type Result
- type Solver
- func (s *Solver) AppendClause(clause *Clause)
- func (s *Solver) Assume(lits []Lit) Status
- 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
Examples ¶
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 )
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type CardConstr ¶
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 ¶
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 ¶
func AtMost1(lits ...int) CardConstr
AtMost1 returns a cardinality constraint stating that at most one of the given lits can be true.
func Exactly1 ¶
func Exactly1(lits ...int) []CardConstr
Exactly1 returns two cardinality constraints stating that exactly one of the given lits must be true.
type Clause ¶
type Clause struct {
// contains filtered or unexported fields
}
A Clause is a list of Lit, associated with possible data (for learned clauses).
func NewCardClause ¶
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 NewLearnedClause ¶
NewLearnedClause returns a new clause marked as learned.
func NewPBClause ¶
NewPBClause returns a pseudo-boolean clause with the given lits, weights and minimal cardinality.
func (*Clause) Cardinality ¶
Cardinality returns the minimum number of literals that must be true to satisfy the clause.
func (*Clause) PBString ¶
PBString returns a string representation of c as a pseudo-boolean expression.
func (*Clause) PseudoBoolean ¶
PseudoBoolean returns true iff c is a pseudo boolean constraint, and not just a propositional clause or cardinality constraint.
func (*Clause) Shrink ¶
Shrink reduces the length of the clauses, by removing all lits starting from position newLen.
func (*Clause) SimplifyPB ¶ added in v1.4.0
SimplifyPB tries to simplify a pseudo boolean constraint by propagating all lits that can be propagated not matter whet the assignment. A PB constraint can also be false if all its coeficients are smaller than the cardinality. It will return a list of unit lits (if any), a new, simplified clause (or nil if all lits can be propagated and/or ignored) and a boolean ok indicating whether the clause can be satisfied or not. If ok is false, other return parameters are irrelevant.
type Interface ¶ added in v1.1.0
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 ¶
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 IntsToLits ¶ added in v1.4.0
IntsToLits converts a list of CNF literals to a []Lit. This is a helper function as the same result can be achieved by calling IntToLit several times.
type Model ¶
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 ¶
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 ¶
AtLeast returns a PB constraint stating that at least n literals must be true. It takes ownership of lits.
func AtMost ¶
AtMost returns a PB constraint stating that at most n literals can be true. It takes ownership of lits.
func Eq ¶
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 ¶
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 ¶
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 ¶
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.
type Problem ¶
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 ParseCardConstrs ¶
func ParseCardConstrs(constrs []CardConstr) *Problem
ParseCardConstrs parses the given cardinality constraints. Will panic if a zero value appears in the literals.
Example ¶
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 ¶
ParseOPB parses a file corresponding to the OPB syntax. See http://www.cril.univ-artois.fr/PB16/format.pdf for more details.
func ParsePBConstrs ¶
ParsePBConstrs parses and returns a PB problem from PBConstr values.
func ParseSlice ¶
ParseSlice parse a slice of slice of lits and returns the equivalent problem. The argument is supposed to be a well-formed CNF.
func ParseSliceNb ¶ added in v1.2.0
ParseSliceNb parse a slice of slice of lits and returns the equivalent problem. The argument is supposed to be a well-formed CNF. The number of vars is provided because clauses might be added to it later.
func (*Problem) DetectAtMostOne ¶ added in v1.4.0
func (pb *Problem) DetectAtMostOne()
DetectAtMostOne tries to detect AtMostOne constraints encoded using the pairwise encoding. It replaces those binary clauses by a single cardinality constraint. This should mostly be called using the CuttingPlanes option, as it can dramatically improve the resolution process in some cases.
func (*Problem) Optim ¶
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 ¶
PBString returns a representation of the problem as a pseudo-boolean problem.
func (*Problem) SetCostFunc ¶
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 ¶ added in v1.1.0
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 ¶
type Solver struct {
Verbose bool // Indicates whether the solver should display information during solving or not. False by default
Certified bool // Indicates whether a certificate should be generated during solving or not, using the RUP notation. This is useful to prove UNSAT instances. False by default.
CertChan chan string // Indicates where to write the certificate. If Certified is true but CertChan is nil, the certificate will be written on stdout.
CuttingPlanes bool // Indicates that the cutting planes resolution method should be used. Note that this is only efficient on PB problems.
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 ¶
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 ¶
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) Assume ¶ added in v1.2.0
Assume adds unit literals to the solver. This is useful when calling the solver several times, e.g to keep it "hot" while removing clauses.
func (*Solver) CountModels ¶
CountModels returns the total number of models for the given problem.
func (*Solver) Enumerate ¶ added in v1.1.0
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 ¶
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 ¶
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 ¶ added in v1.0.3
Optim returns true iff the underlying problem is an optimization problem (rather than a satisfaction one).
func (*Solver) Optimal ¶ added in v1.1.0
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 ¶
func (s *Solver) OutputModel()
OutputModel outputs the model for the problem on stdout.
type Stats ¶
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.
Source Files