Documentation ¶
Overview ¶
Package dpll provides a solver for problems of propositional satisfiability (SAT) using the DPLL search algorithm. The specific search implementation used is based on the MiniSat program.
The DPLL solver included runs single-threaded because the DPLL algorithm does not extend simply into multiple threads. Furthermore the memory requirements for multithreaded solving can become extremely high.
Forked packages may be modified to allow for multi-threaded solving using the DPLL type under the hood. Alternatively, a simple way to achieve multi-threaded solving is to run multiple single-threaded solvers (potenially identical solvers with different random seeds) and wait for the first to finish.
Index ¶
- Constants
- func Decode(s Solver, r io.Reader) (ok bool, err error)
- func DecodeFile(s Solver, path string) (ok bool, err error)
- func Luby(y float64, x int) float64
- type CCMinMode
- type Clause
- type ClauseExtra
- type ClauseHeader
- type DPLL
- func (d *DPLL) AddClause(c ...Lit) bool
- func (d *DPLL) ClearInterrupt()
- func (d *DPLL) Conflict() []Lit
- func (d *DPLL) Implies(assumps []Lit) (assign []Lit, ok bool)
- func (d *DPLL) Interrupt()
- func (d *DPLL) Model() []LBool
- func (d *DPLL) NewVar(upol LBool, dvar bool) Var
- func (d *DPLL) NumAssign() int
- func (d *DPLL) NumClause() int
- func (d *DPLL) NumLearn() int
- func (d *DPLL) NumVar() int
- func (d *DPLL) NumVarFree() int
- func (d *DPLL) Okay() bool
- func (d *DPLL) PrintStats()
- func (d *DPLL) ReleaseVar(lit Lit)
- func (d *DPLL) SetDecision(v Var, ok bool)
- func (d *DPLL) SetPolarity(v Var, upol LBool)
- func (d *DPLL) Simplify() bool
- func (d *DPLL) Solve(assump ...Lit) bool
- func (d *DPLL) SolveLimited(assump ...Lit) LBool
- func (d *DPLL) Value(v Var) LBool
- func (d *DPLL) ValueLit(lit Lit) LBool
- func (d *DPLL) ValueLitModel(lit Lit) LBool
- func (d *DPLL) ValueModel(v Var) LBool
- type LBool
- type Lit
- type Mark
- type Opt
- type PhaseSavingLevel
- type Seen
- type Simp
- func (s *Simp) AddClause(ps ...Lit) bool
- func (s *Simp) ClearInterrupt()
- func (s *Simp) Eliminate(turnOffElim bool) bool
- func (s *Simp) FreezeVar(v Var)
- func (s *Simp) Interrupt()
- func (s *Simp) IsEliminated(v Var) bool
- func (s *Simp) NewVar(upol LBool, dvar bool) Var
- func (s *Simp) NumClause() int
- func (s *Simp) NumVar() int
- func (s *Simp) Okay() bool
- func (s *Simp) PrintStats()
- func (s *Simp) ReleaseVar(p Lit)
- func (s *Simp) SetFrozen(v Var, frozen bool)
- func (s *Simp) Solve(assump ...Lit) bool
- func (s *Simp) SolveLimited(assump ...Lit) LBool
- func (s *Simp) SolveLimitedSimp(assump []Lit, presimp bool, turnOffSimp bool) LBool
- func (s *Simp) SolveSimp(assump []Lit, presimp bool, turnOffSimp bool) bool
- func (s *Simp) Thaw()
- type SimpOpt
- type Solver
- type Var
Constants ¶
const ( LTrue = LBool(0) LFalse = LBool(1) LUndef = LBool(2) )
LBool constants
const ( VarUndef = Var(0) LitUndef = Lit(0) VarMax = math.MaxUint32 / 2 )
Helpful constants
Variables ¶
This section is empty.
Functions ¶
func DecodeFile ¶
DecodeFile decodes a CNF problem in DIMACS format from a file at the given path and adds the contained clauses into s.
solver := dpll.New(nil) err := DecodeFile(solver, "problem.dimacs") if err != nil { // ... }
Types ¶
type Clause ¶
type Clause struct { ClauseHeader Lit []Lit }
Clause is a disjunction of literals.
func NewClauseFrom ¶
NewClauseFrom creates a new clause with an inherited ClauseHeader. The extra argument overrides any from ClauseExtra metadata.
func (*Clause) CalcAbstraction ¶
func (c *Clause) CalcAbstraction()
CalcAbstraction computes and stores an abstraction of variables in c like a checksum.
func (*Clause) Strengthen ¶
Strengthen removes p from the list of literals in c.
type ClauseExtra ¶
ClauseExtra are extra fields that may appear in a clause.
type ClauseHeader ¶
type ClauseHeader struct { Mark Mark Learnt bool Relocated bool // this seems unnecessary *ClauseExtra }
ClauseHeader contains Clause metadata that can be inherited from other clauses.
type DPLL ¶
type DPLL struct { Opt // contains filtered or unexported fields }
DPLL is a DPLL satisfiability (SAT) solver. DPLL is a synchronous structure and its variables/methods must not be used concurrently from multiple goroutines. The only methods on DPLL which may be called concurrent with other methods are Interrupt and ClearInterrupt.
func (*DPLL) AddClause ¶
AddClause adds a CNF clause containing the given literals. The literals in c will be sorted.
func (*DPLL) ClearInterrupt ¶
func (d *DPLL) ClearInterrupt()
ClearInterrupt clears the interrupt flag.
func (*DPLL) Conflict ¶
Conflict returns the final, non-empty clause expressed in assumptions if Solve could not find a model. If the last call to Solve found a model then Conflict returns nil.
func (*DPLL) Implies ¶
Implies returns any assignments implied by the given assumptions. If assumptions are plausible then the second return argument of Implies is true. Otherwise Implies returns false if the assumptions result in a contradiction.
func (*DPLL) Interrupt ¶
func (d *DPLL) Interrupt()
Interrupt allows a goroutine to interrupt a long running concurrent search.
func (*DPLL) Model ¶
Model returns assignments found in the last call to Solve. If Solve could not find a model (perhaps under assupmtions) Model returns nil.
func (*DPLL) NumVarFree ¶
NumVarFree returns the number of free variables.
BUG: Computation is not quite correct. Try to calculate right instead of adapting it like below.
func (*DPLL) PrintStats ¶
func (d *DPLL) PrintStats()
PrintStats prints statistics about solving meant to be called after solving has terminated.
func (*DPLL) ReleaseVar ¶
ReleaseVar makes lit true. The caller promises to never refer to variable after ReleaseVar is called.
func (*DPLL) SetDecision ¶
SetDecision declares if a variable should be eligible for selection in the decision heuristic.
func (*DPLL) SetPolarity ¶
SetPolarity declares which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
func (*DPLL) Simplify ¶
Simplify the clause database according to the current top-level assignment. Currently removal of satisfied clauses is all the simplification provided but additional logic may be added in forked implementations.
func (*DPLL) SolveLimited ¶
SolveLimited behaves like Solve but respects resource contraints (?).
func (*DPLL) ValueLitModel ¶
ValueLitModel returns the value of lit in the last model. The last call to Solve must have returned true.
func (*DPLL) ValueModel ¶
ValueModel returns the value of v in the last model. The last call to Solve must have returned true.
type LBool ¶
type LBool uint8
LBool is a lifted boolean value which may be undefined.
type Lit ¶
type Lit uint32
Lit is a propositional literal that encodes possible negation with a variable.
func (Lit) Inverse ¶
Inverse returns a negated literal. If lit is negated the result is a double negated (positive) literal.
func (Lit) IsNeg ¶
IsNeg returns true iff l is a negated literal. If IsUndef returns true then the return value of IsNeg is unspecified.
type Mark ¶
type Mark uint8
Mark is a small scratch space that can be used to flag clauses for application dependent purposes. The DPLL type in this package sets the Mark to signal that a clause should be deleted.
const (
MarkDel Mark = 1 // The marked clause should be deleted
)
Marks that are used by the package's DPLL solver. Use of any Mark constants in not required in a custom solver.
const (
MarkTouch Mark = 2
)
Marks used by the Simp solver
type Opt ¶
type Opt struct { Verbosity int // Log verbosity VarDecay float64 // Activity decay factor ClauseDecay float64 // Activity decay factor RandVarFreq float64 // Frequency with which the decision heuristic tries to choose a random variable RandSeed int64 // Control pseudorandom number sequence NoLubyRestart bool // Do not use the Luby restart sequence CCMin CCMinMode // Control conflict clause minimization PhaseSaving PhaseSavingLevel // Control phase saving RandPol bool // Random polarities for branching heuristics. RandInitAct bool // Initialize variable activities with a small random value. MinLearnt int // Minimum number to set learnt limit to. GarbageFrac float64 // fraction of wasted memory allowed before garbage collection (???) RestartFirst int // The initial restart limit. RestartIncr float64 // Factor by which limit increases with each restart. LearntFraction float64 // Initial limit for learnt clauses as fraction of original clauses. LearntIncr float64 // Factor by which limit for learnt clauses increase with each restart. LearntAdjustConfl int LearntAdjustIncr float64 }
Opt declares options for a DPLL solver.
type PhaseSavingLevel ¶
type PhaseSavingLevel int
PhaseSavingLevel controls the amount of phase saving.
const ( PhaseSavingInvalid PhaseSavingLevel = iota PhaseSavingNone PhaseSavingLimited PhaseSavingFull )
Avalaible levels of phase saving.
type Simp ¶
type Simp struct { SimpOpt // contains filtered or unexported fields }
Simp is a solver that simplifies clauses before solving. Do not call runtime.SetFinalizer on a Simp it will never be garbage collected.
func NewSimp ¶
NewSimp returns a new simplifying solver initialized with the given search and simplification options.
func (*Simp) AddClause ¶
AddClause behaves like DPLL.AddClause. The literals given to AddClause cannot contain eliminated variables.
func (*Simp) ClearInterrupt ¶
func (s *Simp) ClearInterrupt()
ClearInterrupt clears the interrupt flag.
func (*Simp) Eliminate ¶
Eliminate performs simplification and variable elimination turnOffElim should be true the last time that Eliminate is called to free memory used during variable elimination.
func (*Simp) Interrupt ¶
func (s *Simp) Interrupt()
Interrupt allows a goroutine to interrupt a long running concurrent search.
func (*Simp) IsEliminated ¶
IsEliminated returns true if the v was eliminated.
func (*Simp) PrintStats ¶
func (s *Simp) PrintStats()
PrintStats prints solver stats after Solve has returned
func (*Simp) ReleaseVar ¶
ReleaseVar behaves like DPLL.ReleaseVar. An eliminated variable cannot be released.
func (*Simp) SolveLimited ¶
SolveLimited implements Solver
func (*Simp) SolveLimitedSimp ¶
SolveLimitedSimp is like SolveLimited but allows something...
type SimpOpt ¶
type SimpOpt struct { Asymm bool // Shrink clauses by asymmetric branching RCheck bool // Check if a clause is already implied (costly) NoElim bool // Do not perform variable elimination NoExtend bool // When true the caller does not need to know the full model Grow int // Allow a variable elimination step to grow by the given number of clauses ClauseLimit int // Variables are not eliminated if it produces a resolvent with a length above this limit SubsumptionLimit int // Do not check if subsumption against a clause larger than this SimpGarbageFrac float64 // The fraction of wasted memory allowed before a garbage collection is triggered during simplification }
SimpOpt contain options for the Simp solver.
type Solver ¶
type Solver interface { NumVar() int NumClause() int NewVar(upol LBool, dvar bool) Var AddClause(p ...Lit) bool Interrupt() ClearInterrupt() Solve(assumptions ...Lit) bool SolveLimited(assumptions ...Lit) LBool }
Solver is a simple interface for dpll solvers. It is not comprehensive but it is adequate for simple tasks like aggregation/multi-solving and deserialization.