`import "github.com/crillab/gophersat/maxsat"`

Package maxsat provides an optimization solver for SAT/PB. It allows the user to provide weighted partial MAXSAT problems or weighted pseudo-booleans problems.

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.

- 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
- func Not(name string) Lit
- func Var(name string) Lit
- func (l Lit) Negation() Lit
- func (l Lit) String() string
- type Model
- type Problem
- func New(constrs ...Constr) *Problem
- func (pb *Problem) Output()
- func (pb *Problem) SetVerbose(verbose bool)
- func (pb *Problem) Solve() (Model, int)
- type Solver

constr.go doc.go parser.go problem.go

ParseWCNF parses a CNF file and returns the corresponding solver.Interface.

❖

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.

HardClause returns a propositional clause that must be satisfied.

HardPBConstr returns a pseudo-boolean constraint that must be satisfied.

SoftClause returns an optional propositional clause.

SoftPBConstr returns an optional pseudo-boolean constraint.

WeightedClause returns a weighted optional propositional clause.

WeightedPBConstr returns a weighted optional pseudo-boolean constraint.

A Lit is a potentially-negated boolean variable.

Not returns a new negated Lit whose var is named "name".

Var returns a new positive Lit whose var is named "name".

Negation returns the logical negation of l.

A Model associates variable names with a binding.

❖

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

A Problem is a set of constraints.

New returns a new problem associated with the given constraints.

Output output the problem to stdout in the OPB format.

SetVerbose makes the underlying solver verbose, or not.

Solve returns an optimal Model for the problem and the associated cost. If the model is nil, the problem was not satisfiable (i.e hard clauses could not be satisfied).

❖

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

A Solver is a [partial][weighted] MAXSAT solver. It implements solver.Interface.

Enumerate does not make sense for a MAXSAT problem, so it will panic when called. This might change in later versions.

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.

Package maxsat imports 6 packages (graph) and is imported by 1 packages. Updated 2019-05-05. Refresh now. Tools for package owners.