lpb

package
v0.0.0-...-4284493 Latest Latest
Warning

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

 Go to latest Published: Oct 17, 2017 License: Apache-2.0 Imports: 10 Imported by: 2

Documentation

Overview

Package lpb provides solving algorithms for converting a minimal DNF ϕ to a so called linear pseudo-Boolean constraint (LPB).

Introduction to LPBs

A LPB is an expression of the form

Index

Constants

View Source 
const (
	IsFalse dnfFinal = iota
	IsTrue
	NotFinal
)

Variables

View Source 
var ErrNotSymmetric error = errors.New("Found variables that are not symmetric.")

ErrNotSymmetric may be returned by Split if the symmetric property is violated.

Functions

func ComputeMFPs 

func ComputeMFPs(mtps []br.BooleanVector, sortPoints bool) []br.BooleanVector

TODO test this with 0, I don't know what happens to the wait group otherwise, or just never call it with a DNF with zero clauses

func ComputeMTPs 

func ComputeMTPs(phi br.ClauseSet, nbvar int) []br.BooleanVector

ComputeMTPs computes the set of minimal true points of a minimal ϕ. Since ϕ is minimal this is easy: Each clause defines exactly one minimal true point.

func ComputeMaxL 

func ComputeMaxL(patterns []*OccurrencePattern) int

ComputeMaxL computes the max l s.t. the first l patterns are equal.

There are some TODO here.

func FormulateLP 

func FormulateLP(mtps, mfps []br.BooleanVector, nbvar int, winder br.WinderMatrix, tighten TightenMode) (*golp.LP, error)

FormulateLP will formulate the linear program to solve. It will set the following constraings: 1. All variables must be of type int (note that this is really bad for the runtime of lpsolve) 2. For each minimal true point (a1, ..., ak) where ai are the variables that are true a constraint that says that the sum of all variables must be ≥ the degree that is we transform the problem a bit and get: a1 + ... + ak ≥ d ⇔ a1 + ... + ak -d ≥ 0 3. For each maximal false point (a1, ..., ak) where are ai are the variables that are true a constraint that says that the sum of all variables must be < the degree: a1 + ... + ak < d because lpsolve only allows ≤ we transform this to a1 + ... + ak ≤ d - 1 ⇔ a1 + ... + ak - ≤ -1

The additional constraints depend on the mode: If mode is TightenNeighbours we compare all variables w(i) and w(i+1). We know that it must always hold that w(i) ≥ w(i+1), but it could also be w(i) = w(i+1), we find that out by comparing the Winder matrix entries. So we have w(i) ≥ w(i+1) ⇔ w(i) - w(i+1) >= 0 or w(i) - w(i+1) = 0. TODO we can make this easily concurrent

func InitLP 

func InitLP(phi br.ClauseSet, nbvar int, sortMatrix bool) (br.ClauseSet, br.WinderMatrix, []int, []int)

InitLP initializes the lp, that is it creates the Winder matrix for (the renamed) ϕ. It will also compute Renaming and ReverseRenaming as discussed in NewLinearProgram.

It returns first the renamedDNF, the Winder matrix, then Renaming and then ReverseRenaming. If sortMatrix is false the old dnf will be returned.

func RegisterNode 

func RegisterNode(n SplitNode)

RegisterNode will register the node in the context. This method must be called each time a node gets created, so probably in a New... method. It will determine the column and row of the node and set the values on the node.

func SortAll 

func SortAll(patterns []*OccurrencePattern)

SortAll will sort each occurrence pattern in patterns. So don't confuse this method with SortPatterns, this will sort the patterns according to ≽, but each pattern itself must be sorted first with this method.

This method will sort all patterns concurrently.

TODO potential improvement? Sort the clauses according to length first. So when constructing new patterns we don't have to sort again and again. But is this always correct when we split away variables? I don't think so.

func SortPatterns 

func SortPatterns(patterns []*OccurrencePattern)

SortPatterns will sort the occurrence patterns according to importance of the variables. That is the greatest element according to ≽ comes first.

func SplitBoth 

func SplitBoth(n SplitNode, createPatterns, symmetryTest bool) (*SplitResult, *SplitResult)

