1package solver23import (4 "fmt"5 "sort"6)78type watcher struct {9 other Lit // Another lit from the clause10 clause *Clause11}1213// A watcherList is a structure used to store clauses and propagate unit literals efficiently.14type watcherList struct {15 nbMax int // Max # of learned clauses at current moment16 idxReduce int // # of calls to reduce + 117 wlistBin [][]watcher // For each literal, a list of binary clauses where its negation appears18 wlist [][]watcher // For each literal, a list of non-binary clauses where its negation appears at position 1 or 219 wlistPb [][]*Clause // For each literal, a list of PB or cardinality constraints.20 wlistCardAMO [][]*Clause // For each literal, a list of cardinality constraints where card = length - 1, meaning any false literal propagates all others.21 origClauses []*Clause // All the problem clauses.22 learned []*Clause23}2425// initWatcherList makes a new watcherList for the solver.26func (s *Solver) initWatcherList(clauses []*Clause) {27 nbMax := initNbMaxClauses28 newClauses := make([]*Clause, len(clauses))29 copy(newClauses, clauses)30 s.wl = watcherList{31 nbMax: nbMax,32 idxReduce: 1,33 wlistBin: make([][]watcher, s.nbVars*2),34 wlist: make([][]watcher, s.nbVars*2),35 wlistPb: make([][]*Clause, s.nbVars*2),36 wlistCardAMO: make([][]*Clause, s.nbVars*2),37 origClauses: newClauses,38 }39 for _, c := range clauses {40 s.watchClause(c)41 }42}4344// Should be called when new vars are added to the problem (see Solver.newVar)45func (s *Solver) addVarWatcherList(v Var) {46 cnfVar := int(v.Int())47 for i := s.nbVars; i < cnfVar; i++ {48 s.wl.wlistBin = append(s.wl.wlistBin, nil, nil)49 s.wl.wlist = append(s.wl.wlist, nil, nil)50 s.wl.wlistPb = append(s.wl.wlistPb, nil, nil)51 s.wl.wlistCardAMO = append(s.wl.wlistCardAMO, nil, nil)52 }53}5455// appendClause appends the clause without checking whether the clause is already satisfiable, unit, or unsatisfiable.56// To perform those checks, call s.AppendClause.57// clause is supposed to be a problem clause, not a learned one.58func (s *Solver) appendClause(clause *Clause) {59 s.wl.origClauses = append(s.wl.origClauses, clause)60 // log.Printf("appending (and watching) %s", clause.PBString())61 s.watchClause(clause)62}6364// bumpNbMax increases the max nb of clauses used.65// It is typically called after a restart.66func (s *Solver) bumpNbMax() {67 s.wl.nbMax += incrNbMaxClauses68}6970// postponeNbMax increases the max nb of clauses used.71// It is typically called when too many good clauses were learned and a cleaning was expected.72func (s *Solver) postponeNbMax() {73 s.wl.nbMax += incrPostponeNbMax74}7576// Utilities for sorting according to clauses' LBD and activities.77func (wl *watcherList) Len() int { return len(wl.learned) }78func (wl *watcherList) Swap(i, j int) { wl.learned[i], wl.learned[j] = wl.learned[j], wl.learned[i] }7980func (wl *watcherList) Less(i, j int) bool {81 ci := wl.learned[i]82 cj := wl.learned[j]83 lbdI := ci.lbd()84 lbdJ := cj.lbd()85 // Sort by lbd, break ties by activity86 return lbdI > lbdJ || (lbdI == lbdJ && wl.learned[i].activity < wl.learned[j].activity)87}8889// Watches the provided clause.90func (s *Solver) watchClause(c *Clause) {91 if c.PseudoBoolean() {92 s.watchPB(c)93 } else if card := c.Cardinality(); card > 1 {94 if card == c.Len()+1 {95 s.watchCardAMO(c, card)96 } else {97 // log.Printf("watching cardinality %s", c.PBString())98 for i := 0; i < c.Cardinality()+1; i++ {99 lit := c.Get(i)100 neg := lit.Negation()101 s.wl.wlistPb[neg] = append(s.wl.wlistPb[neg], c)102 }103 }104 } else if c.Len() == 2 {105 // log.Printf("watching binary %s", c.PBString())106 first := c.First()107 second := c.Second()108 neg0 := first.Negation()109 neg1 := second.Negation()110 s.wl.wlistBin[neg0] = append(s.wl.wlistBin[neg0], watcher{clause: c, other: second})111 s.wl.wlistBin[neg1] = append(s.wl.wlistBin[neg1], watcher{clause: c, other: first})112 } else { // Regular, propositional clause113 // log.Printf("watching regular %s", c.PBString())114 first := c.First()115 second := c.Second()116 neg0 := first.Negation()117 neg1 := second.Negation()118 s.wl.wlist[neg0] = append(s.wl.wlist[neg0], watcher{clause: c, other: second})119 s.wl.wlist[neg1] = append(s.wl.wlist[neg1], watcher{clause: c, other: first})120 }121}122123func (s *Solver) watchPB(c *Clause) {124 // log.Printf("watching PB %s", c.PBString())125 goal := c.Weight(0) + c.Cardinality() // We'll keep watching vars until the max weight at least reaches this value126 sum := 0127 i := 0128 // log.Printf("goal is %d", goal)129 for sum < goal && i < c.Len() {130 lit := c.Get(i)131 neg := lit.Negation()132 s.wl.wlistPb[neg] = append(s.wl.wlistPb[neg], c)133 c.pbData.watched[i] = true134 sum += c.Weight(i)135 i++136 }137}138139func (s *Solver) watchCardAMO(c *Clause, card int) {140 // This is an AtMostOne constraint. At most one of the literals is false.141 // Any falsified literal propagates all other lits.142 // log.Printf("watching AMO %s", c.PBString())143 for i := 0; i < card+1; i++ {144 lit := c.Get(i)145 neg := lit.Negation()146 s.wl.wlistCardAMO[neg] = append(s.wl.wlistCardAMO[neg], c)147 }148}149150// unwatch the given learned clause.151// NOTE: since it is only called when c.lbd() > 2, we know for sure152// that c is not a binary clause.153// We also know for sure this is a propositional clause, since only those are learned.154func (s *Solver) unwatchClause(c *Clause) {155 for i := 0; i < 2; i++ {156 neg := c.Get(i).Negation()157 j := 0158 length := len(s.wl.wlist[neg])159 // We're looking for the index of the clause.160 // This will panic if c is not in wlist[neg], but this shouldn't happen.161 for s.wl.wlist[neg][j].clause != c {162 j++163 }164 s.wl.wlist[neg][j] = s.wl.wlist[neg][length-1]165 s.wl.wlist[neg] = s.wl.wlist[neg][:length-1]166 }167}168169// unwatch the given learned PB constraint.170// Note: this should only be called when c.PseudoBoolean() is true.171func (s *Solver) unwatchPB(c *Clause) {172 for i := 0; i < c.Len(); i++ {173 if !c.pbData.watched[i] {174 continue175 }176 neg := c.Get(i).Negation()177 j := 0178 length := len(s.wl.wlistPb[neg])179 // We're looking for the index of the clause.180 // This will panic if c is not in wlist[neg], but this shouldn't happen.181 for s.wl.wlistPb[neg][j] != c {182 j++183 }184 s.wl.wlistPb[neg][j] = s.wl.wlistPb[neg][length-1]185 s.wl.wlistPb[neg] = s.wl.wlistPb[neg][:length-1]186 }187}188189// reduceLearned removes a few learned clauses that are deemed useless.190func (s *Solver) reduceLearned() {191 sort.Sort(&s.wl)192 nbLearned := len(s.wl.learned)193 length := nbLearned / 2194 if s.wl.learned[length].lbd() <= 3 { // Lots of good clauses, postpone reduction195 s.postponeNbMax()196 }197 nbRemoved := 0198 for i := 0; i < length; i++ {199 c := s.wl.learned[i]200 if c.lbd() <= 2 || c.isLocked() {201 continue202 }203 nbRemoved++204 s.Stats.NbDeleted++205 s.wl.learned[i] = s.wl.learned[nbLearned-nbRemoved]206 s.unwatchClause(c)207 }208 nbLearned -= nbRemoved209 s.wl.learned = s.wl.learned[:nbLearned]210}211212type watcherListPB watcherList // A type synonymous to sort PB constraints a little more efficiently.213214func (wl *watcherListPB) Len() int { return len(wl.learned) }215func (wl *watcherListPB) Swap(i, j int) { wl.learned[i], wl.learned[j] = wl.learned[j], wl.learned[i] }216217func (wl *watcherListPB) Less(i, j int) bool {218 return wl.learned[i].activity < wl.learned[j].activity219}220221func (s *Solver) reduceLearnedPB() {222 wlpb := watcherListPB(s.wl)223 sort.Sort(&wlpb)224 nbLearned := len(s.wl.learned)225 length := nbLearned / 2226 nbRemoved := 0227 for i := 0; i < length; i++ {228 c := s.wl.learned[i]229 if c.isLocked() {230 continue231 }232 nbRemoved++233 s.Stats.NbDeleted++234 s.wl.learned[i] = s.wl.learned[nbLearned-nbRemoved]235 s.unwatchPB(c)236 }237 nbLearned -= nbRemoved238 s.wl.learned = s.wl.learned[:nbLearned]239}240241// Adds the given learned clause and updates watchers.242// If too many clauses have been learned yet, one will be removed.243func (s *Solver) addLearned(c *Clause) {244 s.wl.learned = append(s.wl.learned, c)245 s.watchClause(c)246 s.clauseBumpActivity(c)247 if s.Certified {248 if s.CertChan == nil {249 fmt.Printf("%s\n", c.CNF())250 } else {251 s.CertChan <- c.CNF()252 }253 }254}255256// Adds the given unit literal to the model at the top level.257func (s *Solver) addLearnedUnit(unit Lit) {258 s.model[unit.Var()] = lvlToSignedLvl(unit, 1)259 if s.Certified {260 if s.CertChan == nil {261 fmt.Printf("%d 0\n", unit.Int())262 } else {263 s.CertChan <- fmt.Sprintf("%d 0", unit.Int())264 }265 }266}267268// If l is negative, -lvl is returned. Else, lvl is returned.269func lvlToSignedLvl(l Lit, lvl decLevel) decLevel {270 if l.IsPositive() {271 return lvl272 }273 return -lvl274}275276// Removes the first occurrence of c from lst.277// The element *must* be present into lst.278func removeFrom(lst []*Clause, c *Clause) []*Clause {279 i := 0280 for lst[i] != c {281 i++282 }283 last := len(lst) - 1284 lst[i] = lst[last]285 return lst[:last]286}287288// Propagates literals in the trail starting from the ptrth, and returns a conflict clause, or nil if none arose.289func (s *Solver) propagate(ptr int, lvl decLevel) *Clause {290 for ptr < len(s.trail) {291 lit := s.trail[ptr]292 // log.Printf("propagating %d", lit.Int())293 for _, w := range s.wl.wlistBin[lit] {294 v2 := w.other.Var()295 if assign := s.model[v2]; assign == 0 { // Other was unbounded: propagate296 s.reason[v2] = w.clause297 s.model[v2] = lvlToSignedLvl(w.other, lvl)298 s.trail = append(s.trail, w.other)299 } else if (assign > 0) != w.other.IsPositive() { // Conflict here300 return w.clause301 }302 }303 if confl := s.simplifyPropClauses(lit, lvl); confl != nil {304 return confl305 }306 for _, c := range s.wl.wlistPb[lit] {307 if c.PseudoBoolean() {308 if !s.simplifyPseudoBool(c, lvl) {309 return c310 }311 } else {312 if !s.simplifyCardConstr(c, lvl) {313 return c314 }315 }316 }317 for _, c := range s.wl.wlistCardAMO[lit] {318 if !s.simplifyCardAMOConstr(c, lvl) {319 return c320 }321 }322 ptr++323 }324 // No unsat clause was met325 return nil326}327328// Unifies the given literal and returns a conflict clause, or nil if no conflict arose.329func (s *Solver) unifyLiteral(lit Lit, lvl decLevel) *Clause {330 s.model[lit.Var()] = lvlToSignedLvl(lit, lvl)331 s.trail = append(s.trail, lit)332 return s.propagate(len(s.trail)-1, lvl)333}334335func (s *Solver) unifyLiterals(lits []Lit, lvl decLevel) *Clause {336 for _, lit := range lits {337 s.model[lit.Var()] = lvlToSignedLvl(lit, lvl)338 s.trail = append(s.trail, lit)339 }340 for i := 0; i < len(lits); i++ {341 if confl := s.propagate(len(s.trail)-len(lits)-i, lvl); confl != nil {342 return confl343 }344 }345 return nil346}347348func (s *Solver) propagateUnit(c *Clause, lvl decLevel, unit Lit) {349 // log.Printf("propagating unit %d", unit.Int())350 v := unit.Var()351 s.reason[v] = c352 c.lock()353 s.model[v] = lvlToSignedLvl(unit, lvl)354 s.trail = append(s.trail, unit)355}356357func (s *Solver) simplifyPropClauses(lit Lit, lvl decLevel) *Clause {358 wl := s.wl.wlist[lit]359 j := 0360 for i, w := range wl {361 if s.litStatus(w.other) == Sat { // blocking literal is SAT? Don't explore clause!362 wl[j] = w363 j++364 continue365 }366 c := w.clause367 // make sure c.Second() is lit368 if c.First() == lit.Negation() {369 c.swap(0, 1)370 }371 w2 := watcher{clause: c, other: c.First()}372 firstStatus := s.litStatus(c.First())373 if firstStatus == Sat { // Clause is already sat374 wl[j] = w2375 j++376 } else {377 found := false378 for k := 2; k < c.Len(); k++ {379 if litK := c.Get(k); s.litStatus(litK) != Unsat {380 c.swap(1, k)381 neg := litK.Negation()382 s.wl.wlist[neg] = append(s.wl.wlist[neg], w2)383 found = true384 break385 }386 }387 if !found { // No free lit found: unit propagation or UNSAT388 wl[j] = w2389 j++390 if firstStatus == Unsat {391 copy(wl[j:], wl[i+1:]) // Keep remaining clauses392 s.wl.wlist[lit] = wl[:len(wl)-((i+1)-j)]393 return c394 }395 s.propagateUnit(c, lvl, c.First())396 }397 }398 }399 s.wl.wlist[lit] = wl[:j]400 return nil401}402403// simplifyCardConstr simplifies a constraint of cardinality > 1, but with all weights = 1.404// returns false iff the clause cannot be satisfied.405func (s *Solver) simplifyCardConstr(clause *Clause, lvl decLevel) bool {406 length := clause.Len()407 card := clause.Cardinality()408 nbTrue := 0409 nbFalse := 0410 nbUnb := 0411 for i := 0; i < length; i++ {412 lit := clause.Get(i)413 switch s.litStatus(lit) {414 case Indet:415 nbUnb++416 case Sat:417 nbTrue++418 if nbTrue == card {419 return true420 }421 case Unsat:422 nbFalse++423 if length-nbFalse < card {424 return false425 }426 }427 if nbUnb+nbTrue > card {428 break429 }430 }431 if nbUnb+nbTrue == card {432 // All unbounded lits must be bound to make the clause true433 i := 0434 for nbUnb > 0 {435 lit := clause.Get(i)436 if s.model[lit.Var()] == 0 {437 s.propagateUnit(clause, lvl, lit)438 nbUnb--439 } else {440 i++441 }442 }443 return true444 }445 s.swapFalse(clause)446 return true447}448449// simplifyCardAMOConstr simplifies the special cardinality constraints where card == length -1, and returns false iff the constraint is UNSAT.450// Whenever a literal is false, all other literals must be true.451// This is a special case, which can be dealt with slightly more efficiently than more general cases.452func (s *Solver) simplifyCardAMOConstr(clause *Clause, lvl decLevel) bool {453 card := clause.Cardinality()454 length := card + 1455 foundFalse := false456 for i := 0; i < length; i++ {457 lit := clause.Get(i)458 if s.litStatus(lit) == Unsat {459 if foundFalse { // A second false lit460 return false461 }462 foundFalse = true463 }464 }465 // All unbounded lits must be bound to make the clause true466 for i := 0; i < length; i++ {467 lit := clause.Get(i)468 if s.model[lit.Var()] == 0 {469 s.propagateUnit(clause, lvl, lit)470 }471 }472 return true473}474475// swapFalse swaps enough literals from the clause so that all watching literals are either true or unbounded lits.476// Must only be called when there a at least cardinality + 1 true and unbounded lits.477func (s *Solver) swapFalse(clause *Clause) {478 card := clause.Cardinality()479 i := 0480 j := card + 1481 for i < card+1 {482 lit := clause.Get(i)483 for s.litStatus(lit) != Unsat {484 i++485 if i == card+1 {486 return487 }488 lit = clause.Get(i)489 }490 lit = clause.Get(j)491 for s.litStatus(lit) == Unsat {492 j++493 lit = clause.Get(j)494 }495 ni := &s.wl.wlistPb[clause.Get(i).Negation()]496 nj := &s.wl.wlistPb[clause.Get(j).Negation()]497 clause.swap(i, j)498 *ni = removeFrom(*ni, clause)499 *nj = append(*nj, clause)500 i++501 j++502 }503}504505// slackSum returns slack value for c and whether the clause is already sat or not.506// The slack value is defined as sum of weights - cardinality - sum of weights of falsified lits.507// It can be negative, meaning the whole constraint is falsified.508// If it's 0 or above, it means all literals with a weight >= slack must be propagated.509// If the clause is already satisfied, the slack value shall not be used.510// This is mostly useful for PB constraints.511func (s *Solver) slackSum(c *Clause) (slack int, sat bool) {512 card := c.Cardinality()513 slack = -card514 sum := 0515 for i, w := range c.pbData.weights {516 status := s.litStatus(c.Get(i))517 switch status {518 case Indet:519 slack += w520 case Sat:521 slack += w522 sum += w523 if sum >= card {524 return slack, true525 }526 }527 }528 return slack, false529}530531// propagateAll propagates all unbounded literals from c as unit literals532func (s *Solver) propagateAll(c *Clause, lvl decLevel) {533 for i := 0; i < c.Len(); i++ {534 if lit := c.Get(i); s.litStatus(lit) == Indet {535 s.propagateUnit(c, lvl, lit)536 }537 }538}539540func (s *Solver) simplifyPseudoBool(clause *Clause, lvl decLevel) bool {541 foundUnit := true542 for foundUnit {543 slack, sat := s.slackSum(clause)544 if sat {545 return true546 }547 if slack < 0 {548 return false549 }550 if slack == 0 {551 s.propagateAll(clause, lvl)552 return true553 }554 foundUnit = false555 for i := 0; i < clause.Len(); i++ {556 lit := clause.Get(i)557 if s.litStatus(lit) == Indet && clause.Weight(i) > slack { // lit will be propagated558 s.propagateUnit(clause, lvl, lit)559 foundUnit = true560 }561 }562 }563 s.updateWatchPB(clause)564 return true565}566567func (s *Solver) updateWatchPB(clause *Clause) {568 weightWatched := 0569 i := 0570 card := clause.Cardinality()571 for weightWatched <= card && i < clause.Len() {572 lit := clause.Get(i)573 if s.litStatus(lit) == Unsat {574 if clause.pbData.watched[i] {575 ni := &s.wl.wlistPb[lit.Negation()]576 *ni = removeFrom(*ni, clause)577 clause.pbData.watched[i] = false578 }579 } else {580 weightWatched += clause.Weight(i)581 if !clause.pbData.watched[i] {582 ni := &s.wl.wlistPb[lit.Negation()]583 *ni = append(*ni, clause)584 clause.pbData.watched[i] = true585 }586 }587 i++588 }589 // If there are some more watched literals, they are now useless590 for i := i; i < clause.Len(); i++ {591 if clause.pbData.watched[i] {592 ni := &s.wl.wlistPb[clause.Get(i).Negation()]593 *ni = removeFrom(*ni, clause)594 clause.pbData.watched[i] = false595 }596 }597}