1package solver23import (4 "fmt"5 "sort"6 "strings"7)89// data used in PB constraints.10type pbData struct {11 weights []int // weight of each literal. If nil, weights are all 1.12 watched []bool // indices of watched literals.13}1415// A Clause is a list of Lit, associated with possible data (for learned clauses).16type Clause struct {17 lits []Lit18 // lbdValue's bits are as follow:19 // leftmost bit: learned flag.20 // second bit: locked flag (if learned).21 // last 30 bits: LBD value (if learned) or minimal cardinality - 1 (if !learned).22 // NOTE: actual cardinality is value + 1, since this is the default value and go defaults to 0.23 lbdValue uint3224 activity float3225 pbData *pbData26}2728const (29 learnedMask uint32 = 1 << 3130 lockedMask uint32 = 1 << 3031 bothMasks uint32 = learnedMask | lockedMask32)3334// NewClause returns a clause whose lits are given as an argument.35func NewClause(lits []Lit) *Clause {36 return &Clause{lits: lits}37}3839// NewCardClause returns a clause whose lits are given as an argument and40// for which at least 'card' literals must be true.41// Note tha NewClause(lits) is equivalent to NewCardClause(lits, 1).42func NewCardClause(lits []Lit, card int) *Clause {43 if card < 1 || card > len(lits) {44 panic("Invalid cardinality value")45 }46 return &Clause{lits: lits, lbdValue: uint32(card - 1)}47}4849// Used to sort literals when constructing PB clause.50type weightedLits struct {51 lits []Lit52 weights []int53}5455func (wl weightedLits) Less(i, j int) bool { return wl.weights != nil && wl.weights[i] > wl.weights[j] }56func (wl weightedLits) Len() int { return len(wl.lits) }57func (wl *weightedLits) Swap(i, j int) {58 wl.lits[i], wl.lits[j] = wl.lits[j], wl.lits[i]59 if wl.weights != nil {60 wl.weights[i], wl.weights[j] = wl.weights[j], wl.weights[i]61 }62}6364// NewPBClause returns a pseudo-boolean clause with the given lits, weights and minimal cardinality.65func NewPBClause(lits []Lit, weights []int, card int) *Clause {66 if card < 1 {67 panic("Invalid cardinality value")68 }69 wl := &weightedLits{lits: lits, weights: weights}70 sort.Sort(wl)71 pbd := pbData{weights: weights, watched: make([]bool, len(lits))}72 if pbd.weights == nil {73 pbd.weights = make([]int, len(lits))74 for i := range pbd.weights {75 pbd.weights[i] = 176 }77 }78 return &Clause{lits: lits, lbdValue: uint32(card - 1), pbData: &pbd}79}8081// NewLearnedClause returns a new clause marked as learned.82func NewLearnedClause(lits []Lit) *Clause {83 return &Clause{lits: lits, lbdValue: learnedMask}84}8586// Cardinality returns the minimum number of literals that must be true to satisfy the clause.87func (c *Clause) Cardinality() int {88 if c.Learned() {89 return 190 }91 return int(c.lbdValue & ^bothMasks) + 192}9394// Learned returns true iff c was a learned clause.95func (c *Clause) Learned() bool {96 return c.lbdValue&learnedMask == learnedMask97}9899// PseudoBoolean returns true iff c is a pseudo boolean constraint, and not100// just a propositional clause or cardinality constraint.101func (c *Clause) PseudoBoolean() bool {102 return c.pbData != nil103}104105func (c *Clause) lock() {106 c.lbdValue = c.lbdValue | lockedMask107}108109func (c *Clause) unlock() {110 c.lbdValue = c.lbdValue & ^lockedMask111}112113func (c *Clause) lbd() int {114 return int(c.lbdValue & ^bothMasks)115}116117func (c *Clause) setLbd(lbd int) {118 c.lbdValue = (c.lbdValue & bothMasks) | uint32(lbd)119}120121func (c *Clause) incLbd() {122 c.lbdValue++123}124125func (c *Clause) isLocked() bool {126 return c.lbdValue&bothMasks == bothMasks127}128129// Len returns the nb of lits in the clause.130func (c *Clause) Len() int {131 return len(c.lits)132}133134// First returns the first lit from the clause.135func (c *Clause) First() Lit {136 return c.lits[0]137}138139// Second returns the second lit from the clause.140func (c *Clause) Second() Lit {141 return c.lits[1]142}143144// Get returns the ith literal from the clause.145func (c *Clause) Get(i int) Lit {146 return c.lits[i]147}148149// Set sets the ith literal of the clause.150func (c *Clause) Set(i int, l Lit) {151 c.lits[i] = l152}153154// Weight returns the weight of the ith literal.155// In a propositional clause or a cardinality constraint, that value will always be 1.156func (c *Clause) Weight(i int) int {157 if c.pbData == nil {158 return 1159 }160 return c.pbData.weights[i]161}162163// WeightSum returns the sum of the PB weights.164// If c is a propositional clause, the function will return the length of the clause.165func (c *Clause) WeightSum() int {166 if c.pbData == nil {167 return len(c.lits)168 }169 res := 0170 for _, w := range c.pbData.weights {171 res += w172 }173 return res174}175176// swap swaps the ith and jth lits from the clause.177func (c *Clause) swap(i, j int) {178 c.lits[i], c.lits[j] = c.lits[j], c.lits[i]179 if c.pbData != nil {180 c.pbData.weights[i], c.pbData.weights[j] = c.pbData.weights[j], c.pbData.weights[i]181 }182}183184// updateCardinality adds "add" to c's cardinality.185// Must not be called on learned clauses!186func (c *Clause) updateCardinality(add int) {187 if add < 0 && uint32(-add) > c.lbdValue {188 c.lbdValue = 0189 } else {190 c.lbdValue += uint32(add)191 }192}193194// removeLit remove the idx'th lit from c.195// The order of literals might be updated, so this function196// should not be called once the whole solver was created,197// only during simplification of the problem.198func (c *Clause) removeLit(idx int) {199 c.lits[idx] = c.lits[len(c.lits)-1]200 c.lits = c.lits[:len(c.lits)-1]201 if c.pbData != nil {202 c.pbData.weights[idx] = c.pbData.weights[len(c.pbData.weights)-1]203 c.pbData.weights = c.pbData.weights[:len(c.pbData.weights)-1]204 }205}206207// Shrink reduces the length of the clauses, by removing all lits208// starting from position newLen.209func (c *Clause) Shrink(newLen int) {210 c.lits = c.lits[:newLen]211 if c.pbData != nil {212 c.pbData.weights = c.pbData.weights[:newLen]213 c.pbData.watched = c.pbData.watched[:newLen]214 }215}216217// CNF returns a DIMACS CNF representation of the clause.218func (c *Clause) CNF() string {219 res := ""220 for _, lit := range c.lits {221 res += fmt.Sprintf("%d ", lit.Int())222 }223 return fmt.Sprintf("%s0", res)224}225226// PBString returns a string representation of c as a pseudo-boolean expression.227func (c *Clause) PBString() string {228 terms := make([]string, c.Len())229 for i, lit := range c.lits {230 weight := 1231 if c.pbData != nil {232 weight = c.pbData.weights[i]233 }234 val := lit.Int()235 sign := ""236 if val < 0 {237 val = -val238 sign = "~"239 }240 terms[i] = fmt.Sprintf("%d %sx%d", weight, sign, val)241 }242 return fmt.Sprintf("%s >= %d ;", strings.Join(terms, " +"), c.Cardinality())243}244245// SimplifyPB tries to simplify a pseudo boolean constraint by propagating all lits that can be propagated246// not matter whet the assignment.247// A PB constraint can also be false if all its coeficients are smaller than the cardinality.248// It will return a list of unit lits (if any), a new, simplified clause (or nil if all lits can be propagated and/or ignored)249// and a boolean ok indicating whether the clause can be satisfied or not. If ok is false, other return parameters are irrelevant.250func (c *Clause) SimplifyPB() (units []Lit, c2 *Clause, ok bool) {251 card := c.Cardinality()252 thresh := c.WeightSum() - card253 if thresh < 0 {254 // Even if all lits are true, the clause is still unsatisfied255 return nil, nil, false256 }257 // all lits whose weights are > thresh must be satisfied258 i := 0259 for i < c.Len() && c.Weight(i) > thresh {260 units = append(units, c.Get(i))261 card -= c.Weight(i)262 i++263 }264 if card <= 0 {265 // clause is now satisfied, other lits are irrelevant266 return units, nil, true267 }268 // All lits starting from i must be kept269 newLen := c.Len() - i270 newLits := make([]Lit, newLen)271 newWeights := make([]int, newLen)272 copy(newLits, c.lits[i:])273 copy(newWeights, c.pbData.weights[i:])274 // saturate weights so that none is higher than card275 i = 0276 for newWeights[i] > card {277 newWeights[i] = card278 }279 return units, NewPBClause(newLits, newWeights, card), true280}