maxsat

Documentation

Overview

Package maxsat provides an implementation of a MAX-SAT solver with different solving algorithms in LogicNG.

Given an unsatisfiable formula in CNF, the MAX-SAT problem is the problem of finding an assignment which satisfies the maximum number of clauses and therefore solves an optimization problem rather than a decision problem. There are two extensions to MAX-SAT Solving: 1) the distinction of hard/soft clauses, and 2) additional weighted clauses, yielding four different flavours of MAX-SAT solving:

1. Pure MaxSAT
2. Partial MaxSAT
3. Weighted MaxSAT
4. Weighted Partial MaxSAT

In a Partial MAX-SAT problem you can distinguish between hard and soft clauses. A hard clause must be satisfied whereas a soft clause should be satisfied but can be left unsatisfied. This means the solver only optimizes over the soft clauses. If the hard clauses themselves are unsatisfiable, no solution can be found.

In a Weighted MAX-SAT problem clauses can have a positive weight. The solver then does not optimize the number of satisfied clauses but the sum of the weights of the satisfied clauses.

The Weighted Partial MAX-SAT problem is the combination of Partial MaxSAT and weighted MAX-SAT. I.e. you can add hard clauses and weighted soft clauses to the MAX-SAT solver.

Note two important points:

• MAX-SAT can be defined as weighted MAX-SAT restricted to formulas whose clauses have weight 1, and as Partial MAX-SAT in the case that all the clauses are declared to be soft.
• The above definitions talk about clauses on the solver, not arbitrary formulas. In real-world use cases you often want to weight whole formulas and not just clauses. LogicNG's MAX-SAT solver API gives you this possibility and internally translates the formulas and their weights accordingly.

A small example for using the solver:

fac := formula.NewFactory()
p := parser.New(fac)
solver := maxsat.OLL(fac)
solver.AddHardFormula(p.ParseUnsafe("A & B & (C | D)"))
solver.AddSoftFormula(p.ParseUnsafe("A => ~B"), 2)
solver.AddSoftFormula(p.ParseUnsafe("~C"), 4)
solver.AddSoftFormula(p.ParseUnsafe("~D"), 8)
result := solver.Solve() // {Satisfiable: true, Optimum: 6}

Index

• func ReadDimacsToSolver(fac f.Factory, solver *Solver, filename string) error
• type Algorithm
  • func (i Algorithm) String() string
• type Config
  • func DefaultConfig() *Config
  • func (Config) DefaultConfig() configuration.Config
  • func (Config) Sort() configuration.Sort
• type Handler
• type IncrementalStrategy
  • func (i IncrementalStrategy) String() string
• type Result
• type Solver
  • func IncWBO(fac f.Factory, config ...*Config) *Solver
  • func LinearSU(fac f.Factory, config ...*Config) *Solver
  • func LinearUS(fac f.Factory, config ...*Config) *Solver
  • func MSU3(fac f.Factory, config ...*Config) *Solver
  • func OLL(fac f.Factory, config ...*Config) *Solver
  • func WBO(fac f.Factory, config ...*Config) *Solver
  • func WMSU3(fac f.Factory, config ...*Config) *Solver
  • func (m *Solver) AddHardFormula(formula ...f.Formula) error
  • func (m *Solver) AddSoftFormula(formula f.Formula, weight int) error
  • func (m *Solver) Model() (*model.Model, error)
  • func (m *Solver) Reset()
  • func (m *Solver) Solve() Result
  • func (m *Solver) SolveWithHandler(maxsatHandler Handler) (result Result, ok bool)
  • func (m *Solver) SupportsUnweighted() bool
  • func (m *Solver) SupportsWeighted() bool
• type TimeoutHandler
  • func HandlerWithTimeout(timeout handler.Timeout) *TimeoutHandler
  • func (t *TimeoutHandler) FinishedSolving()
  • func (t *TimeoutHandler) FoundLowerBound(lowerBound int, _ *model.Model) bool
  • func (t *TimeoutHandler) FoundUpperBound(upperBound int, _ *model.Model) bool
  • func (t *TimeoutHandler) LowerBoundApproximation() int
  • func (t *TimeoutHandler) SatHandler() sat.Handler
  • func (t *TimeoutHandler) UpperBoundApproximation() int
