sat

package
v0.4.0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: May 11, 2024 License: MIT Imports: 14 Imported by: 2

Documentation

Overview

Package sat provides LogicNG's SAT solver with a rich interface.

The SAT problem is the problem of deciding whether a formula in Boolean logic is satisfiable or not. In other words, does there exist a variable assignment under which the formula evaluates to true?

A SAT solver is a tool that, given a formula f can compute its satisfiability.

A small example for using the solver: 

fac := formula.NewFactory()
p := parser.New(fac)
solver := sat.NewSolver(fac)
solver.Add(p.ParseUnsafe("A & B & (C | D)"))
solver.Add(p.ParseUnsafe("A => X"))
result := solver.Sat() // true
model := solver.Model(fac.Vars("A", "B", "C")) // model on the solver

LogicNG's SAT solver also has an incremental/decremental interface which can be used like this: 

f1 := p.ParseUnsafe("A & B & C")
solver.Add(f1)
solver.Sat()                       // true
initialState := solver.SaveState() // save the initial state
solver.Add(p.ParseUnsafe("~A"))    // add another formula
solver.Sat()                       // false
solver.LoadState(initialState)     // load the initial state again
solver.Add(p.ParseUnsafe("D"))     // add another formula
solver.Sat()                       // true

Index

Constants

View Source 
const (
	LitUndef = int32(-1) // constant for an undefined literal
	LitError = int32(-2) // constant for an error state literal
)

Variables

This section is empty.

Functions

func GenerateNQueens 

func GenerateNQueens(fac f.Factory, n int) f.Formula

GenerateNQueens generates an n-queens problem of size n and returns it as a formula.

func GeneratePigeonHole 

func GeneratePigeonHole(fac f.Factory, n int) f.Formula

GeneratePigeonHole generates a pigeon hole problem of size n and returns it as a formula.

func Implies 

func Implies(fac f.Factory, f1, f2 f.Formula) bool

Implies reports whether f1 implies f2 (f1 => f2 is always true).

func IsContradiction 

func IsContradiction(fac f.Factory, formula f.Formula) bool

IsContradiction reports whether the formula is a contradiction (always false).

func IsEquivalent 

func IsEquivalent(fac f.Factory, f1, f2 f.Formula) bool

IsEquivalent reports whether f1 is equivalent to f2 (f1 <=> f2 is always true).

func IsSatisfiable 

func IsSatisfiable(fac f.Factory, formula f.Formula) bool

IsSatisfiable reports whether the formula is satisfiable.

func IsTautology 

func IsTautology(fac f.Factory, formula f.Formula) bool

IsTautology reports whether the formula is a tautology (always true).

func MkLit 

func MkLit(v int32, sign bool) int32

MkLit generates a solver literals from a solver variable and sign.

func Not 

func Not(lit int32) int32

Not negates a solver literal.

func Sign 

func Sign(lit int32) bool

Sign returns if a literal on the solver is negative.

func UncheckedEnqueue 

func UncheckedEnqueue(m *CoreSolver, lit int32, reason *clause)

UncheckedEnqueue is the default function to add new variable decisions to the solver.

func Vari 

func Vari(lit int32) int32

Vari returns the solver variable of a solver literal.

Types

type Backbone 

type Backbone struct {
	Sat      bool         // flag whether the formula was satisfiable
	Positive []f.Variable // variables that occur positive in each model of the formula
	Negative []f.Variable // variables that occur negative in each model of the formula
	Optional []f.Variable // variables that are neither in the positive nor in the negative backbone
}

A Backbone of a formula is a set of literals (positive and/or negative) which are present in their respective polarity in every model of the given formula. Therefore, the literals must be set accordingly in order for the formula to evaluate to true.

func (*Backbone) CompleteBackbone 

func (b *Backbone) CompleteBackbone(fac f.Factory) []f.Literal

CompleteBackbone returns the positive and negative literals of the backbone.

func (*Backbone) ToFormula 

func (b *Backbone) ToFormula(fac f.Factory) f.Formula

ToFormula returns the conjunction of positive and negative literals of the backbone.

type BackboneSort 

type BackboneSort byte

BackboneSort describes sort of backbone should be computed: 

const (
	BBPos  BackboneSort = iota // only variables which occur positive in every model
	BBNeg                      // only variables which occur negative in every model
	BBBoth                     // positive, negative and optional variables
)

