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