1package solver23//4// import "log"5//6// // Subsumes returns true iff c subsumes c2.7// func (c *Clause) Subsumes(c2 *Clause) bool {8// if c.Len() > c2.Len() {9// return false10// }11// for _, lit := range c.lits {12// found := false13// for _, lit2 := range c2.lits {14// if lit == lit2 {15// found = true16// break17// }18// if lit2 > lit {19// return false20// }21// }22// if !found {23// return false24// }25// }26// return true27// }28//29// // SelfSubsumes returns true iff c self-subsumes c2.30// func (c *Clause) SelfSubsumes(c2 *Clause) bool {31// oneNeg := false32// for _, lit := range c.lits {33// found := false34// for _, lit2 := range c2.lits {35// if lit == lit2 {36// found = true37// break38// }39// if lit == lit2.Negation() {40// if oneNeg { // We want exactly one, but this is the second41// return false42// }43// oneNeg = true44// found = true45// break46// }47// if lit2 > lit { // We won't find it anymore48// return false49// }50// }51// if !found {52// return false53// }54// }55// return oneNeg56// }57//58// // Simplify simplifies the given clause by removing redundant lits.59// // If the clause is trivially satisfied (i.e contains both a lit and its negation),60// // true is returned. Otherwise, false is returned.61// func (c *Clause) Simplify() (isSat bool) {62// c.Sort()63// lits := make([]Lit, 0, len(c.lits))64// i := 065// for i < len(c.lits) {66// if i < len(c.lits)-1 && c.lits[i] == c.lits[i+1].Negation() {67// return true68// }69// lit := c.lits[i]70// lits = append(lits, lit)71// i++72// for i < len(c.lits) && c.lits[i] == lit {73// i++74// }75// }76// if len(lits) < len(c.lits) {77// c.lits = lits78// }79// return false80// }81//82// // Generate returns a subsumed clause from c and c2, by removing v.83// func (c *Clause) Generate(c2 *Clause, v Var) *Clause {84// c3 := &Clause{lits: make([]Lit, 0, len(c.lits)+len(c2.lits)-2)}85// for _, lit := range c.lits {86// if lit.Var() != v {87// c3.lits = append(c3.lits, lit)88// }89// }90// for _, lit2 := range c2.lits {91// if lit2.Var() != v {92// c3.lits = append(c3.lits, lit2)93// }94// }95// return c396// }97//98// func (pb *Problem) preprocess() {99// log.Printf("Preprocessing... %d clauses currently", len(pb.Clauses))100// occurs := make([][]int, pb.NbVars*2)101// for i, c := range pb.Clauses {102// for j := 0; j < c.Len(); j++ {103// occurs[c.Get(j)] = append(occurs[c.Get(j)], i)104// }105// }106// modified := true107// neverModified := true108// for modified {109// modified = false110// for i := 0; i < pb.NbVars; i++ {111// if pb.Model[i] != 0 {112// continue113// }114// v := Var(i)115// lit := v.Lit()116// nbLit := len(occurs[lit])117// nbLit2 := len(occurs[lit.Negation()])118// if (nbLit < 10 || nbLit2 < 10) && (nbLit != 0 || nbLit2 != 0) {119// modified = true120// neverModified = false121// // pb.deleted[v] = true122// log.Printf("%d can be removed: %d and %d", lit.Int(), len(occurs[lit]), len(occurs[lit.Negation()]))123// for _, idx1 := range occurs[lit] {124// for _, idx2 := range occurs[lit.Negation()] {125// c1 := pb.Clauses[idx1]126// c2 := pb.Clauses[idx2]127// newC := c1.Generate(c2, v)128// if !newC.Simplify() {129// switch newC.Len() {130// case 0:131// log.Printf("Inferred UNSAT")132// pb.Status = Unsat133// return134// case 1:135// log.Printf("Unit %d", newC.First().Int())136// lit2 := newC.First()137// if lit2.IsPositive() {138// if pb.Model[lit2.Var()] == -1 {139// pb.Status = Unsat140// return141// }142// pb.Model[lit2.Var()] = 1143// } else {144// if pb.Model[lit2.Var()] == 1 {145// pb.Status = Unsat146// return147// }148// pb.Model[lit2.Var()] = -1149// }150// pb.Units = append(pb.Units, lit2)151// default:152// pb.Clauses = append(pb.Clauses, newC)153// }154// }155// }156// }157// nbRemoved := 0158// for _, idx := range occurs[lit] {159// pb.Clauses[idx] = pb.Clauses[len(pb.Clauses)-nbRemoved-1]160// nbRemoved++161// }162// for _, idx := range occurs[lit.Negation()] {163// pb.Clauses[idx] = pb.Clauses[len(pb.Clauses)-nbRemoved-1]164// nbRemoved++165// }166// pb.Clauses = pb.Clauses[:len(pb.Clauses)-nbRemoved]167// log.Printf("clauses=%s", pb.CNF())168// // Redo occurs169// occurs = make([][]int, pb.NbVars*2)170// for i, c := range pb.Clauses {171// for j := 0; j < c.Len(); j++ {172// occurs[c.Get(j)] = append(occurs[c.Get(j)], i)173// }174// }175// continue176// }177// }178// }179// if !neverModified {180// pb.simplify()181// }182// log.Printf("Done. %d clauses now", len(pb.Clauses))183// }