type CNFMethod 

type CNFMethod byte

CNFMethod encodes the different methods for adding formulas as CNF to the solver. 

const (
	CNFFactorization CNFMethod = iota // formula factories CNF method
	CNFPG                             // Plaisted-Greenbaum with NNF generation directly on solver
	CNFFullPG                         // Plaisted-Greenbaum without NNF generation directly on solver
)

func (CNFMethod) String 

func (i CNFMethod) String() string

type CallParams added in v0.3.0 

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

CallParams describe the parameters for a single SAT solver call.

func Params added in v0.3.0 

func Params() *CallParams

Params generates a new empty call parameter struct with the following default setting:

  • no handler
  • no additional formulas or propositions for the SAT call
  • no model generation for satisfiable formulas
  • no unsat core computation for unsatisfiable formulas
  • no computation of propagated literals at decision level 0

func WithAssumptions added in v0.3.0 

func WithAssumptions(literals []f.Literal) *CallParams

WithAssumptions generates a new parameter struct with the following setting:

  • additional assumption literals for the SAT call
  • no unsat core computation for unsatisfiable formulas
  • no handler
  • no model generation for satisfiable formulas
  • no computation of propagated literals at decision level 0

func WithCore added in v0.3.0 

func WithCore() *CallParams

WithCore generates a new parameter struct with the following setting:

  • unsat core computation for unsatisfiable formulas
  • no handler
  • no additional formulas or propositions for the SAT call
  • no model generation for satisfiable formulas
  • no computation of propagated literals at decision level 0

func WithHandler added in v0.3.0 

func WithHandler(handler Handler) *CallParams

WithHandler generates a new parameter struct with the following setting:

  • use the given handler
  • no unsat core computation for unsatisfiable formulas
  • no model generation for satisfiable formulas
  • no additional assumption literals for the SAT call
  • no computation of propagated literals at decision level 0

func WithModel added in v0.3.0 

func WithModel(variables []f.Variable) *CallParams

WithModel generates a new parameter struct with the following setting:

  • model generation for satisfiable formulas for the given variables
  • no handler
  • no additional formulas or propositions for the SAT call
  • no unsat core computation for unsatisfiable formulas
  • no computation of propagated literals at decision level 0

func (*CallParams) Formula added in v0.3.0 

func (p *CallParams) Formula(formula ...f.Formula) *CallParams

Formula sets additional formulas which will be added to the SAT solver before solving. Results like satisfiability, model, or unsat core are with respect to these additional formulas.

func (*CallParams) Handler added in v0.3.0 

func (p *CallParams) Handler(handler Handler) *CallParams

Handler sets a handler for the SAT call

func (*CallParams) Literal added in v0.3.0 

func (p *CallParams) Literal(literal ...f.Literal) *CallParams

Literal sets additional literals which will be added to the SAT solver before solving. Results like satisfiability, model, or unsat core are with respect to these additional literals.

func (*CallParams) Proposition added in v0.3.0 

func (p *CallParams) Proposition(proposition ...f.Proposition) *CallParams

Proposition sets additional propositions which will be added to the SAT solver before solving. Results like satisfiability, model, or unsat core are with respect to these additional propositions.

func (*CallParams) Variable added in v0.3.0 

func (p *CallParams) Variable(variable ...f.Variable) *CallParams

Variable sets additional variables which will be added to the SAT solver before solving. Results like satisfiability, model, or unsat core are with respect to these additional variables.

func (*CallParams) WithCore added in v0.3.0 

func (p *CallParams) WithCore() *CallParams

WithCore activates an unsat core computation after the SAT solver call. If the solver is satisfiable, no core will be computed.

func (*CallParams) WithModel added in v0.3.0 

func (p *CallParams) WithModel(variables []f.Variable) *CallParams

WithModel activates model generation after the SAT solver call. The model will be generated only for the given variables. If the solver is unsatisfiable, no model will be generated.

func (*CallParams) WithUPZeros added in v0.3.0 

func (p *CallParams) WithUPZeros() *CallParams

WithUPZeros activates computation of literals propagated at decision level 0 after the SAT solver call. If the solver is unsatisfiable, no literals will be computed.

type CallResult added in v0.3.0 

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

CallResult represents the result of a single call to the SAT solver.

