1package solver23import (4 "fmt"5)67// A Problem is a list of clauses & a nb of vars.8type Problem struct {9 NbVars int // Total nb of vars10 Clauses []*Clause // List of non-empty, non-unit clauses11 Status Status // Status of the problem. Can be trivially UNSAT (if empty clause was met or inferred by UP) or Indet.12 Units []Lit // List of unit literal found in the problem.13 Model []decLevel // For each var, its inferred binding. 0 means unbound, 1 means bound to true, -1 means bound to false.14 minLits []Lit // For an optimisation problem, the list of lits whose sum must be minimized15 minWeights []int // For an optimisation problem, the weight of each lit.16}1718// Optim returns true iff pb is an optimisation problem, ie19// a problem for which we not only want to find a model, but also20// the best possible model according to an optimization constraint.21func (pb *Problem) Optim() bool {22 return pb.minLits != nil23}2425// CNF returns a DIMACS CNF representation of the problem.26func (pb *Problem) CNF() string {27 res := fmt.Sprintf("p cnf %d %d\n", pb.NbVars, len(pb.Clauses)+len(pb.Units))28 for _, unit := range pb.Units {29 res += fmt.Sprintf("%d 0\n", unit.Int())30 }31 for _, clause := range pb.Clauses {32 res += fmt.Sprintf("%s\n", clause.CNF())33 }34 return res35}3637// PBString returns a representation of the problem as a pseudo-boolean problem.38func (pb *Problem) PBString() string {39 res := pb.costFuncString()40 for _, unit := range pb.Units {41 sign := ""42 if !unit.IsPositive() {43 sign = "~"44 unit = unit.Negation()45 }46 res += fmt.Sprintf("1 %sx%d = 1 ;\n", sign, unit.Int())47 }48 for _, clause := range pb.Clauses {49 res += fmt.Sprintf("%s\n", clause.PBString())50 }51 return res52}5354// SetCostFunc sets the function to minimize when optimizing the problem.55// If all weights are 1, weights can be nil.56// In all other cases, len(lits) must be the same as len(weights).57func (pb *Problem) SetCostFunc(lits []Lit, weights []int) {58 if weights != nil && len(lits) != len(weights) {59 panic("length of lits and of weights don't match")60 }61 pb.minLits = lits62 pb.minWeights = weights63}6465// costFuncString returns a string representation of the cost function of the problem, if any, followed by a \n.66// If there is no cost function, the empty string will be returned.67func (pb *Problem) costFuncString() string {68 if pb.minLits == nil {69 return ""70 }71 res := "min: "72 for i, lit := range pb.minLits {73 w := 174 if pb.minWeights != nil {75 w = pb.minWeights[i]76 }77 sign := ""78 if w >= 0 && i != 0 { // No plus sign for the first term or for negative terms.79 sign = "+"80 }81 val := lit.Int()82 neg := ""83 if val < 0 {84 val = -val85 neg = "~"86 }87 res += fmt.Sprintf("%s%d %sx%d", sign, w, neg, val)88 }89 res += " ;\n"90 return res91}9293func (pb *Problem) updateStatus(nbClauses int) {94 pb.Clauses = pb.Clauses[:nbClauses]95 if pb.Status == Indet && nbClauses == 0 {96 pb.Status = Sat97 }98}99100// simplify simplifies the pure SAT problem, i.e runs unit propagation if possible.101func (pb *Problem) simplify2() {102 nbClauses := len(pb.Clauses)103 restart := true104 for restart {105 restart = false106 i := 0107 for i < nbClauses {108 c := pb.Clauses[i]109 nbLits := c.Len()110 clauseSat := false111 j := 0112 for j < nbLits {113 lit := c.Get(j)114 k := j + 1115 for k < nbLits {116 lit2 := c.Get(k)117 if lit2 == lit.Negation() {118 clauseSat = true119 break120 }121 if lit2 == lit { // duplicate lit122 nbLits--123 c.Set(k, c.Get(nbLits))124 } else {125 k++126 }127 }128 if clauseSat {129 clauseSat = true130 break131 }132 if pb.Model[lit.Var()] == 0 {133 j++134 } else if (pb.Model[lit.Var()] == 1) == lit.IsPositive() {135 clauseSat = true136 break137 } else {138 nbLits--139 c.Set(j, c.Get(nbLits))140 }141 }142 if clauseSat {143 nbClauses--144 pb.Clauses[i] = pb.Clauses[nbClauses]145 } else if nbLits == 0 {146 pb.Status = Unsat147 return148 } else if nbLits == 1 { // UP149 pb.addUnit(c.First())150 if pb.Status == Unsat {151 return152 }153 nbClauses--154 pb.Clauses[i] = pb.Clauses[nbClauses]155 restart = true // Must restart, since this lit might have made one more clause Unit or SAT.156 } else { // nb lits unbound > cardinality157 if c.Len() != nbLits {158 c.Shrink(nbLits)159 }160 i++161 }162 }163 }164 pb.updateStatus(nbClauses)165}166167// DetectAtMostOne tries to detect AtMostOne constraints encoded using the pairwise encoding.168// It replaces those binary clauses by a single cardinality constraint.169// This should mostly be called using the CuttingPlanes option, as it can dramatically improve the resolution process in some cases.170func (pb *Problem) DetectAtMostOne() {171 considered := make([]bool, pb.NbVars*2) // Has lit 1 already been detected in a clique?172 propagates := make([][]Lit, pb.NbVars*2) // For each lit, the literals it propagates in a binary clause173 indexes := make([][]int, len(propagates)) // Indexes of binary clauses, to remove them efficiently174 toRemove := make([]int, 0, 1_000) // Indexes of clauses that have to be removed afterwards175 for i, c := range pb.Clauses {176 if c.Len() == 2 {177 lit1 := c.First()178 neg1 := lit1.Negation()179 lit2 := c.Second()180 neg2 := lit2.Negation()181 propagates[neg1] = append(propagates[neg1], lit2)182 propagates[neg2] = append(propagates[neg2], lit1)183 indexes[neg1] = append(indexes[neg1], i)184 indexes[neg2] = append(indexes[neg2], i)185 }186 }187 for i := range propagates {188 if considered[i] {189 continue190 }191 lit := Lit(i)192 others := propagates[lit]193 if len(others) < 2 { // We won't find a cardinality constraint here194 continue195 }196 constr := []Lit{lit.Negation()}197 for j, other := range others {198 if considered[other] {199 continue200 }201 ok := true202 for j := 1; j < len(constr); j++ {203 lit2 := constr[j].Negation()204 found := false205 for _, lit3 := range propagates[lit2] {206 if lit3 == other {207 found = true208 break209 }210 }211 if !found {212 ok = false213 break214 }215 }216 if ok { // other was found in a binary clause with each literal in constr217 constr = append(constr, other)218 toRemove = append(toRemove, indexes[lit][j])219 }220 }221 if len(constr) > 2 { // We detected a stronger cardinality constraint222 for _, lit := range constr {223 considered[lit.Negation()] = true224 }225 pb.Clauses = append(pb.Clauses, NewCardClause(constr, len(constr)-1))226 }227 }228 pb.removeBinaries(toRemove)229}230231// removeBinaries removes the binary clauses that were used to build the232// hidden cardinality constraint whose lits are given as a parameter.233func (pb *Problem) removeBinaries(toRemove []int) {234 if len(toRemove) == 0 {235 return236 }237 newClauses := make([]*Clause, 0, len(pb.Clauses)-len(toRemove))238 i := 0239 for j, c := range pb.Clauses {240 if j == toRemove[i] {241 i++242 if i == len(toRemove) {243 break244 }245 } else {246 newClauses = append(newClauses, c)247 }248 }249 pb.Clauses = newClauses250}251252// simplifyCard simplifies the problem, i.e runs unit propagation if possible.253func (pb *Problem) simplifyCard() {254 nbClauses := len(pb.Clauses)255 restart := true256 for restart {257 restart = false258 i := 0259 for i < nbClauses {260 c := pb.Clauses[i]261 nbLits := c.Len()262 card := c.Cardinality()263 clauseSat := false264 nbSat := 0265 j := 0266 for j < nbLits {267 lit := c.Get(j)268 if pb.Model[lit.Var()] == 0 {269 j++270 } else if (pb.Model[lit.Var()] == 1) == lit.IsPositive() {271 nbSat++272 if nbSat == card {273 clauseSat = true274 break275 }276 } else {277 nbLits--278 c.Set(j, c.Get(nbLits))279 }280 }281 if clauseSat {282 nbClauses--283 pb.Clauses[i] = pb.Clauses[nbClauses]284 } else if nbLits < card {285 pb.Status = Unsat286 return287 } else if nbLits == card { // UP288 pb.addUnits(c, nbLits)289 if pb.Status == Unsat {290 return291 }292 nbClauses--293 pb.Clauses[i] = pb.Clauses[nbClauses]294 restart = true // Must restart, since this lit might have made one more clause Unit or SAT.295 } else { // nb lits unbound > cardinality296 if c.Len() != nbLits {297 c.Shrink(nbLits)298 }299 i++300 }301 }302 }303 pb.updateStatus(nbClauses)304}305306func (pb *Problem) simplifyPB() {307 pb.replicateUnits()308 modified := true309 for modified {310 modified = false311 i := 0312 for i < len(pb.Clauses) {313 c := pb.Clauses[i]314 j := 0315 card := c.Cardinality()316 wSum := c.WeightSum()317 for j < c.Len() {318 lit := c.Get(j)319 v := lit.Var()320 w := c.Weight(j)321 if pb.Model[v] == 0 { // Literal not assigned: is it unit?322 if wSum-w < card { // Lit must be true for the clause to be satisfiable323 pb.addUnit(lit)324 if pb.Status == Unsat {325 return326 }327 c.removeLit(j)328 card -= w329 c.updateCardinality(-w)330 wSum -= w331 modified = true332 } else {333 j++334 }335 } else { // Bound literal: remove it and update, if needed, cardinality336 wSum -= w337 if (pb.Model[v] == 1) == lit.IsPositive() {338 card -= w339 c.updateCardinality(-w)340 }341 c.removeLit(j)342 modified = true343 }344 }345 if card <= 0 { // Clause is Sat346 pb.Clauses[i] = pb.Clauses[len(pb.Clauses)-1]347 pb.Clauses = pb.Clauses[:len(pb.Clauses)-1]348 modified = true349 } else if wSum < card {350 pb.Clauses = nil351 pb.Status = Unsat352 return353 } else {354 i++355 }356 }357 }358 if pb.Status == Indet && len(pb.Clauses) == 0 {359 pb.Status = Sat360 }361}362363func (pb *Problem) addUnit(lit Lit) {364 if lit.IsPositive() {365 if pb.Model[lit.Var()] == -1 {366 pb.Status = Unsat367 return368 }369 pb.Model[lit.Var()] = 1370 } else {371 if pb.Model[lit.Var()] == 1 {372 pb.Status = Unsat373 return374 }375 pb.Model[lit.Var()] = -1376 }377 pb.Units = append(pb.Units, lit)378}379380func (pb *Problem) addUnits(c *Clause, nbLits int) {381 for i := 0; i < nbLits; i++ {382 lit := c.Get(i)383 pb.addUnit(lit)384 }385}386387func (pb *Problem) replicateUnits() {388 for _, unit := range pb.Units {389 v := unit.Var()390 if unit.IsPositive() {391 pb.Model[v] = 1392 } else {393 pb.Model[v] = -1394 }395 }396}