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
- Variables
- func ComputeMFPs(mtps []br.BooleanVector, sortPoints bool) []br.BooleanVector
- func ComputeMTPs(phi br.ClauseSet, nbvar int) []br.BooleanVector
- func ComputeMaxL(patterns []*OccurrencePattern) int
- func FormulateLP(mtps, mfps []br.BooleanVector, nbvar int, winder br.WinderMatrix, ...) (*golp.LP, error)
- func InitLP(phi br.ClauseSet, nbvar int, sortMatrix bool) (br.ClauseSet, br.WinderMatrix, []int, []int)
- func RegisterNode(n SplitNode)
- func SortAll(patterns []*OccurrencePattern)
- func SortPatterns(patterns []*OccurrencePattern)
- func SplitBoth(n SplitNode, createPatterns, symmetryTest bool) (*SplitResult, *SplitResult)
- type AuxNode
- type ColumnHandler
- type CombinatorialSolver
- type DNFToLPB
- type DNFTree
- func (tree *DNFTree) BuildTree()
- func (tree *DNFTree) CreateLeftChild(nodeID int, phi br.ClauseSet, isFinal bool) int
- func (tree *DNFTree) CreateNodeEntry(phi br.ClauseSet, depth int, isFinal bool) int
- func (tree *DNFTree) CreateRightChild(nodeID int, phi br.ClauseSet, isFinal bool) int
- func (tree *DNFTree) CreateRoot(phi br.ClauseSet, isFinal bool) int
- func (tree *DNFTree) IsImplicant(mtp br.BooleanVector) bool
- func (tree *DNFTree) IsLeaf(nodeID int) bool
- func (tree *DNFTree) IsRegular(mtps []br.BooleanVector) bool
- func (tree *DNFTree) Split(nodeID int) (*LPSplitResult, *LPSplitResult)
- type DNFTreeNodeContent
- type GenericSplitNode
- func (n *GenericSplitNode) GetColumn() int
- func (n *GenericSplitNode) GetContext() *TreeContext
- func (n *GenericSplitNode) GetLowerChild() SplitNode
- func (n *GenericSplitNode) GetLowerParent() SplitNode
- func (n *GenericSplitNode) GetPatterns() []*OccurrencePattern
- func (n *GenericSplitNode) GetPhi() br.ClauseSet
- func (n *GenericSplitNode) GetRow() int
- func (n *GenericSplitNode) GetUpperChild() SplitNode
- func (n *GenericSplitNode) GetUpperParent() SplitNode
- func (n *GenericSplitNode) IsAlreadySplit() bool
- func (n *GenericSplitNode) SetAlreadySplit(val bool)
- func (n *GenericSplitNode) SetColumn(column int)
- func (n *GenericSplitNode) SetContext(context *TreeContext)
- func (n *GenericSplitNode) SetLowerChild(node SplitNode)
- func (n *GenericSplitNode) SetLowerParent(node SplitNode)
- func (n *GenericSplitNode) SetPatterns(patterns []*OccurrencePattern)
- func (n *GenericSplitNode) SetPhi(phi br.ClauseSet)
- func (n *GenericSplitNode) SetRow(row int)
- func (n *GenericSplitNode) SetUpperChild(node SplitNode)
- func (n *GenericSplitNode) SetUpperParent(node SplitNode)
- type Interval
- type LPB
- type LPBCoeff
- func (val1 LPBCoeff) Add(val2 LPBCoeff) LPBCoeff
- func (val1 LPBCoeff) Compare(val2 LPBCoeff) int
- func (val1 LPBCoeff) Equals(val2 LPBCoeff) bool
- func (val1 LPBCoeff) Greater(val2 LPBCoeff) bool
- func (val1 LPBCoeff) Lesser(val2 LPBCoeff) bool
- func (val1 LPBCoeff) Mult(val2 LPBCoeff) LPBCoeff
- func (val LPBCoeff) String() string
- func (val1 LPBCoeff) Sub(val2 LPBCoeff) LPBCoeff
- type LPSolver
- type LPSplitResult
- type LinearProgram
- type MainNode
- type MinColumnHandler
- func (handler MinColumnHandler) ChooseCoeff(i Interval, s *SolverState, t *SplittingTree, column int) (LPBCoeff, error)
- func (handler MinColumnHandler) ChooseDegree(i Interval, s *SolverState, t *SplittingTree) (LPBCoeff, error)
- func (handler MinColumnHandler) HandleColumn(s *SolverState, t *SplittingTree, column int) Interval
- func (handler MinColumnHandler) Init(t *SplittingTree)
- type OccurrencePattern
- type SimpleTreeSolver
- type SolverState
- type SplitNode
- type SplitResult
- type SplittingTree
- type TightenMode
- type TreeContext
- type TreeSolver
Constants ¶
const ( IsFalse dnfFinal = iota IsTrue NotFinal )
Variables ¶
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
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.
type DNFToLPB ¶
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 ¶
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 ¶
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 ¶
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 ¶
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 ¶
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) 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 ¶
type LPB ¶
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 ParseLPB ¶
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".
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.
func (LPBCoeff) Add ¶
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 ¶
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 ¶
Equals returns true iff val1 == val2. This is the case iff val1.Compare(val2) == 0.
func (LPBCoeff) Greater ¶
Greater returns true iff val1 > val2. This is the case iff val1.Compare(val2) > 0.
func (LPBCoeff) Lesser ¶
Lesser returns true iff val1 < val2. This is the case iff val.Compare(val2) < 0.
func (LPBCoeff) Mult ¶
Mult computes val1 * val2. If either of the value is ∞ or -∞ this value is returned.
func (LPBCoeff) Sub ¶
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.
type LPSplitResult ¶
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
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 ¶
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