dpll

package module
v0.0.0-...-9f975b8 Latest Latest
Warning

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

 Go to latest Published: Mar 23, 2016 License: MIT Imports: 12 Imported by: 0

README

#dpll GoDoc Build Status

DPLL satisfiability solver based on MiniSat.

The goal of project is to provide a basic and somewhat efficient SAT solving package that can be used for constraint solving in practical Go applications. A command line program is provided though it should not be expected to outperform MiniSat.

Like MiniSat the dpll package can be thought of as a core implementation suitable for hacking on. Updates to the dpll package itself should be limited to bug fixes and performance tweaks.

##License (MIT)

Copyright 2016 Bryan Matsuo

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to conditions specified in the LICENSE file distributed with this software.

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

View Source 
const (
	LTrue  = LBool(0)
	LFalse = LBool(1)
	LUndef = LBool(2)
)

LBool constants

View Source 
const (
	VarUndef = Var(0)
	LitUndef = Lit(0)

	VarMax = math.MaxUint32 / 2
)

Helpful constants

Variables

This section is empty.

Functions

func Decode 

func Decode(s Solver, r io.Reader) (ok bool, err error)

Decode is like DecodeFile. But, Decode reads a DIMACS formatted byte stream from r.

func DecodeFile 

func DecodeFile(s Solver, path string) (ok bool, err error)

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 {
	// ...
}

func Luby 

func Luby(y float64, x int) float64

Luby uses the Luby algorithm to generate a restart sequence from factor y and current number of restarts x. 

Finite subsequences of the Luby-sequence:
0: 1
1: 1 1 2
2: 1 1 2 1 1 2 4
3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
...

Types

type CCMinMode 

type CCMinMode int

CCMinMode controls conflict clause minimization. 

const (
	CCMinInvalid CCMinMode = iota
	CCMinNone
	CCMinBasic
	CCMinDeep
)

Available conflict clause minimization modes.

type Clause 

type Clause struct {
	ClauseHeader
	Lit []Lit
}

Clause is a disjunction of literals.

func NewClause 

func NewClause(ps []Lit, extra bool, learnt bool) *Clause

NewClause creates a new clause containing a copy of ps.

func NewClauseFrom 

func NewClauseFrom(from *Clause, extra bool) *Clause

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) Len 

func (c *Clause) Len() int

Len returns the number of literals in c.

func (*Clause) Strengthen 

func (c *Clause) Strengthen(p Lit) bool

Strengthen removes p from the list of literals in c.

func (*Clause) Subsumes 

func (c *Clause) Subsumes(c2 *Clause) (ok bool, p Lit)

Subsumes checks if c subsumes c2 and if it can be used to simplify c2 by subsumption resolution. If Subsumes returns true and p is not LitUndef then p can be removed from c2.

type ClauseExtra 

type ClauseExtra struct {
	Activity    float64
	Abstraction uint32
}

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 New 

func New(opt *Opt) *DPLL

New initializes and returns a new SAT solver.

func (*DPLL) AddClause 

func (d *DPLL) AddClause(c ...Lit) bool

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 

func (d *DPLL) Conflict() []Lit

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 

func (d *DPLL) Implies(assumps []Lit) (assign []Lit, ok bool)

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 

func (d *DPLL) Model() []LBool

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) NewVar 

func (d *DPLL) NewVar(upol LBool, dvar bool) Var

NewVar adds a new variable. The parameters specify variable mode.

func (*DPLL) NumAssign 

func (d *DPLL) NumAssign() int

NumAssign returns the number of assigned literals.

func (*DPLL) NumClause 

func (d *DPLL) NumClause() int

NumClause returns the number of original clauses.

func (*DPLL) NumLearn 

func (d *DPLL) NumLearn() int

NumLearn returns the number of learnt clauses.

func (*DPLL) NumVar 

func (d *DPLL) NumVar() int

NumVar returns the number of variables.

