constraints

package
v0.0.0-...-c730170 Latest Latest
Warning

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

 Go to latest Published: Oct 18, 2021 License: MIT Imports: 11 Imported by: 0

Documentation

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func Binary 

func Binary(n int64) (bin []int)

binary 23 = 10111 special case if n==0 then return empty slice panic if n<0

func BinaryStr 

func BinaryStr(n int64) (s string)

func CategorizeTranslate2 

func CategorizeTranslate2(pbs []*Threshold)

func CreateEncoding 

func CreateEncoding(input []sat.Literal, which [8]bool, output []sat.Literal, tag string, pred sat.Pred, sorter sorters.Sorter) (cs sat.ClauseSet)

Create Encoding for Sorting Network 0) Omitted for clarity (ids as in paper) 1) A or -D 2) B or -D 3) -A or -B or D 4) -A or C 5) -B or C 6) A or B or -C 7) C or -D -1,0,1 = *, false, true

func CreateMDD 

func CreateMDD(store *mdd.IntervalMddStore, K int64, entries []Entry) (int, int64, int64, error)

func CreateMDDChain 

func CreateMDDChain(store *mdd.IntervalMddStore, K int64, entries []Entry, chains Chains) (int, int64, int64, error)

Chains is a set of chains in order of the PB Chain: there are clauses xi <-xi+1 <- xi+2 ... <- xi+k, and xi .. xi+k are in order of PB assumption: chains are subsets of literals of PB and in their order

func PositionSlice 

func PositionSlice(e1 []Entry, e2 []Entry) (bool, []int)

assumption is that pb2 is already a subsequece of pb1

func PreprocessPBwithAMO 

func PreprocessPBwithAMO(pb *Threshold, amo CardTranslation) bool

returns if preprocessing was successful Uses the translation of pb2 (count translation)

func PreprocessPBwithExactly 

func PreprocessPBwithExactly(pb1 *Threshold, pb2 *Threshold) bool

returns if preprocessing was successful returns if it cant do the preprocessing

func PrintThresholdTikZ 

func PrintThresholdTikZ(filename string, ts []SortingNetwork)

func ToLits 

func ToLits(entries []*Entry) (lits []sat.Literal)

func TranslateBySNChain 

func TranslateBySNChain(pb *Threshold, literals []sat.Literal)

func TranslatePBwithAMO 

func TranslatePBwithAMO(pb *Threshold, amo CardTranslation)

returns if preprocessing was successful Uses the translation of pb2 (count translation)

Types

type CardTranslation 

type CardTranslation struct {
	PB      *Threshold
	Typ     OneTranslationType
	Aux     []sat.Literal
	Clauses sat.ClauseSet
}

func TranslateAtMostOne 

func TranslateAtMostOne(typ OneTranslationType, tag string, lits []sat.Literal) (trans CardTranslation)

func TranslateExactlyOne 

func TranslateExactlyOne(typ OneTranslationType, tag string, lits []sat.Literal) (trans CardTranslation)

type Chain 

type Chain []sat.Literal

func CleanChain 

func CleanChain(entries []Entry, chain1 Chain) (chain2 Chain)

finds the subexpression of chain1 in e and returns the entries of chain1 existing in e.

func (Chain) Print 

func (c Chain) Print()

func (Chain) String 

func (c Chain) String() (s string)

type Chains 

type Chains []Chain

type EntriesAscending 

type EntriesAscending []Entry

func (EntriesAscending) Len 

func (a EntriesAscending) Len() int

func (EntriesAscending) Less 

func (a EntriesAscending) Less(i, j int) bool

func (EntriesAscending) Swap 

func (a EntriesAscending) Swap(i, j int)

type EntriesDescending 

type EntriesDescending []Entry

func (EntriesDescending) Len 

func (a EntriesDescending) Len() int

func (EntriesDescending) Less 

func (a EntriesDescending) Less(i, j int) bool

func (EntriesDescending) Swap 

func (a EntriesDescending) Swap(i, j int)

type EntriesVariables 

type EntriesVariables []Entry

func (EntriesVariables) Len 

func (a EntriesVariables) Len() int

func (EntriesVariables) Less 

func (a EntriesVariables) Less(i, j int) bool

func (EntriesVariables) Swap 

func (a EntriesVariables) Swap(i, j int)

type Entry 

type Entry struct {
	Literal sat.Literal
	Weight  int64
}

func CommonSlice 

func CommonSlice(e1 []Entry, e2 []Entry) (bool, []Entry)

assumption is that pb2 is already a subsequece of pb1 TODO deprecated

type EquationType 

type EquationType int
const (
	LE  EquationType = iota //"<="
	GE                      //">="
	EQ                      //"=="
	OPT                     //"MIN"
)

func (EquationType) String 

func (e EquationType) String() string

type IndEntries 

type IndEntries []IndEntry

func (IndEntries) Len 

func (a IndEntries) Len() int

func (IndEntries) Less 

func (a IndEntries) Less(i, j int) bool

func (IndEntries) Swap 

func (a IndEntries) Swap(i, j int)

type IndEntry 

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

type Lits 

type Lits []sat.Literal

func (Lits) Print 

func (c Lits) Print()

func (Lits) String 

func (c Lits) String() (s string)

type Match 

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

type Matching 

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

type MatchingsBySize 

type MatchingsBySize []Matching

func (MatchingsBySize) Len 

func (a MatchingsBySize) Len() int

func (MatchingsBySize) Less 

func (a MatchingsBySize) Less(i, j int) bool

func (MatchingsBySize) Swap 

func (a MatchingsBySize) Swap(i, j int)

type OneTranslationType 

type OneTranslationType int
const (
	Naive OneTranslationType = iota
	Sort
	Split
	Count
	Heule
	Log
	Pigeon
)

