gophersat: github.com/crillab/gophersat/maxsat

## package maxsat

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

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

### func ParseWCNF¶Uses

`func ParseWCNF(f io.Reader) (solver.Interface, error)`

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

### type Constr¶Uses

```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¶Uses

`func HardClause(lits ...Lit) Constr`

HardClause returns a propositional clause that must be satisfied.

#### func HardPBConstr¶Uses

`func HardPBConstr(lits []Lit, coeffs []int, atLeast int) Constr`

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

#### func SoftClause¶Uses

`func SoftClause(lits ...Lit) Constr`

SoftClause returns an optional propositional clause.

#### func SoftPBConstr¶Uses

`func SoftPBConstr(lits []Lit, coeffs []int, atLeast int) Constr`

SoftPBConstr returns an optional pseudo-boolean constraint.

#### func WeightedClause¶Uses

`func WeightedClause(lits []Lit, weight int) Constr`

WeightedClause returns a weighted optional propositional clause.

#### func WeightedPBConstr¶Uses

`func WeightedPBConstr(lits []Lit, coeffs []int, atLeast int, weight int) Constr`

WeightedPBConstr returns a weighted optional pseudo-boolean constraint.

### type Lit¶Uses

```type Lit struct {
Var     string
Negated bool
}```

A Lit is a potentially-negated boolean variable.

#### func Not¶Uses

`func Not(name string) Lit`

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

#### func Var¶Uses

`func Var(name string) Lit`

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

#### func (Lit) Negation¶Uses

`func (l Lit) Negation() Lit`

Negation returns the logical negation of l.

#### func (Lit) String¶Uses

`func (l Lit) String() string`

### type Model¶Uses

`type Model map[string]bool`

A Model associates variable names with a binding.

### type Problem¶Uses

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

A Problem is a set of constraints.

#### func New¶Uses

`func New(constrs ...Constr) *Problem`

New returns a new problem associated with the given constraints.

#### func (*Problem) Output¶Uses

`func (pb *Problem) Output()`

Output output the problem to stdout in the OPB format.

#### func (*Problem) SetVerbose¶Uses

`func (pb *Problem) SetVerbose(verbose bool)`

SetVerbose makes the underlying solver verbose, or not.

#### func (*Problem) Solve¶Uses

`func (pb *Problem) Solve() (Model, int)`

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¶Uses

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

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

#### func (*Solver) Enumerate¶Uses

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

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

#### func (*Solver) Optimal¶Uses

`func (s *Solver) Optimal(results chan solver.Result, stop chan struct{}) solver.Result`

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.