TODO implement symmetry test.

Types

type AuxNode 

type AuxNode struct {
	*GenericSplitNode
	LValue, LPrime int
}

func NewAuxNode 

func NewAuxNode(lp, up SplitNode, phi br.ClauseSet,
	patterns []*OccurrencePattern, context *TreeContext,
	lValue, lPrime int) *AuxNode

func (*AuxNode) IsFinal 

func (n *AuxNode) IsFinal() bool

func (*AuxNode) Split 

func (n *AuxNode) Split(symmetryTest, cut bool) error

type ColumnHandler 

type ColumnHandler interface {
	Init(t *SplittingTree)
	ChooseCoeff(i Interval, s *SolverState, t *SplittingTree, column int) (LPBCoeff, error)
	ChooseDegree(i Interval, s *SolverState, t *SplittingTree) (LPBCoeff, error)
	HandleColumn(s *SolverState, t *SplittingTree, column int) Interval
}

ColumnHandler is used to choose coefficients (coefficients α s.t. a < α < b) and the degree of the LPB // given an interval (a, b] and additional information such as the tree.

It also must handle the columns with the HandleColumn function. This function takes the column that should be handled next. By handling we mean that it must compute all the intervals in that column and return the values a, b in which we must choose the coefficient (i.e. choose α s.t. a < α < b). If column = 0 we don't have to choose a coefficient, so in this case it may return whatever it wants.

If you need more information than what is stored in the solver state this would be the right place, simply add all the information you need in your own type and make sure they're handled correctly. Of course you can also just implement your own solver at your will if none of the provided ones fits your purposes. When implementing your own chooser you should check the ComputeInterval function that computes the interval for a given node in the tree. MinColumnHandler is an example of such an implementation.

All solving algorithms should make sure that these functions get only called with valid intervals, i.e. there must be a valid coefficient to choose. So implementations here must not check that a < b or something like that. Also it is not possible that we have a conflict of the form b = a + 1, this must be checked in another place.

The Init function gets called each the handler should be initialized for a new tree.

type CombinatorialSolver 

type CombinatorialSolver struct {
	TSolver                                 TreeSolver
	SortPatterns, SortClauses, Cut, SymTest bool
}

CombinatorialSolver implements the DNFToLPB interface by using the combinatorial algorithm as proposed by Smaus.

It depends on a TreeSolver instance that "solves" the constructed tree, i.e. transforms a fully built tree to an LPB.

There are some options you may want to change, see the documentation of NewCombinatorialSolver and NewSplittingTree for details.

It will also rename the variables in the LPB again, that is if the variables were renamed for our algorithm to work it will rename the resulting LPB correctly.

func NewCombinatorialSolver 

func NewCombinatorialSolver(tSolver TreeSolver) *CombinatorialSolver

NewCombinatorialSolver returns a new combinatorial solver given the tree solver.

It sets SortPatterns, SortClauses, Cut and SymTest to true, if that's not what you want just change it after creating the solver. For details of these variables see NewSplittingTree were the options are discussed in more detail.

func (*CombinatorialSolver) Convert 

func (s *CombinatorialSolver) Convert(phi br.ClauseSet, nbvar int) (*LPB, error)

Convert does everything required to compute the LPB: Create the tree, start the tree solver and rename the variables if required.

type DNFToLPB 

type DNFToLPB interface {
	Convert(phi br.ClauseSet, nbvar int) (*LPB, error)
}

DNFToLPB is an interface that provides a single method Convert. This method creates a DNF representation from a DNF ϕ. Note that some solvers might have restrictions on how the DNF must be composed (for example variables must be sorted).

type DNFTree 

type DNFTree struct {
	Content []*DNFTreeNodeContent
	Nbvar   int
}

A DNFTree is a collection of DNFTreeNodeContent objects. The root note is stored on position 0.

func NewDNFTree 

func NewDNFTree(nbvar int) *DNFTree

NewDNFTree returns an empty tree containing no nodes.

func (*DNFTree) BuildTree 

func (tree *DNFTree) BuildTree()

BuildTree will build the whole tree. The root note must be set already.