• type WeightStrategy
  • func (i WeightStrategy) String() string

Functions

func ReadDimacsToSolver

func ReadDimacsToSolver(fac f.Factory, solver *Solver, filename string) error

ReadDimacsToSolver reads a Dimacs file for weighted MAX-SAT problems from the given filename and loads it directly to the given solver. Returns an error if the file could not be read.

Types

type Algorithm

type Algorithm byte

Algorithm encodes the different MAX-SAT algorithms.

const (
	AlgWBO Algorithm = iota
	AlgIncWBO
	AlgLinearSU
	AlgLinearUS
	AlgMSU3
	AlgWMSU3
	AlgOLL
)

func (Algorithm) String

func (i Algorithm) String() string

type Config

type Config struct {
	IncrementalStrategy IncrementalStrategy
	WeightStrategy      WeightStrategy
	Symmetry            bool
	Limit               int
	BMO                 bool
}

Config describes the configuration of a MAX-SAT solver. Incremental and weight strategy can be configured as well as flags for symmetry usage, and BMO as well as the symmetry limit.

func DefaultConfig

func DefaultConfig() *Config

DefaultConfig returns the default configuration for a MAX-SAT configuration.

func (Config) DefaultConfig

func (Config) DefaultConfig() configuration.Config

DefaultConfig returns the default configuration for a MAX-SAT configuration.

func (Config) Sort

func (Config) Sort() configuration.Sort

Sort returns the configuration sort (MaxSat).

type Handler

type Handler interface {
	handler.Handler
	SatHandler() sat.Handler
	FoundLowerBound(lowerBound int, model *model.Model) bool
	FoundUpperBound(upperBound int, model *model.Model) bool
	FinishedSolving()
	LowerBoundApproximation() int
	UpperBoundApproximation() int
}

Handler is an interface for MAX-SAT handlers which can abort the computation based on the upper and lower bounds found during the computation.

type IncrementalStrategy

type IncrementalStrategy byte

IncrementalStrategy encodes the different strategies for incremental encoding.

const (
	IncNone IncrementalStrategy = iota
	IncIterative
)

func (IncrementalStrategy) String

func (i IncrementalStrategy) String() string

type Result

type Result struct {
	Satisfiable bool
	Optimum     int
}

Result represents the result of a MAX-SAT computation. It holds a flag whether the problem was satisfiable or not. In case it was satisfiable, the final lower bound of the solver is stored as the Optimum.

type Solver

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

A Solver can be used to solve the MAX-SAT problem. Depending on the underlying solving algorithm it supports also partial and/or weighted MAX-SAT problems.

func IncWBO

func IncWBO(fac f.Factory, config ...*Config) *Solver

IncWBO generates a new MAX-SAT solver with the Incremental Weighted Boolean Optimization algorithm. This algorithm is based on unsat cores and supports both partial and weighted MAX-SAT problems.

func LinearSU

func LinearSU(fac f.Factory, config ...*Config) *Solver

LinearSU generates a new MAX-SAT solver with the Linear Sat-Unsat algorithm. This algorithm is based on linear search and supports both weighted and partial MAX-SAT problems.

func LinearUS

func LinearUS(fac f.Factory, config ...*Config) *Solver

LinearUS generates a new MAX-SAT solver with the Linear Unsat-Sat algorithm. This algorithm is based on linear search and supports partial MAX-SAT problems but no weighted problems.

func MSU3

func MSU3(fac f.Factory, config ...*Config) *Solver

MSU3 generates a new MAX-SAT solver with the MSU3 algorithm, a seminal-core guided algorithm. This algorithm is based on unsat cores and supports partial MAX-SAT problems but no weighted problems.

func OLL

func OLL(fac f.Factory, config ...*Config) *Solver

OLL generates a new MAX-SAT solver with the OLL algorithm. This algorithm is based on unsat cores and supports both partial and weighted MAX-SAT problems.

func WBO

func WBO(fac f.Factory, config ...*Config) *Solver