func (CallResult) Aborted added in v0.3.0 

func (r CallResult) Aborted() bool

Aborted reports whether the SAT solver call was aborted by the given handler.

func (CallResult) Model added in v0.3.0 

func (r CallResult) Model() *model.Model

Model returns the model of the last SAT call if the formula was satisfiable and model generation was requested in the call.

func (CallResult) OK added in v0.3.0 

func (r CallResult) OK() bool

OK reports whether the call to the SAT solver yielded a result and was not aborted.

func (CallResult) Sat added in v0.3.0 

func (r CallResult) Sat() bool

Sat reports whether the SAT solver call returned SAT or UNSAT.

func (CallResult) UnsatCore added in v0.3.0 

func (r CallResult) UnsatCore() *explanation.UnsatCore

UnsatCore returns the unsatisfiable core of the last SAT call if the formula was unsatisfiable and unsat core computation was requested in the call.

func (CallResult) UpZeroLits added in v0.3.0 

func (r CallResult) UpZeroLits() []f.Literal

UpZeroLits returns the propagated literals at decision level 0 of the last SAT call if the formula was satisfiable and UpZero computation was requested in the call.

type ClauseMinimization 

type ClauseMinimization byte

ClauseMinimization encodes the different algorithms for minimizing learnt clauses on the solver. 

const (
	ClauseMinNone  ClauseMinimization = iota // no clause minimization
	ClauseMinBasic                           // simple minimization
	ClauseMinDeep                            // recursive deep minimization
)

func (ClauseMinimization) String 

func (i ClauseMinimization) String() string

type Config 

type Config struct {
	ProofGeneration    bool               // record proof generation information on-the-fly
	UseAtMostClauses   bool               // use a special representation of at-most-one clauses
	CNFMethod          CNFMethod          // method for adding CNFs
	ClauseMinimization ClauseMinimization // algorithm for minimizing learnt clauses
	InitialPhase       bool               // initial phase for assigning literals
	LowLevelConfig     *LowLevelConfig    // low level config
}

Config describes the configuration of a SAT solver.

func DefaultConfig 

func DefaultConfig() *Config

DefaultConfig returns the default configuration for a SAT solver configuration.

func (*Config) CNF 

func (c *Config) CNF(cnfMethod CNFMethod) *Config

CNF sets the CNF method on this configuration and returns the config.

func (*Config) ClauseMin 

func (c *Config) ClauseMin(clauseMin ClauseMinimization) *Config

ClauseMin sets the clause minimization method on this configuration and returns the config.

func (*Config) DefaultConfig 

func (c *Config) DefaultConfig() configuration.Config

DefaultConfig returns the default configuration for a SAT solver configuration.

func (*Config) InitPhase added in v0.3.0 

func (c *Config) InitPhase(initPhase bool) *Config

InitPhase sets the initial phase on this configuration and returns the config.

func (*Config) Proofs added in v0.3.0 

func (c *Config) Proofs(proofs bool) *Config

Proofs sets whether proofs should be generated and returns the config.

func (*Config) Sort 

func (c *Config) Sort() configuration.Sort

Sort returns the configuration sort (Sat).

func (*Config) UseAtMost 

func (c *Config) UseAtMost(useAtMost bool) *Config

UseAtMost sets the flat whether at-most clauses should be used and returns the config.

type CoreSolver 

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

CoreSolver represents a core SAT solver.

The LogicNG solver is based on MiniSat, Glucose, and MiniCard. Usually you should not need to interact with the core solver yourself but only via its Solver wrapper.

func NewCoreSolver 

func NewCoreSolver(
	config *Config,
	enqueueFunction func(m *CoreSolver, lit int32, reason *clause),
) *CoreSolver

NewCoreSolver generates a new core SAT solver with the given configuration. An enqueue function to insert new variable assignment decisions must be given. The default is the included UncheckedEnqueue function.

func (*CoreSolver) AddClause 

func (m *CoreSolver) AddClause(ps []int32, proposition f.Proposition) bool

AddClause adds a new clause to the solver.

func (*CoreSolver) Conflict 

func (m *CoreSolver) Conflict() []int32

Conflict returns the current conflict of the solver.

func (*CoreSolver) CreateModel 

func (m *CoreSolver) CreateModel(fac f.Factory, mVec []bool, relevantIndices []int32) *model.Model

