gophersat: github.com/crillab/gophersat/maxsat Index | Files

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.

Index

Package Files

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

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.