func (*DNFTree) CreateLeftChild 

func (tree *DNFTree) CreateLeftChild(nodeID int, phi br.ClauseSet, isFinal bool) int

CreateLeftChild creates a new node and sets the left child of nodeID to this node. Returns the ID of the new node.

func (*DNFTree) CreateNodeEntry 

func (tree *DNFTree) CreateNodeEntry(phi br.ClauseSet, depth int, isFinal bool) int

CreateNodeEntry creates a new node given its DNF, depth and the information if that DNF is final.

It will append the new node to the tree and return the index of the new node.

func (*DNFTree) CreateRightChild 

func (tree *DNFTree) CreateRightChild(nodeID int, phi br.ClauseSet, isFinal bool) int

CreateLeftChild creates a new node and sets the right child of nodeID to this node. Returns the ID of the new node.

func (*DNFTree) CreateRoot 

func (tree *DNFTree) CreateRoot(phi br.ClauseSet, isFinal bool) int

CreateRoot creates a root node and returns its ID (should be 0).

func (*DNFTree) IsImplicant 

func (tree *DNFTree) IsImplicant(mtp br.BooleanVector) bool

func (*DNFTree) IsLeaf 

func (tree *DNFTree) IsLeaf(nodeID int) bool

IsLeaf checks if the node is a leaf (has no child nodes).

func (*DNFTree) IsRegular 

func (tree *DNFTree) IsRegular(mtps []br.BooleanVector) bool

func (*DNFTree) Split 

func (tree *DNFTree) Split(nodeID int) (*LPSplitResult, *LPSplitResult)

type DNFTreeNodeContent 

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

DNFTreeNodeContent is a node in the tree we construct for the regularity test. Each node stores a DNF, the information if that DNF is final (i.e. true or false), its depth and two children.

The children are stored by ID, in the tree we store a list of all nodes and can therefore retrieve the actual node.

type GenericSplitNode 

type GenericSplitNode struct {
	LowerParent, UpperParent, LowerChild, UpperChild SplitNode
	Phi                                              br.ClauseSet
	Context                                          *TreeContext
	Column, Row                                      int
	Patterns                                         []*OccurrencePattern
	AlreadySplit                                     bool
}

func NewGenericSplitNode 

func NewGenericSplitNode(lp, up SplitNode, phi br.ClauseSet,
	patterns []*OccurrencePattern, context *TreeContext) *GenericSplitNode

func (*GenericSplitNode) GetColumn 

func (n *GenericSplitNode) GetColumn() int

func (*GenericSplitNode) GetContext 

func (n *GenericSplitNode) GetContext() *TreeContext

func (*GenericSplitNode) GetLowerChild 

func (n *GenericSplitNode) GetLowerChild() SplitNode

func (*GenericSplitNode) GetLowerParent 

func (n *GenericSplitNode) GetLowerParent() SplitNode

func (*GenericSplitNode) GetPatterns 

func (n *GenericSplitNode) GetPatterns() []*OccurrencePattern

func (*GenericSplitNode) GetPhi 

func (n *GenericSplitNode) GetPhi() br.ClauseSet

func (*GenericSplitNode) GetRow 

func (n *GenericSplitNode) GetRow() int

func (*GenericSplitNode) GetUpperChild 

func (n *GenericSplitNode) GetUpperChild() SplitNode

func (*GenericSplitNode) GetUpperParent 

func (n *GenericSplitNode) GetUpperParent() SplitNode

func (*GenericSplitNode) IsAlreadySplit 

func (n *GenericSplitNode) IsAlreadySplit() bool

func (*GenericSplitNode) SetAlreadySplit 

func (n *GenericSplitNode) SetAlreadySplit(val bool)

func (*GenericSplitNode) SetColumn 

func (n *GenericSplitNode) SetColumn(column int)

func (*GenericSplitNode) SetContext 

func (n *GenericSplitNode) SetContext(context *TreeContext)

func (*GenericSplitNode) SetLowerChild 

func (n *GenericSplitNode) SetLowerChild(node SplitNode)

func (*GenericSplitNode) SetLowerParent 