CreateModel is used to create a model data-structure from the given model.

func (*CoreSolver) IdxForName 

func (m *CoreSolver) IdxForName(name string) int32

func (*CoreSolver) KnownVariables added in v0.3.0 

func (m *CoreSolver) KnownVariables(fac f.Factory) *f.VarSet

KnownVariables returns the variables currently known by the solver.

func (*CoreSolver) Model 

func (m *CoreSolver) Model() []bool

Model returns the current model of the solver.

func (*CoreSolver) NVars 

func (m *CoreSolver) NVars() int32

NVars returns the number of vars on the solver.

func (*CoreSolver) NewVar 

func (m *CoreSolver) NewVar(sign, dvar bool) int32

NewVar generates a new variable on the solver.

func (*CoreSolver) Solve 

func (m *CoreSolver) Solve(satHandler Handler) (res f.Tristate, ok bool)

Solve solves the formula on the solver with the given handler. Returns the result as tristate and an ok flag which is false when the computation was aborted by the handler.

func (*CoreSolver) SolveWithAssumptions 

func (m *CoreSolver) SolveWithAssumptions(handler Handler, assumptions []int32) (res f.Tristate, ok bool)

SolveWithAssumptions is used to the the formulas on the solver with the given assumptions. Returns the result as tristate and an ok flag which is false when the computation was aborted by the handler.

type DnnfSatSolver 

type DnnfSatSolver interface {
	Factory() f.Factory
	Add(formula f.Formula)
	Start() bool
	Decide(variable int32, phase bool) bool
	UndoDecide(variable int32)
	AtAssertionLevel() bool
	AssertCdLiteral() bool
	NewlyImplied(knownVariables []bool) f.Formula
	VariableIndex(lit f.Literal) int32
	LitForIdx(variable int32) f.Formula
	ValueOf(lit int32) f.Tristate
}

DnnfSatSolver is a special solver used for DNNF generation.

type DnnfSolver 

type DnnfSolver struct {
	*CoreSolver
	// contains filtered or unexported fields
}

func NewDnnfSolver 

func NewDnnfSolver(fac f.Factory, numberOfVariables int) *DnnfSolver

func (*DnnfSolver) Add 

func (m *DnnfSolver) Add(formula f.Formula)

func (*DnnfSolver) AssertCdLiteral 

func (m *DnnfSolver) AssertCdLiteral() bool

func (*DnnfSolver) AtAssertionLevel 

func (m *DnnfSolver) AtAssertionLevel() bool

func (*DnnfSolver) Decide 

func (m *DnnfSolver) Decide(variable int32, phase bool) bool

func (*DnnfSolver) Factory 

func (m *DnnfSolver) Factory() f.Factory

func (*DnnfSolver) LitForIdx 

func (m *DnnfSolver) LitForIdx(variable int32) f.Formula

func (*DnnfSolver) NewlyImplied 

func (m *DnnfSolver) NewlyImplied(knownVariables []bool) f.Formula

func (*DnnfSolver) Start 

func (m *DnnfSolver) Start() bool

func (*DnnfSolver) UndoDecide 

func (m *DnnfSolver) UndoDecide(variable int32)

func (*DnnfSolver) ValueOf 

func (m *DnnfSolver) ValueOf(lit int32) f.Tristate

func (*DnnfSolver) VariableIndex 

func (m *DnnfSolver) VariableIndex(lit f.Literal) int32

type Handler 

type Handler interface {
	handler.Handler
	DetectedConflict() bool
	FinishedSolving()
}

Handler is an interface for SAT handlers which can abort the computation based on the number of conflicts found during the computation.

type LowLevelConfig 

type LowLevelConfig struct {
	VarDecay         float64
	VarInc           float64
	RestartFirst     int
	RestartInc       float64
	ClauseDecay      float64
	LearntsizeFactor float64
	LearntsizeInc    float64

	LBLBDMinimizingClause  int
	LBLBDFrozenClause      int
	LBSizeMinimizingClause int
	FirstReduceDB          int
	SpecialIncReduceDB     int
	IncReduceDB            int
	FactorK                float64
	FactorR                float64
	SizeLBDQueue           int
	SizeTrailQueue         int
	ReduceOnSize           bool
	ReduceOnSizeSize       int
	MaxVarDecay            float64
}

