Documentation
¶
Overview ¶
Package maxsat provides an optimization solver for SAT/PB. It allows the user to provide weighted partial MAXSAT problems or weighted pseudo-booleans problems.
Definition ¶
A MAXSAT problem is a problem where, contrary to "plain-old" SAT decision problems, the user is not looking at whether the problem can be solved at all, but, if it cannot be solved, if at least a subset of it can be solved, with that subset being as big as important. In other words, the MAXSAT solver is trying to find a model that satisfies as many clauses as possible, ideally all of them.
Pure MAXSAT is not very useful in practice. Generally, the user wants to add two more constraints : - a subset of the problem must be satisfied, no matter what; these are called *hard clauses*, - other clauses (called *soft clauses*) are optional, but some of them are deemed more important than others: they are associated with a cost.
That problem is called weighted partial MAXSAT (WP-MAXSAT). Note that MAXSAT is a special case of WP-MAXSAT where all the clauses are soft clauses of weight 1. Also note that the traditional, SAT decision problem is a special case of WP-MAXSAT where all clauses are hard clauses.
Gophersat is guaranteed to provide the best possible solution to any WP-MAXSAT problem, if given enough time. It will also give potentially suboptimal solutions as soon as it finds them. So, the user can either get a good-enough solution after a given amount of time, or wait as long as needed for the best possible solution.
Index ¶
- func ParseWCNF(f io.Reader) (solver.Interface, error)
- type Constr
- func HardClause(lits ...Lit) Constr
- func HardPBConstr(lits []Lit, coeffs []int, atLeast int) Constr
- func SoftClause(lits ...Lit) Constr
- func SoftPBConstr(lits []Lit, coeffs []int, atLeast int) Constr
- func WeightedClause(lits []Lit, weight int) Constr
- func WeightedPBConstr(lits []Lit, coeffs []int, atLeast int, weight int) Constr
- type Lit
- type Model
- type Problem
- type Solver
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
Types ¶
type Constr ¶
type Constr struct {
Lits []Lit // The list of lits in the problem.
Coeffs []int // The coefficients associated with each literals. If nil, all coeffs are supposed to be 1.
AtLeast int // Minimal cardinality for the constr to be satisfied.
Weight int // The weight of the clause, or 0 for a hard clause.
}
A Constr is a weighted pseudo-boolean constraint.
func HardClause ¶
HardClause returns a propositional clause that must be satisfied.
func HardPBConstr ¶
HardPBConstr returns a pseudo-boolean constraint that must be satisfied.
func SoftClause ¶
SoftClause returns an optional propositional clause.
func SoftPBConstr ¶
SoftPBConstr returns an optional pseudo-boolean constraint.
func WeightedClause ¶
WeightedClause returns a weighted optional propositional clause.
type Problem ¶
type Problem struct {
// contains filtered or unexported fields
}
A Problem is a set of constraints.
func (*Problem) Output ¶
func (pb *Problem) Output()
Output output the problem to stdout in the OPB format.
func (*Problem) SetVerbose ¶
SetVerbose makes the underlying solver verbose, or not.
type Solver ¶ added in v1.1.4
type Solver struct {
// contains filtered or unexported fields
}
A Solver is a [partial][weighted] MAXSAT solver. It implements solver.Interface.
func (*Solver) Enumerate ¶ added in v1.1.4
Enumerate does not make sense for a MAXSAT problem, so it will panic when called. This might change in later versions.
func (*Solver) Optimal ¶ added in v1.1.4
Optimal looks for the optimal solution to the underlying problem. If results is not nil, it writes a suboptimal solution every time it finds a new, better one. In any case, it returns the optimal solution to the problem, or UNSAT if the problem cannot be found.
Source Files