func (*DPLL) NumVarFree 

func (d *DPLL) NumVarFree() int

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) Okay 

func (d *DPLL) Okay() bool

Okay returns false if the solver is in a conflicting state.

func (*DPLL) PrintStats 

func (d *DPLL) PrintStats()

PrintStats prints statistics about solving meant to be called after solving has terminated.

func (*DPLL) ReleaseVar 

func (d *DPLL) ReleaseVar(lit Lit)

ReleaseVar makes lit true. The caller promises to never refer to variable after ReleaseVar is called.

func (*DPLL) SetDecision 

func (d *DPLL) SetDecision(v Var, ok bool)

SetDecision declares if a variable should be eligible for selection in the decision heuristic.

func (*DPLL) SetPolarity 

func (d *DPLL) SetPolarity(v Var, upol LBool)

SetPolarity declares which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.

func (*DPLL) Simplify 

func (d *DPLL) Simplify() bool

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) Solve 

func (d *DPLL) Solve(assump ...Lit) bool

Solve searches for a model that respects the given assupmtions.

func (*DPLL) SolveLimited 

func (d *DPLL) SolveLimited(assump ...Lit) LBool

SolveLimited behaves like Solve but respects resource contraints (?).

func (*DPLL) Value 

func (d *DPLL) Value(v Var) LBool

Value returns the current value of v.

func (*DPLL) ValueLit 

func (d *DPLL) ValueLit(lit Lit) LBool

ValueLit returns the current value of lit.

func (*DPLL) ValueLitModel 

func (d *DPLL) ValueLitModel(lit Lit) LBool

ValueLitModel returns the value of lit in the last model. The last call to Solve must have returned true.

func (*DPLL) ValueModel 

func (d *DPLL) ValueModel(v Var) LBool

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.

func LiftBool 

func LiftBool(b bool) LBool

LiftBool returns LTrue or LFalse if b is true or false respectively.

func (LBool) And 

func (b LBool) And(b2 LBool) LBool

And returns the conjunction of b and b2.

func (LBool) Equal 

func (b LBool) Equal(b2 LBool) bool

Equal returns true iff b and b2 are equivalent.

func (LBool) IsFalse 

func (b LBool) IsFalse() bool

IsFalse returns true if b is equivalent to LFalse

func (LBool) IsTrue 

func (b LBool) IsTrue() bool

IsTrue returns true if b is equivalent to LTrue

func (LBool) IsUndef 

func (b LBool) IsUndef() bool

IsUndef returns true if b is equivalent to LUndef

func (LBool) Or 

func (b LBool) Or(b2 LBool) LBool

Or returns the disjunction of b and b2.

func (LBool) String 

func (b LBool) String() string

String returns the string representation of an LBool

func (LBool) Xor 

func (b LBool) Xor(b2 bool) LBool

Xor returns the exclusive or of b and b2.

type Lit 

type Lit uint32

Lit is a propositional literal that encodes possible negation with a variable.

func Literal 

func Literal(v Var, neg bool) Lit

Literal creates a Lit from v. If neg is true then the literal is negated.

func LiteralInt 

func LiteralInt(x int) Lit

LiteralInt creates a Lit from integer x.

func (Lit) Inverse 

func (l Lit) Inverse() Lit

Inverse returns a negated literal. If lit is negated the result is a double negated (positive) literal.

func (Lit) IsNeg 

func (l Lit) IsNeg() bool

IsNeg returns true iff l is a negated literal. If IsUndef returns true then the return value of IsNeg is unspecified.

func (Lit) IsUndef 

func (l Lit) IsUndef() bool

IsUndef returns true if l is undefined.

func (Lit) SharesVar 

func (l Lit) SharesVar(l2 Lit) bool

SharesVar returns true if l.Var() and l2.Var() are equal.

func (Lit) String 

func (l Lit) String() string

String returns the string representation of l. For example "1", "-2", or "0".