LowLevelConfig describes the low-level parameters of the SAT solver. Usually there is no need to manually change these parameters.

func DefaultLowLevelConfig 

func DefaultLowLevelConfig() *LowLevelConfig

DefaultLowLevelConfig returns a new default configuration of the low-level parameters of the SAT solver.

type OptimizationHandler 

type OptimizationHandler interface {
	handler.Handler
	SatHandler() Handler
	FoundBetterBound(model *model.Model) bool
	SetModel(model *model.Model)
}

OptimizationHandler is an interface for SAT-based optimizations which can abort the computation everytime a better solution is found during the optimization.

type Solver 

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

A Solver is the main interface an external user should interact with a SAT solver. It provides methods for adding and removing formulas to the solver, solving them, extracting models, generating proofs for unsatisfiable formulas, computing backbones, or optimize the formula on the solver.

func NewSolver 

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

NewSolver creates a new SAT solver with the optional configuration.

func (*Solver) Add 

func (s *Solver) Add(formulas ...f.Formula)

Add adds the given formulas to the solver. If the formulas are not already in CNF, they are converted by the CNFMethod configured in the solver's configuration.

func (*Solver) AddIncrementalCC 

func (s *Solver) AddIncrementalCC(cc f.Formula) (*encoding.CCIncrementalData, error)

AddIncrementalCC adds the given constraint as an incremental cardinality constraint to the solver. It returns the incremental data used to tighten the bound of the formula on the solver. Returns with an error if the incremental constraint could not be generated.

func (*Solver) AddProposition 

func (s *Solver) AddProposition(propositions ...f.Proposition)

AddProposition adds the given propositions to the solver. Propositions wrap formulas with some additional information. If generating proofs for unsatisfiable formulas, it is a good idea to use propositions, since otherwise you just get clauses of the internal solver formulas as result.

func (*Solver) Call added in v0.3.0 

func (s *Solver) Call(params ...*CallParams) CallResult

Call calls the SAT solver with the given call parameters. Such a call always performs a solving process. If additional variables / literals / formulas were set, these are added to the solver before solving. When there are only variables and literals this is done by assumption solving, otherwise the solver's save and load state capabilities are used. Depending on the request a model, unsat core, or propagated literals are also computed.

func (*Solver) ComputeBackbone 

func (s *Solver) ComputeBackbone(
	fac f.Factory, variables []f.Variable, backboneSort ...BackboneSort,
) *Backbone

ComputeBackbone computes the positive and negative backbone on the solver.

func (*Solver) ComputeBackboneWithHandler 

func (s *Solver) ComputeBackboneWithHandler(
	fac f.Factory, variables []f.Variable, satHandler Handler, backboneSort ...BackboneSort,
) (*Backbone, bool)

ComputeBackboneWithHandler computes the positive and negative backbone on the solver. The given SAT handler can be used to abort the solver used for the backbone computation.

func (*Solver) CoreSolver 

func (s *Solver) CoreSolver() *CoreSolver

CoreSolver returns the core solver. You should not need this from the outside.

func (*Solver) Factory 

func (s *Solver) Factory() f.Factory

Factory returns the solver's formula factory.

func (*Solver) FormulasOnSolver 

func (s *Solver) FormulasOnSolver() []f.Formula

FormulasOnSolver returns the current formulas on the solver.

Note that this formula is usually syntactically different to the formulas which were actually added to the solver, since the formulas are added as CNF and may be simplified or even removed depending on the state of the solver. Furthermore, the solver might add learnt clauses or propagate literals.

If the formula on the solver is known to be unsatisfiable, this function will add false to the returned set of formulas. However, as long as Sat was not called on the current solver state, the absence of false does not imply that the formula is satisfiable.

Also note that formulas are not added to the solver as soon as the solver is known be unsatisfiable.

func (*Solver) LoadState 

func (s *Solver) LoadState(state *SolverState) error

LoadState loads the given state to the solver. Returns with an error if the state is not valid on the solver.

func (*Solver) Maximize 

func (s *Solver) Maximize(literals []f.Literal, additionalVariables ...f.Variable) *model.Model

Maximize searches for a model on the solver with the maximum of the given literals set to true. The returned model will also include the additional variables.

func (*Solver) MaximizeWithHandler 