func (n *GenericSplitNode) SetLowerParent(node SplitNode)

func (*GenericSplitNode) SetPatterns 

func (n *GenericSplitNode) SetPatterns(patterns []*OccurrencePattern)

func (*GenericSplitNode) SetPhi 

func (n *GenericSplitNode) SetPhi(phi br.ClauseSet)

func (*GenericSplitNode) SetRow 

func (n *GenericSplitNode) SetRow(row int)

func (*GenericSplitNode) SetUpperChild 

func (n *GenericSplitNode) SetUpperChild(node SplitNode)

func (*GenericSplitNode) SetUpperParent 

func (n *GenericSplitNode) SetUpperParent(node SplitNode)

type Interval 

type Interval struct {
	LHS, RHS LPBCoeff
}

Interval defines an of the form interval (a, b]. a and b are natural numbers, but we allow ∞ and -∞ as well.

We will also used it sometimes if we just need a pair of numbers.

func ComputeInterval 

func ComputeInterval(s *SolverState, t *SplittingTree, column, row int) Interval

ComputeInterval will compute the interval for the node in the specified column and row. For true and false the intervals are easy, for everything else the intervals and coefficient in the next column are looked at and s and b get computed accordingly.

It will also set the interval in s.

func NewInterval 

func NewInterval(lhs, rhs LPBCoeff) Interval

func (Interval) String 

func (i Interval) String() string

type LPB 

type LPB struct {
	Threshold    LPBCoeff
	Coefficients []LPBCoeff
}

LPB represents an LPB of the form a_1 ⋅ x_1 + ... + a_n ⋅ x_n ≥ d Each of the coefficients a_i must be a natural number (positive integer). d can be any integer.

func EmptyLPB 

func EmptyLPB() *LPB

EmptyLPB creates a new LPB with the threshold set to -1 and an empty coefficients list.

func NewLPB 

func NewLPB(threshold LPBCoeff, coefficients []LPBCoeff) *LPB

NewLPB creates a new LPB with the given threshold and coefficients.

func ParseLPB 

func ParseLPB(str string) (*LPB, error)

ParseLPB parses an LPB from the given string, if there is a syntax error it returns an error != nil.

The syntax for parsing LPBs is as follows: First all the coefficients are separated by a space, then the threshold follows, also separated by a space.

So the LPB 2 ⋅ x1 + 1 ⋅ x2 + 1 ⋅ x3 ≥ 2 is represented by "2 1 1 2".

func SolveLP 

func SolveLP(lp *golp.LP) (*LPB, error)

TODO only call if there is at least one variable

func (*LPB) Equals 

func (lpb *LPB) Equals(other *LPB) bool

Equals checks if to LPBs are syntactically equal.

func (*LPB) Rename 

func (lpb *LPB) Rename(reverseRenaming []int) *LPB

TODO test me TODO doc me

func (*LPB) String 

func (lpb *LPB) String() string

func (*LPB) ToDNF 

func (lpb *LPB) ToDNF() br.ClauseSet

ToDNF transforms an LPB to a DNF, algorithm as described in my bachelor thesis.

This function assumes that the LPB is sorted, i.e. the first value in the coefficients is the greatest etc.

type LPBCoeff 

type LPBCoeff int

LPBCoeff is the type used for integers in an LPB, i.e. for coefficients and the threshold.

There are to reasons (I see) not to use ints directly: 1. We can change the type to a float or something else if needed be 2. We need ∞ and -∞ later, this is not directly possible with an int so we kind of wrap this type around ints. Important note: LPBCoeff is intended to be positive always. We will use negative values to indicate ∞ and -∞ (see constants later).

If you want to print them nicely (for example with Printf) don't use %d as a specifier but %s, the String() method will format it correctly.

Also you can still use some int methods like +, but if one of the values is ∞ or -∞ this will not give you what you want. Use Add(), Sub() and Mult() instead. 

const (
	PositiveInfinity LPBCoeff = LPBCoeff(-1) // Value for ∞
	NegativeInfinity LPBCoeff = LPBCoeff(-2) // Value for -∞
)

func CoeffMax 