type SortingNetwork 

type SortingNetwork struct {
	Tare   int64
	Sorter sorters.Sorter
	Bags   [][]sat.Literal
	LitIn  []sat.Literal //Bags flattened, input to Sorter
	// contains filtered or unexported fields
}

func NewSortingNetwork 

func NewSortingNetwork(pb Threshold) (sn SortingNetwork)

TODO: update construction of sorting network!

func (*SortingNetwork) CreateBags 

func (t *SortingNetwork) CreateBags()

assumes LE, positive weights

func (*SortingNetwork) CreateSorter 

func (t *SortingNetwork) CreateSorter()

type Threshold 

type Threshold struct {
	Id         int // unique id to reference Threshold in encodings
	Entries    []Entry
	K          int64
	Typ        EquationType
	Offset     int64 // for Typ=Opt; opt= sumWeights - Offset
	Translated bool  //indicates if constraint is translated
	TransTyp   TranslationType
	Clauses    sat.ClauseSet
	Chains     Chains // has to be in order of Entries
	Err        error  // some error in the translation
}

func CreatePB 

func CreatePB(weights []int64, K int64) (pb Threshold)

creates an AtMost constraint with coefficients in weights, variables x1..xm

func CreatePBOffset 

func CreatePBOffset(offset int, weights []int64, K int64) (pb Threshold)

creates an AtMost constraint with coefficients in weights, variables x1..xm

func (*Threshold) Cardinality 

func (t *Threshold) Cardinality() (allSame bool, literals []sat.Literal)

all weights are the same; performs rounding if this is true, then all weights are 1, and K is the cardinality

func (*Threshold) CatSimpl 

func (pb *Threshold) CatSimpl()

func (*Threshold) CategorizeTranslate1 

func (pb *Threshold) CategorizeTranslate1()

func (*Threshold) Copy 

func (pb *Threshold) Copy() (pb2 Threshold)

creates copy of pb, new allocation of Entry slice copy empties the clauseSet!

func (*Threshold) CreateCardinality 

func (pb *Threshold) CreateCardinality()

CreateCardinality takes set of literals and creates a sorting network

func (*Threshold) Empty 

func (pb *Threshold) Empty() bool

func (*Threshold) Evaluate 

func (pb *Threshold) Evaluate(a sat.Assignment) (r int64)

func (*Threshold) IdS 

func (pb *Threshold) IdS() string

func (*Threshold) IsComplex 

func (pb *Threshold) IsComplex() bool

checks if same coefficient for all entries

func (*Threshold) IsComplexTranslation 

func (pb *Threshold) IsComplexTranslation() (b bool)

func (*Threshold) Literals 

func (t *Threshold) Literals() (lits []sat.Literal)

func (*Threshold) Multiply 

func (t *Threshold) Multiply(c int64)

func (*Threshold) Normalize 

func (t *Threshold) Normalize(typ EquationType, posWeights bool)

normalizes the threshold Change EquationType in case of LE/GE in case of EQ and OPT, positive weights

func (*Threshold) NormalizePositiveCoefficients 

func (t *Threshold) NormalizePositiveCoefficients()

func (*Threshold) NormalizePositiveLiterals 

func (t *Threshold) NormalizePositiveLiterals()

func (*Threshold) PosAfterChains 

func (pb *Threshold) PosAfterChains() int

func (*Threshold) Positive 

func (pb *Threshold) Positive() bool

func (*Threshold) Print10 

func (t *Threshold) Print10()

func (*Threshold) Print2 

func (t *Threshold) Print2()

func (*Threshold) PrintGringo 

func (t *Threshold) PrintGringo()

func (*Threshold) PrintGurobi 

func (t *Threshold) PrintGurobi()

func (*Threshold) PrintPBO 

func (t *Threshold) PrintPBO()

func (*Threshold) RemoveZeros 

func (t *Threshold) RemoveZeros()

finds trivially implied facts, returns set of facts removes such entries from the pb threshold can become empty!

func (*Threshold) RewriteSameWeights 

func (pb *Threshold) RewriteSameWeights()

returns the encoding of this PB adds to internal clauses

func (*Threshold) Simplify 

func (pb *Threshold) Simplify()

finds trivially implied facts, returns set of facts removes such entries from the pb threshold can become empty!

func (*Threshold) SortAscending 

func (t *Threshold) SortAscending()

func (*Threshold) SortDescending 

func (t *Threshold) SortDescending()

func (*Threshold) SortVar 

func (t *Threshold) SortVar()

func (*Threshold) String 

func (t *Threshold) String() (s string)

func (*Threshold) SumWeights 

func (t *Threshold) SumWeights() (total int64)

sums up all weights

func (*Threshold) Translate 

func (pb *Threshold) Translate(K_lessOffset int64) sat.ClauseSet

returns the encoding of this PB

func (*Threshold) TranslateByMDD 

func (pb *Threshold) TranslateByMDD()

func (*Threshold) TranslateByMDDChain 

func (pb *Threshold) TranslateByMDDChain(chains Chains)

chains must be in order of pb and be subsets of its literals

func (*Threshold) TranslateBySN 

func (pb *Threshold) TranslateBySN()

func (*Threshold) TranslateComplexThreshold 

func (pb *Threshold) TranslateComplexThreshold()

func (*Threshold) WriteFormula 

func (t *Threshold) WriteFormula(base int, file *os.File)

type TranslationType 

type TranslationType int // replace by a configuration

const (
	UNKNOWN TranslationType = iota
	Facts
	Clause
	AMO
	EX1
	EXK
	CARD
	CMDD
	CSN
	CMDDC
	TranslationTypes
	CSNC
)

func (TranslationType) String 

func (t TranslationType) String() (s string)

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.