func (s *Solver) MaximizeWithHandler(
	literals []f.Literal, optimizationHandler OptimizationHandler, additionalVariables ...f.Variable,
) (mdl *model.Model, ok bool)

MaximizeWithHandler searches for a model on the solver with the maximum of the given literals set to true. The returned model will also include the additional variables. The given optimizationHandler can be used to abort the optimization process. The ok flag is false when the computation was aborted by the handler.

func (*Solver) Minimize 

func (s *Solver) Minimize(literals []f.Literal, additionalVariables ...f.Variable) *model.Model

Minimize searches for a model on the solver with the minimum of the given literals set to true. The returned model will also include the additional variables.

func (*Solver) MinimizeWithHandler 

func (s *Solver) MinimizeWithHandler(
	literals []f.Literal, optimizationHandler OptimizationHandler, additionalVariables ...f.Variable,
) (*model.Model, bool)

MinimizeWithHandler searches for a model on the solver with the minimum of the given literals set to true. The returned model will also include the additional variables. The given optimizationHandler can be used to abort the optimization process. The ok flag is false when the computation was aborted by the handler.

func (*Solver) Sat 

func (s *Solver) Sat() bool

Sat solves the formula on the solver and returns whether it is satisfiable.

func (*Solver) SaveState 

func (s *Solver) SaveState() *SolverState

SaveState saves and returns the current solver state.

func (*Solver) VarOccurrences 

func (s *Solver) VarOccurrences(variables *f.VarSet) map[f.Variable]int

VarOccurrences counts all occurrences of variables on the solver and returns the mapping from variable to number of occurrences. Note that these are usually not the same occurrences as in the original formula, since the formula might have been converted to CNF and/or variables in clauses might have been subsumed. If variables are given as parameters, only the occurrences of these variables are counted, otherwise all variables are considered.

type SolverState 

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

A SolverState can be extracted from the solver by the SaveState method and be loaded again with the LoadState method. It is used to mark certain states of the solver (the loaded formulas and learnt clauses) and be able to come back to them.

type TimeoutHandler 

type TimeoutHandler struct {
	handler.Timeout
}

A TimeoutHandler can be used to abort a 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) DetectedConflict 

func (t *TimeoutHandler) DetectedConflict() bool

DetectedConflict is calles by the solver each time a conflict is detected.

func (*TimeoutHandler) FinishedSolving 

func (t *TimeoutHandler) FinishedSolving()

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

type TimeoutOptimizationHandler 

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

A TimeoutOptimizationHandler can be used to abort a SAT optimization depending on a timeout set beforehand.

func OptimizationHandlerWithTimeout 

func OptimizationHandlerWithTimeout(timeout handler.Timeout) *TimeoutOptimizationHandler

OptimizationHandlerWithTimeout generates a new timeout handler with the given timeout.

func (*TimeoutOptimizationHandler) FoundBetterBound 

func (t *TimeoutOptimizationHandler) FoundBetterBound(model *model.Model) bool

FoundBetterBound is called everytime a better solution bound is found on the SAT solver.

func (*TimeoutOptimizationHandler) IntermediateResult 

func (t *TimeoutOptimizationHandler) IntermediateResult() *model.Model

IntermediateResult returns the last found model of the solver.

func (*TimeoutOptimizationHandler) SatHandler 

func (t *TimeoutOptimizationHandler) SatHandler() Handler

SatHandler returns the SAT handler of the optimization handler.

func (*TimeoutOptimizationHandler) SetModel 

func (t *TimeoutOptimizationHandler) SetModel(model *model.Model)

SetModel is called by the solver with the current model everytime a better solutions bound is found.

type UnitPropagator 

type UnitPropagator struct {
	*CoreSolver
	// contains filtered or unexported fields
}

A UnitPropagator is a special solver used for just propagating unit literals on the solver.

func NewUnitPropagator 

func NewUnitPropagator(fac f.Factory) *UnitPropagator

NewUnitPropagator returns a new unit propagator solver.

func (*UnitPropagator) Add 

func (p *UnitPropagator) Add(formula f.Formula)

Add adds a formula to the unit propagator

func (*UnitPropagator) PropagateFormula 

func (p *UnitPropagator) PropagateFormula() f.Formula

PropagateFormula propagates the units on the formula and returns the result.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.