1package solver23// computeLbd computes and sets c's LBD (Literal Block Distance).4func (c *Clause) computeLbd(model Model) {5 c.setLbd(1)6 curLvl := abs(model[c.Get(0).Var()])7 for i := 0; i < c.Len(); i++ {8 lit := c.Get(i)9 if lvl := abs(model[lit.Var()]); lvl != curLvl {10 curLvl = lvl11 c.incLbd()12 }13 }14}1516// addClauseLits is a helper function for learnClause.17// It deals with lits from the conflict clause.18func (s *Solver) addClauseLits(confl *Clause, lvl decLevel, met, metLvl []bool, lits *[]Lit) int {19 nbLvl := 020 for i := 0; i < confl.Len(); i++ {21 l := confl.Get(i)22 v := l.Var()23 if s.litStatus(l) != Unsat {24 // In clauses where cardinality > 1, some lits might be true in the conflict clause: ignore them25 continue26 }27 met[v] = true28 s.varBumpActivity(v)29 if abs(s.model[v]) == lvl {30 metLvl[v] = true31 nbLvl++32 } else {33 *lits = append(*lits, l)34 }35 }36 return nbLvl37}3839// bufLits (per Solver) is the buffer for lits in learnClause, kept to40// reduce allocations; a package-level buffer made concurrent solvers41// unsafe (mosaic: moved onto the Solver).4243// learnClause creates a conflict clause and returns either:44// - the clause itself, if its len is at least 2,45// - a nil clause and a unit literal, if its len is exactly 1,46// - a nil clause and -1, if the empty clause was learned.47func (s *Solver) learnClause(confl *Clause, lvl decLevel) (learned *Clause, unit Lit) {48 s.clauseBumpActivity(confl)49 if s.bufLits == nil {50 s.bufLits = make([]Lit, 10_000)51 }52 lits := s.bufLits[:1] // Not 0: make room for asserting literal53 buf := make([]bool, s.nbVars*2) // Buffer for met and metLvl; reduces allocs/deallocs54 met := buf[:s.nbVars] // List of all vars already met55 metLvl := buf[s.nbVars:] // List of all vars from current level to deal with56 // nbLvl is the nb of vars in lvl currently used57 nbLvl := s.addClauseLits(confl, lvl, met, metLvl, &lits)58 ptr := len(s.trail) - 1 // Pointer in propagation trail59 for nbLvl > 1 { // We will stop once we only have one lit from current level.60 for !metLvl[s.trail[ptr].Var()] {61 if abs(s.model[s.trail[ptr].Var()]) == lvl { // This var was deduced afterwards and was not a reason for the conflict62 met[s.trail[ptr].Var()] = true63 }64 ptr--65 }66 v := s.trail[ptr].Var()67 if s.assumptions[v] {68 // Now we only have assumed lits: this is a top-level conflict69 return nil, -170 }71 ptr--72 nbLvl--73 if reason := s.reason[v]; reason != nil {74 s.clauseBumpActivity(reason)75 for i := 0; i < reason.Len(); i++ {76 lit := reason.Get(i)77 if v2 := lit.Var(); !met[v2] {78 if s.litStatus(lit) != Unsat { // In clauses where cardinality > 1, some lits might be true in the conflict clause: ignore them79 continue80 }81 met[v2] = true82 s.varBumpActivity(v2)83 if abs(s.model[v2]) == lvl {84 metLvl[v2] = true85 nbLvl++86 } else {87 lits = append(lits, lit)88 }89 }90 }91 }92 }93 for _, l := range s.trail { // Look for last lit from lvl and use it as asserting lit94 if metLvl[l.Var()] {95 lits[0] = l.Negation()96 break97 }98 }99 s.varDecayActivity()100 s.clauseDecayActivity()101 sortLiterals(lits, s.model)102 sz := s.minimizeLearned(met, lits)103 if sz == 1 {104 // fmt.Printf("learned unit %d, trail is %s\n", lits[0].Int(), s.trailString())105 return nil, lits[0]106 }107 if cap(lits) > cap(s.bufLits) {108 s.bufLits = lits[:cap(lits)] // the buffer grew: keep it109 }110 lits2 := make([]Lit, sz)111 copy(lits2, lits[:sz])112 learned = NewLearnedClause(lits2)113 learned.computeLbd(s.model)114 // fmt.Printf("learned clause %s, trail is %s\n", learned.CNF(), s.trailString())115 return learned, -1116}117118// minimizeLearned reduces (if possible) the length of the learned clause and returns the size119// of the new list of lits.120func (s *Solver) minimizeLearned(met []bool, learned []Lit) int {121 sz := 1122 for i := 1; i < len(learned); i++ {123 if reason := s.reason[learned[i].Var()]; reason == nil {124 learned[sz] = learned[i]125 sz++126 } else {127 for k := 0; k < reason.Len(); k++ {128 lit := reason.Get(k)129 if !met[lit.Var()] /*&& abs(s.model[lit.Var()]) > 1*/ {130 learned[sz] = learned[i]131 sz++132 break133 }134 }135 }136 }137 return sz138}