func CoeffMax(val1, val2 LPBCoeff) LPBCoeff

CoeffMax returns the maximum of both arguments.

func CoeffMin 

func CoeffMin(val1, val2 LPBCoeff) LPBCoeff

CoeffMin returns the minimum of both arguments.

func (LPBCoeff) Add 

func (val1 LPBCoeff) Add(val2 LPBCoeff) LPBCoeff

Add adds two LPBCoeff elements and returns the sum. If val1 one is ∞ or -∞ this value is returned, otherwise if it is a number the sum will be returned (if val2 is ∞ or -∞ this value gets returned as well).

func (LPBCoeff) Compare 

func (val1 LPBCoeff) Compare(val2 LPBCoeff) int

Compare compares two values and returns 0 iff val1 = val2, -1 iff val1 < val2 and 1 iff val1 > val2.

∞ and -∞ are handled in the following way: ∞ = ∞ and -∞ = -∞. No value is greater than ∞ and no value is smaller than -∞.

func (LPBCoeff) Equals 

func (val1 LPBCoeff) Equals(val2 LPBCoeff) bool

Equals returns true iff val1 == val2. This is the case iff val1.Compare(val2) == 0.

func (LPBCoeff) Greater 

func (val1 LPBCoeff) Greater(val2 LPBCoeff) bool

Greater returns true iff val1 > val2. This is the case iff val1.Compare(val2) > 0.

func (LPBCoeff) Lesser 

func (val1 LPBCoeff) Lesser(val2 LPBCoeff) bool

Lesser returns true iff val1 < val2. This is the case iff val.Compare(val2) < 0.

func (LPBCoeff) Mult 

func (val1 LPBCoeff) Mult(val2 LPBCoeff) LPBCoeff

Mult computes val1 * val2. If either of the value is ∞ or -∞ this value is returned.

func (LPBCoeff) String 

func (val LPBCoeff) String() string

func (LPBCoeff) Sub 

func (val1 LPBCoeff) Sub(val2 LPBCoeff) LPBCoeff

Sub computes val1 - val2. If neither is ∞ or -∞ it returns val1 - val2. If val1 is ∞ or -∞ this value is returned. If val1 is a number and val2 is ∞ it returns -∞, if val2 is -∞ it returns ∞. It will however not test if the result is still positive! So check this first if you are not sure.

type LPSolver 

type LPSolver struct {
	SortMatrix, SortClauses, RegTest bool
	Tighten                          TightenMode
}

LPSolver implements the DNFToLPB interface by using the linear programming algorithm.

Ther are some options you can change, see NewLPSolver, NewLinearProgram and NewLinearProgram.Solve for more details.

It will also rename the variables in the LPB again, that is if the variables were renamed for our algorithm to work it will rename the resulting LPB correctly.

func NewLPSolver 

func NewLPSolver(tighten TightenMode) *LPSolver

NewLPSolver returns a new LPSolver with SortMatrix, SortClauses and RegTest set to true.

For details of these variables see NewLinearProgram and LinearProgram.Solve for more details.

tighten describes how many additional constraints should be added to the lp, see TightenMode documentation for more details.

func (*LPSolver) Convert 

func (s *LPSolver) Convert(phi br.ClauseSet, nbvar int) (*LPB, error)

Convert does everything required to compute the LPB: It sets up the program and tries to solve it. It will also undo the renaming if required.

type LPSplitResult 

type LPSplitResult struct {
	Final bool
	Phi   br.ClauseSet
}

type LinearProgram 

type LinearProgram struct {
	Renaming, ReverseRenaming []int
	Tree                      *DNFTree
	Winder                    br.WinderMatrix
	LP                        *golp.LP
	MFPs, MTPs                []br.BooleanVector
	Phi                       br.ClauseSet
	Nbvar                     int
}

func NewLinearProgram 

func NewLinearProgram(phi br.ClauseSet, nbvar int, sortMatrix, sortClauses bool) *LinearProgram

NewLinearProgram creates a new lp given the DNF ϕ.

It will however not create the actual program or the tree, this must be done somewhere else, it only creates the root node.

