Documentation ¶
Index ¶
- func Binary(n int64) (bin []int)
- func BinaryStr(n int64) (s string)
- func CategorizeTranslate2(pbs []*Threshold)
- func CreateEncoding(input []sat.Literal, which [8]bool, output []sat.Literal, tag string, ...) (cs sat.ClauseSet)
- func CreateMDD(store *mdd.IntervalMddStore, K int64, entries []Entry) (int, int64, int64, error)
- func CreateMDDChain(store *mdd.IntervalMddStore, K int64, entries []Entry, chains Chains) (int, int64, int64, error)
- func PositionSlice(e1 []Entry, e2 []Entry) (bool, []int)
- func PreprocessPBwithAMO(pb *Threshold, amo CardTranslation) bool
- func PreprocessPBwithExactly(pb1 *Threshold, pb2 *Threshold) bool
- func PrintThresholdTikZ(filename string, ts []SortingNetwork)
- func ToLits(entries []*Entry) (lits []sat.Literal)
- func TranslateBySNChain(pb *Threshold, literals []sat.Literal)
- func TranslatePBwithAMO(pb *Threshold, amo CardTranslation)
- type CardTranslation
- type Chain
- type Chains
- type EntriesAscending
- type EntriesDescending
- type EntriesVariables
- type Entry
- type EquationType
- type IndEntries
- type IndEntry
- type Lits
- type Match
- type Matching
- type MatchingsBySize
- type OneTranslationType
- type SortingNetwork
- type Threshold
- func (t *Threshold) Cardinality() (allSame bool, literals []sat.Literal)
- func (pb *Threshold) CatSimpl()
- func (pb *Threshold) CategorizeTranslate1()
- func (pb *Threshold) Copy() (pb2 Threshold)
- func (pb *Threshold) CreateCardinality()
- func (pb *Threshold) Empty() bool
- func (pb *Threshold) Evaluate(a sat.Assignment) (r int64)
- func (pb *Threshold) IdS() string
- func (pb *Threshold) IsComplex() bool
- func (pb *Threshold) IsComplexTranslation() (b bool)
- func (t *Threshold) Literals() (lits []sat.Literal)
- func (t *Threshold) Multiply(c int64)
- func (t *Threshold) Normalize(typ EquationType, posWeights bool)
- func (t *Threshold) NormalizePositiveCoefficients()
- func (t *Threshold) NormalizePositiveLiterals()
- func (pb *Threshold) PosAfterChains() int
- func (pb *Threshold) Positive() bool
- func (t *Threshold) Print10()
- func (t *Threshold) Print2()
- func (t *Threshold) PrintGringo()
- func (t *Threshold) PrintGurobi()
- func (t *Threshold) PrintPBO()
- func (t *Threshold) RemoveZeros()
- func (pb *Threshold) RewriteSameWeights()
- func (pb *Threshold) Simplify()
- func (t *Threshold) SortAscending()
- func (t *Threshold) SortDescending()
- func (t *Threshold) SortVar()
- func (t *Threshold) String() (s string)
- func (t *Threshold) SumWeights() (total int64)
- func (pb *Threshold) Translate(K_lessOffset int64) sat.ClauseSet
- func (pb *Threshold) TranslateByMDD()
- func (pb *Threshold) TranslateByMDDChain(chains Chains)
- func (pb *Threshold) TranslateBySN()
- func (pb *Threshold) TranslateComplexThreshold()
- func (t *Threshold) WriteFormula(base int, file *os.File)
- type TranslationType
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
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 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 ¶
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 ¶
returns if preprocessing was successful returns if it cant do the preprocessing
func PrintThresholdTikZ ¶
func PrintThresholdTikZ(filename string, ts []SortingNetwork)
func TranslateBySNChain ¶
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 ¶
func CleanChain ¶
finds the subexpression of chain1 in e and returns the entries of chain1 existing in e.
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 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 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 CreatePBOffset ¶
creates an AtMost constraint with coefficients in weights, variables x1..xm
func (*Threshold) Cardinality ¶
all weights are the same; performs rounding if this is true, then all weights are 1, and K is the cardinality
func (*Threshold) CategorizeTranslate1 ¶
func (pb *Threshold) CategorizeTranslate1()
func (*Threshold) Copy ¶
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) IsComplexTranslation ¶
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 (*Threshold) PrintGringo ¶
func (t *Threshold) PrintGringo()
func (*Threshold) PrintGurobi ¶
func (t *Threshold) PrintGurobi()
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) TranslateByMDD ¶
func (pb *Threshold) TranslateByMDD()
func (*Threshold) TranslateByMDDChain ¶
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()
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)