func (Lit) Var 

func (l Lit) Var() Var

Var returns the variable in l. If IsUndef returns is true Var returns an undefined variable (its IsUndef method will return true).

func (Lit) Xor 

func (l Lit) Xor(b bool) Lit

Xor returns a literal of l.Var() that is negated iff l.IsNeg() XOR b.

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

func (Mark) HasAll 

func (m Mark) HasAll(mm Mark) bool

HasAll returns true if and only if m contains all of the bits marked in mm.

func (Mark) HasAny 

func (m Mark) HasAny(mm Mark) bool

HasAny returns true if and only if m contains any of the bits marked in mm.

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 Seen 

type Seen uint8

Seen marks how a variable was seen 

const (
	SeenUndef Seen = iota
	SeenSource
	SeenRemovable
	SeenFailed
)

Avaible methods of being seen.

func (Seen) IsSeen 

func (s Seen) IsSeen() bool

IsSeen returns true if s is non-zero

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 

func NewSimp(opt *Opt, simpOpt *SimpOpt) *Simp

NewSimp returns a new simplifying solver initialized with the given search and simplification options.

func (*Simp) AddClause 

func (s *Simp) AddClause(ps ...Lit) bool

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 

func (s *Simp) Eliminate(turnOffElim bool) bool

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) FreezeVar 

func (s *Simp) FreezeVar(v Var)

FreezeVar is an alternative to SetFrozen

func (*Simp) Interrupt 

func (s *Simp) Interrupt()

Interrupt allows a goroutine to interrupt a long running concurrent search.

func (*Simp) IsEliminated 

func (s *Simp) IsEliminated(v Var) bool

IsEliminated returns true if the v was eliminated.

func (*Simp) NewVar 

func (s *Simp) NewVar(upol LBool, dvar bool) Var

NewVar behaves like DPLL.NewVar.

func (*Simp) NumClause 

func (s *Simp) NumClause() int

NumClause implements Solver

func (*Simp) NumVar 

func (s *Simp) NumVar() int

NumVar implements Solver

func (*Simp) Okay 

func (s *Simp) Okay() bool

Okay returns true if s hasn't yet found a contradiction

func (*Simp) PrintStats 

func (s *Simp) PrintStats()

PrintStats prints solver stats after Solve has returned

func (*Simp) ReleaseVar 

func (s *Simp) ReleaseVar(p Lit)

ReleaseVar behaves like DPLL.ReleaseVar. An eliminated variable cannot be released.

func (*Simp) SetFrozen 

func (s *Simp) SetFrozen(v Var, frozen bool)

SetFrozen lets variables be frozen, preventing them from being eliminated.

func (*Simp) Solve 

func (s *Simp) Solve(assump ...Lit) bool

Solve implements Solver

func (*Simp) SolveLimited 

func (s *Simp) SolveLimited(assump ...Lit) LBool

SolveLimited implements Solver

func (*Simp) SolveLimitedSimp 

func (s *Simp) SolveLimitedSimp(assump []Lit, presimp bool, turnOffSimp bool) LBool

SolveLimitedSimp is like SolveLimited but allows something...

func (*Simp) SolveSimp 

func (s *Simp) SolveSimp(assump []Lit, presimp bool, turnOffSimp bool) bool

SolveSimp is like Solve but allows something...

func (*Simp) Thaw 

func (s *Simp) Thaw()

Thaw unfreezes all variables

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.

type Var 

type Var uint32

Var is a propositional variable. Variables begin at 1.

func (Var) IsUndef 

func (v Var) IsUndef() bool

IsUndef returns true if v is undefined.

Source Files

View all Source files

Directories

Path Synopsis
cmd
dpll-go
dpll-simp
Package dimacs implements reading and writing of DIMACS format files for satisfiability problem statement.
 Package dimacs implements reading and writing of DIMACS format files for satisfiability problem statement.

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.