WBO generates a new MAX-SAT solver with the Weighted Boolean Optimization algorithm. This algorithm is based on unsat cores and supports both partial and weighted MAX-SAT problems.

func WMSU3

func WMSU3(fac f.Factory, config ...*Config) *Solver

WMSU3 generates a new MAX-SAT solver with the weighted MSU3 algorithm, a seminal-core guided algorithm. This algorithm is based on unsat cores and supports both partial and weighted MAX-SAT problems.

func (*Solver) AddHardFormula

func (m *Solver) AddHardFormula(formula ...f.Formula) error

AddHardFormula adds the given formulas as hard formulas to the solver which must always be satisfied. Since MAX-SAT solvers in LogicNG do not support an incremental interface, this function returns an error if the solver was already solved once.

func (*Solver) AddSoftFormula

func (m *Solver) AddSoftFormula(formula f.Formula, weight int) error

AddSoftFormula adds the given formulas as soft formulas with the given weight to the solver. The weight must be >0 otherwise an error is returned. Since MAX-SAT solvers in LogicNG do not support an incremental interface, this function returns an error if the solver was already solved once.

func (*Solver) Model

func (m *Solver) Model() (*model.Model, error)

Model returns the model for the last MAX-SAT computation. It returns an error if the problem is not yet solved or it was unsatisfiable.

func (*Solver) Reset

func (m *Solver) Reset()

Reset resets the MAX-SAT solver by clearing all internal data structures.

func (*Solver) Solve

func (m *Solver) Solve() Result

Solve solves the MAX-SAT problem currently on the solver and returns the computation result.

func (*Solver) SolveWithHandler

func (m *Solver) SolveWithHandler(maxsatHandler Handler) (result Result, ok bool)

SolveWithHandler solves the MAX-SAT problem currently on the solver. The computation can be aborted with the given handler. The computation result is returned and an ok flag which is false if the computation was aborted by the handler.

func (*Solver) SupportsUnweighted

func (m *Solver) SupportsUnweighted() bool

SupportsUnweighted reports whether the solver supports unweighted problems.

func (*Solver) SupportsWeighted

func (m *Solver) SupportsWeighted() bool

SupportsWeighted reports whether the solver supports weighted problems.

type TimeoutHandler

type TimeoutHandler struct {
	handler.Timeout
	// contains filtered or unexported fields
}

A TimeoutHandler can be used to abort a MAX-SAT computation depending on a timeout set beforehand.

func HandlerWithTimeout

func HandlerWithTimeout(timeout handler.Timeout) *TimeoutHandler

HandlerWithTimeout generates a new timeout handler with the given timeout.

func (*TimeoutHandler) FinishedSolving

func (t *TimeoutHandler) FinishedSolving()

FinishedSolving is called when the MAX-SAT solver has finished the solving process.

func (*TimeoutHandler) FoundLowerBound

func (t *TimeoutHandler) FoundLowerBound(lowerBound int, _ *model.Model) bool

FoundLowerBound is called by the MAX-SAT solver each time a new lower bound is found. The current model for this bound is recorded. Returns whether the computation should be continued.

func (*TimeoutHandler) FoundUpperBound

func (t *TimeoutHandler) FoundUpperBound(upperBound int, _ *model.Model) bool

FoundUpperBound is called by the MAX-SAT solver each time a new upper bound is found. The current model for this bound is recorded. Returns whether the computation should be continued.

func (*TimeoutHandler) LowerBoundApproximation

func (t *TimeoutHandler) LowerBoundApproximation() int

LowerBoundApproximation returns the last found lower bound.

func (*TimeoutHandler) SatHandler

func (t *TimeoutHandler) SatHandler() sat.Handler

SatHandler returns the underlying SAT handler for the MAX-SAT handler.

func (*TimeoutHandler) UpperBoundApproximation

func (t *TimeoutHandler) UpperBoundApproximation() int

UpperBoundApproximation returns the last found upper bound.

type WeightStrategy

type WeightStrategy byte

WeightStrategy encodes the different strategies for handling weights.

const (
	WeightNone WeightStrategy = iota
	WeightNormal
	WeightDiversify
)

func (WeightStrategy) String

func (i WeightStrategy) String() string