Important note: For our algorithm to work the variables must be sorted according to their importance. Since this is not always the case (only during testing and some very special cases) this method will do this for you, i.e. it will create the winder matrix and then rename all variables accordingly. So the DNF we store in the root node is the renamed DNF. But we also store the mapping that caused this renaming in the field Renaming. This slice stores for each "old" variable the id in the new tree, i.e. a lookup tree.Renaming[id] gives you the id of the variable in the new tree. The reverse mapping, i.e. new variable → old variable is stored in ReverseRenaming.

If you don't need the renaming set sortMatrix to false, in this case the matrix will work properly but the variables don't get sorted. That is only set it to false if you know that the ordering of the variables is already correct. Renaming and ReverseRenaming will be set to nil in this case.

Also the clauses in the DNF must be sorted in increasing order. If you don't want the clauses to get sorted set sortClauses to false. Of course this only makes sense if also sortMatrix is set to false, otherwise the new dnf might not be sorted. This functions will sort them in this case nonetheless.

The variables in the DNF have to be 0 <= v < nbar (so nbvar must be correct and variables start with 0). Also each variable should appear at least once in the DNF, what happens otherwise is not tested yet.

func (LinearProgram) Solve 

func (lp LinearProgram) Solve(tighten TightenMode, regTest bool) (*LPB, error)

type MainNode 

type MainNode struct {
	*GenericSplitNode
	MaxL  int
	Final bool
}

func NewMainNode 

func NewMainNode(lp, up SplitNode, phi br.ClauseSet,
	patterns []*OccurrencePattern, context *TreeContext) *MainNode

func (*MainNode) IsFinal 

func (n *MainNode) IsFinal() bool

func (*MainNode) Split 

func (n *MainNode) Split(symmetryTest, cut bool) error

TODO JGS: cut is being ignored because I don't really understand it :)

type MinColumnHandler 

type MinColumnHandler struct{}

func NewMinColumnHandler 

func NewMinColumnHandler() MinColumnHandler

func (MinColumnHandler) ChooseCoeff 

func (handler MinColumnHandler) ChooseCoeff(i Interval, s *SolverState, t *SplittingTree, column int) (LPBCoeff, error)

func (MinColumnHandler) ChooseDegree 

func (handler MinColumnHandler) ChooseDegree(i Interval, s *SolverState, t *SplittingTree) (LPBCoeff, error)

func (MinColumnHandler) HandleColumn 

func (handler MinColumnHandler) HandleColumn(s *SolverState, t *SplittingTree, column int) Interval

func (MinColumnHandler) Init 

func (handler MinColumnHandler) Init(t *SplittingTree)

type OccurrencePattern 

type OccurrencePattern struct {
	// The actual pattern
	Occurrences []int
	// VariableId is the id of the variable, this is only needed in the first run!
	// When we create OPs for DNFs in the second or later column this value will
	// not make sense! It only makes sense in the first column of the tree.
	VariableId int
}

OccurrencePattern is a multiset of sorted integer values. For a DNF ϕ and a variable x in ϕ the occurrence pattern is defined as the multiset having one occurrence of n for each clause of length n in ϕ that contains x. (Definition 6.3 in On Boolean Functions Encodable as a Single Linear Pseudo-Boolean Constraint by Jan-Georg Smaus) They're implemented as a slice of integer values, we also store the id of the variable x.

Occurrence patterns are sorted multisets, we first construct the whole pattern and then sort it. So the Insert method does not (re)sort the OP.

