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:
- Pure MaxSAT
- Partial MaxSAT
- Weighted MaxSAT
- 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
- type Config
- type Handler
- type IncrementalStrategy
- 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 (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
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
Types ¶
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 ¶
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 ¶
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 ¶
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 ¶
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 ¶
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 ¶
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 ¶
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 ¶
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 ¶
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 ¶
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 ¶
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 ¶
Solve solves the MAX-SAT problem currently on the solver and returns the computation result.
func (*Solver) SolveWithHandler ¶
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 ¶ added in v0.4.0
SupportsUnweighted reports whether the solver supports unweighted problems.
func (*Solver) SupportsWeighted ¶
SupportsWeighted reports whether the solver supports weighted problems.
type TimeoutHandler ¶
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
Source Files
¶
- alg_incwbo.go
- alg_linear_su.go
- alg_linear_us.go
- alg_msu3.go
- alg_oll.go
- alg_wbo.go
- alg_wmsu3.go
- algorithm.go
- algorithm_string.go
- config.go
- datastructures.go
- doc.go
- enc_ladder.go
- enc_swc.go
- enc_totalizer.go
- encoder.go
- handler.go
- incrementalstrategy_string.go
- problemtype_string.go
- reader.go
- result_string.go
- solver.go
- weightstrategy_string.go