maxsat

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
  • 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
  • func (s *Solver) Enumerate(models chan []bool, stop chan struct{}) int
  • func (s *Solver) Optimal(results chan solver.Result, stop chan struct{}) solver.Result

Functions

func ParseWCNF

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

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

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

func HardClause(lits ...Lit) Constr

HardClause returns a propositional clause that must be satisfied.

func HardPBConstr

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

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

func SoftClause

func SoftClause(lits ...Lit) Constr

SoftClause returns an optional propositional clause.

func SoftPBConstr

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

SoftPBConstr returns an optional pseudo-boolean constraint.

func WeightedClause

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

WeightedClause returns a weighted optional propositional clause.

func WeightedPBConstr

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

WeightedPBConstr returns a weighted optional pseudo-boolean constraint.

type Lit

type Lit struct {
	Var     string
	Negated bool
}

A Lit is a potentially-negated boolean variable.

func Not

func Not(name string) Lit

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

func Var

func Var(name string) Lit

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

func (Lit) Negation

func (l Lit) Negation() Lit

Negation returns the logical negation of l.

func (Lit) String

func (l Lit) String() string

type Model

type Model map[string]bool

A Model associates variable names with a binding.

type Problem

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

A Problem is a set of constraints.

func New

func New(constrs ...Constr) *Problem

New returns a new problem associated with the given constraints.

func (*Problem) Output

func (pb *Problem) Output()

Output output the problem to stdout in the OPB format.

func (*Problem) SetVerbose

func (pb *Problem) SetVerbose(verbose bool)

SetVerbose makes the underlying solver verbose, or not.

func (*Problem) Solve

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

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

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

func (*Solver) Enumerate

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

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.