Note that occurrence patterns are not safe for concurrent use (don't insert). from multiple goroutines.

func EmptyOccurrencePattern 

func EmptyOccurrencePattern(initialCapacity int) *OccurrencePattern

EmptyOccurrencePattern greates a new occurrence pattern for the variable and the slice of the numbers is initialized with the specified capacity.

func EmptyPatterns 

func EmptyPatterns(size int) []*OccurrencePattern

EmptyPatterns returns a slice of occurrence pattern of the given size, each one is initialized to an empty pattern.

func OPFromDNF 

func OPFromDNF(phi br.ClauseSet, nbvar int) []*OccurrencePattern

OPFromDNF will build the occurrence patterns for the DNF ϕ. The number of variables (nbvar) must be known in advance. No variable in the DNF must be >= nbvar, this will not be checked though!

This function returns a slice of length nbvar where the OP for variable x is stored on position x.

This method does not sort the patterns (neither the patterns themselves or the whole pattern slice)! You must first make sure that all the patterns are sorted (the elements in each pattern), see SortAll for this. Then you must make sure that the elements are sorted according the ≽ order, see SortPatterns for this.

func OPFromDNFShift 

func OPFromDNFShift(phi br.ClauseSet, nbvar, column int) []*OccurrencePattern

OPFromDNFShift will build the occurrence patterns for the DNF ϕ.

This is a rather internal method, but I exported it for testing and playing around. If you want to build the patterns for a whole DNF (no splitting) or something use OPFromDNF.

nbvar is the number of variables in the whole dnf, this means if you already used split some variables you always use the nbvar for the original DNF!

column refers to the column this DNF is created for in the tree. So if we call Split on a node in column zero (the first one) column will be one because we create the successors that are stored in column one (the second one)

func (*OccurrencePattern) CompareTo 

func (op *OccurrencePattern) CompareTo(other *OccurrencePattern) int

CompareTo compares the occurrence pattern to another one. It returns 0 iff op == other, -1 iff op ≺ other and 1 iff op ≻ other.

func (*OccurrencePattern) Insert 

func (op *OccurrencePattern) Insert(val int)

Insert adds the value to the pattern. It will not (re)sort the array.

func (*OccurrencePattern) Sort 

func (op *OccurrencePattern) Sort()

Sort sorts the occurrences in increasing order.

func (*OccurrencePattern) String 

func (op *OccurrencePattern) String() string

type SimpleTreeSolver 

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

func NewSimpleTreeSolver 

func NewSimpleTreeSolver(handler ColumnHandler) SimpleTreeSolver

func (SimpleTreeSolver) Solve 

func (solver SimpleTreeSolver) Solve(t *SplittingTree) (*LPB, error)

type SolverState 

type SolverState struct {
	Coefficients    []LPBCoeff   // The coefficients for each column, must be multiplied with the coeff factor.
	CoeffSums       []LPBCoeff   // Stores the sum of all coefficients including column k, gets updated in SetCoeff
	Intervals       [][]Interval // For each column contains all intervals in the tree
	IntervalFactors []int        // Factor intervals in a certain column must be multiplied with.
}

SolverState provides the solver with certain information about the current search space, like current coefficients and so on.

func NewSolverState 

func NewSolverState(t *SplittingTree) *SolverState

NewSolverState a new solver space that sets all factors to one and intervals big enough to contain all intervals for the tree.

func (*SolverState) GetInterval 

func (s *SolverState) GetInterval(column, row int) Interval

GetInterval returns the current interval value taking into consideration the intervals for that column. Note that a new interval gets returned, so chaning the value you receive won't change anything here.

func (*SolverState) GetSumAfter 

func (s *SolverState) GetSumAfter(column int) LPBCoeff

GetSumAfter returns the sum of all coefficients *after* the specified column, so not including this column.

func (*SolverState) SetCoeff 

func (s *SolverState) SetCoeff(column int, val LPBCoeff)

SetCoeff sets the coefficient in the specified column, also updating the coefficient sum in that column.

func (*SolverState) SolveConflict 

func (s *SolverState) SolveConflict(column int)

SolveConflict solves a conflict of the form α < α_{k+1} < α + 1. It simply doubles the whole system (intervals and coefficients).

If we are forced to solve a conflict in column k this means that we have to double all the intervals in column k and all following and all coefficients starting in column k + 1 (we haven't set a coefficient for k yet).

type SplitNode 

type SplitNode interface {
	Split(symmetryTest, cut bool) error

	IsFinal() bool
	GetLowerParent() SplitNode
	SetLowerParent(node SplitNode)
	GetUpperParent() SplitNode
	SetUpperParent(node SplitNode)
	GetLowerChild() SplitNode
	SetLowerChild(node SplitNode)
	GetUpperChild() SplitNode
	SetUpperChild(node SplitNode)
	GetPhi() br.ClauseSet //
	GetColumn() int       //
	SetColumn(column int) //
	GetRow() int
	SetRow(row int)
	GetContext() *TreeContext          //
	GetPatterns() []*OccurrencePattern //
	IsAlreadySplit() bool
	SetAlreadySplit(val bool)
}

type SplitResult 

type SplitResult struct {
	Final       bool
	Phi         br.ClauseSet
	Occurrences []*OccurrencePattern
}

func NewSplitResult 

func NewSplitResult(final bool, phi br.ClauseSet, occurrences []*OccurrencePattern) *SplitResult

func Split 

func Split(n SplitNode, k int, createPatterns, symmetryTest bool) *SplitResult

Split will split away the next variable. The variable that must be split away is given by the column of the node (in column k we split away variable k).

If createPatterns is true the occurrence patterns will be created

TODO implement symmetry test.

type SplittingTree 

type SplittingTree struct {
	Root                      *MainNode    // The root node
	Context                   *TreeContext // The context of the tree
	Renaming, ReverseRenaming []int        // See NewSplittingTree
	SymTest                   bool         // If true the test for symmetric variables is performed
	Cut                       bool         // TODO JGS Not entirely sure what this is supposed to mean
}

SplittingTree represents the tree for a DNF.

func NewSplittingTree 

func NewSplittingTree(phi br.ClauseSet, nbvar int, sortPatterns, sortClauses bool) *SplittingTree

NewSplittingTree creates a new tree given the DNF ϕ.

It will however not create the whole tree, this must be done somewhere else, it only creates the root node.

Important note: For our algorithm to work the variables must be sorted according to their importance. Since this is not always the case (only during testing and some very special cases) this method will do this for you, i.e. it will create the occurrence patterns and then rename all variables accordingly. So the DNF we store in the root node is the renamed DNF. But we also store the mapping that caused this renaming in the tree in the field Renaming. This slice stores for each "old" variable the id in the new tree, i.e. a lookup tree.Renaming[id] gives you the id of the variable in the new tree. The reverse mapping, i.e. new variable → old variable is stored in ReverseRenaming.

If you don't need the renaming set sortPatterns to false, in this case the patterns will work properly but the patterns don't get sorted. That is only set it to false if you know that the ordering of the variables is already correct. Renaming and ReverseRenaming will be set to nil in this case.

Also the clauses in the DNF must be sorted in increasing order. If you don't want the clauses to get sorted set sortClauses to false. Of course this only makes sense if also sortPatterns is set to false, otherwise the new dnf might not be sorted. This functions will sort them in this case nonetheless.

The variables in the DNF have to be 0 <= v < nbar (so nbvar must be correct and variables start with 0). Also each variable should appear at least once in the DNF, what happens otherwise is not tested yet.

By default Cut and SymTest are set to true, so if you want to debug better set it by hand before calling CreateTree.

func (*SplittingTree) CreateTree 

func (t *SplittingTree) CreateTree() error

CreateTree creates the whole splitting tree and returns ErrNotSymmetric if the symmetric property was violated.

Think about a concurrent approach?

type TightenMode 

type TightenMode int

TightenMode describes different modes to tighten the linear program before solving it.

There are three different modes described below. 

const (
	TightenNone       TightenMode = iota // Add only constraings necessary for solving the problem
	TightenNeighbours                    // Add also constraings between variables x(i) and x(i + 1)
	TightenAll                           // Add additional constraints between all variable pairs
)

type TreeContext 

type TreeContext struct {
	Tree  [][]SplitNode
	Nbvar int
}

func NewTreeContext 

func NewTreeContext(nbvar int) *TreeContext

func (*TreeContext) AddNode 

func (c *TreeContext) AddNode(node SplitNode) int

type TreeSolver 

type TreeSolver interface {
	Solve(t *SplittingTree) (*LPB, error)
}

TreeSolver is an interface for everything that can transform a tree into an LPB or returns an error if that is not possible.

The tree is not fully created when passed to Solve, i.e. it has to be created with CreateTree.

func NewMinSolver 

func NewMinSolver() TreeSolver

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.