1package solver23// A PBConstr is a Pseudo-Boolean constraint.4type PBConstr struct {5 Lits []int // List of literals, designed with integer values. A positive value means the literal is true, a negative one it is false.6 Weights []int // Weight of each lit from Lits. If nil, all lits == 17 AtLeast int // Sum of all lits must be at least this value8}910// WeightSum returns the sum of the weight of all terms.11func (c PBConstr) WeightSum() int {12 if c.Weights == nil { // All weights = 113 return len(c.Lits)14 }15 res := 016 for _, w := range c.Weights {17 res += w18 }19 return res20}2122// Clause returns the clause (in fact, a constraint but the type is named Clause) associated with the given constraint.23func (c PBConstr) Clause() *Clause {24 lits := make([]Lit, len(c.Lits))25 for i, val := range c.Lits {26 lits[i] = IntToLit(int32(val))27 }28 // Saturate weights29 for i := range c.Weights {30 if c.Weights[i] > c.AtLeast {31 c.Weights[i] = c.AtLeast32 }33 }34 return NewPBClause(lits, c.Weights, c.AtLeast)35}3637// PropClause returns a PB constraint equivalent to a propositional clause: at least one of the given38// literals must be true.39// It takes ownership of lits.40func PropClause(lits ...int) PBConstr {41 return PBConstr{Lits: lits, AtLeast: 1}42}4344// AtLeast returns a PB constraint stating that at least n literals must be true.45// It takes ownership of lits.46func AtLeast(lits []int, n int) PBConstr {47 return PBConstr{Lits: lits, AtLeast: n}48}4950// AtMost returns a PB constraint stating that at most n literals can be true.51// It takes ownership of lits.52func AtMost(lits []int, n int) PBConstr {53 lits2 := make([]int, len(lits))54 for i := range lits {55 lits2[i] = -lits[i]56 }57 return PBConstr{Lits: lits2, AtLeast: len(lits2) - n}58}5960// GtEq returns a PB constraint stating that the sum of all literals multiplied by their weight61// must be at least n.62// Will panic if len(weights) != len(lits).63func GtEq(lits []int, weights []int, n int) PBConstr {64 if len(weights) != 0 && len(lits) != len(weights) {65 panic("not as many lits as weights")66 }67 for i := 0; i < len(weights); i++ {68 if weights[i] < 0 {69 weights[i] = -weights[i]70 n += weights[i]71 lits[i] = -lits[i]72 }73 if weights[i] == 0 {74 weights = append(weights[:i], weights[i+1:]...)75 lits = append(lits[:i], lits[i+1:]...)76 i--77 }78 }79 return PBConstr{Lits: lits, Weights: weights, AtLeast: n}80}8182// LtEq returns a PB constraint stating that the sum of all literals multiplied by their weight83// must be at most n.84// Will panic if len(weights) != len(lits).85func LtEq(lits []int, weights []int, n int) PBConstr {86 sum := 087 for i := range lits {88 lits[i] = -lits[i]89 sum += weights[i]90 }91 n = sum - n92 return GtEq(lits, weights, n)93}9495// Eq returns a set of PB constraints stating that the sum of all literals multiplied by their weight96// must be exactly n.97// Will panic if len(weights) != len(lits).98func Eq(lits []int, weights []int, n int) []PBConstr {99 lits2 := make([]int, len(lits))100 weights2 := make([]int, len(weights))101 copy(lits2, lits)102 copy(weights2, weights)103 ge := GtEq(lits2, weights2, n)104 le := LtEq(lits, weights, n)105 var res []PBConstr106 if ge.AtLeast > 0 {107 res = append(res, ge)108 }109 if le.AtLeast > 0 {110 res = append(res, le)111 }112 return res113}