diff --git a/vendor/github.com/crillab/gophersat/bf/bf.go b/vendor/github.com/crillab/gophersat/bf/bf.go index 5d9552f0..09d3a936 100644 --- a/vendor/github.com/crillab/gophersat/bf/bf.go +++ b/vendor/github.com/crillab/gophersat/bf/bf.go @@ -230,6 +230,8 @@ func (a and) String() string { } func (a and) Eval(model map[string]bool) (res bool) { + res = true + for i, s := range a { b := s.Eval(model) if i == 0 { diff --git a/vendor/github.com/crillab/gophersat/solver/learn.go b/vendor/github.com/crillab/gophersat/solver/learn.go index 53e43c02..3598582f 100644 --- a/vendor/github.com/crillab/gophersat/solver/learn.go +++ b/vendor/github.com/crillab/gophersat/solver/learn.go @@ -29,7 +29,7 @@ func (s *Solver) addClauseLits(confl *Clause, lvl decLevel, met, metLvl []bool, if abs(s.model[v]) == lvl { metLvl[v] = true nbLvl++ - } else if abs(s.model[v]) != 1 { + } else { *lits = append(*lits, l) } } @@ -39,8 +39,9 @@ func (s *Solver) addClauseLits(confl *Clause, lvl decLevel, met, metLvl []bool, var bufLits = make([]Lit, 10000) // Buffer for lits in learnClause. Used to reduce allocations. // learnClause creates a conflict clause and returns either: -// the clause itself, if its len is at least 2. -// a nil clause and a unit literal, if its len is exactly 1. +// - the clause itself, if its len is at least 2, +// - a nil clause and a unit literal, if its len is exactly 1, +// - a nil clause and -1, if the empty clause was learned. func (s *Solver) learnClause(confl *Clause, lvl decLevel) (learned *Clause, unit Lit) { s.clauseBumpActivity(confl) lits := bufLits[:1] // Not 0: make room for asserting literal @@ -58,6 +59,10 @@ func (s *Solver) learnClause(confl *Clause, lvl decLevel) (learned *Clause, unit ptr-- } v := s.trail[ptr].Var() + if s.assumptions[v] { + // Now we only have assumed lits: this is a top-level conflict + return nil, -1 + } ptr-- nbLvl-- if reason := s.reason[v]; reason != nil { @@ -65,7 +70,7 @@ func (s *Solver) learnClause(confl *Clause, lvl decLevel) (learned *Clause, unit for i := 0; i < reason.Len(); i++ { lit := reason.Get(i) if v2 := lit.Var(); !met[v2] { - if s.litStatus(lit) != Unsat { + if s.litStatus(lit) != Unsat { // In clauses where cardinality > 1, some lits might be true in the conflict clause: ignore them continue } met[v2] = true @@ -73,7 +78,7 @@ func (s *Solver) learnClause(confl *Clause, lvl decLevel) (learned *Clause, unit if abs(s.model[v2]) == lvl { metLvl[v2] = true nbLvl++ - } else if abs(s.model[v2]) != 1 { + } else { lits = append(lits, lit) } } @@ -109,7 +114,7 @@ func (s *Solver) minimizeLearned(met []bool, learned []Lit) int { } else { for k := 0; k < reason.Len(); k++ { lit := reason.Get(k) - if !met[lit.Var()] && abs(s.model[lit.Var()]) > 1 { + if !met[lit.Var()] /*&& abs(s.model[lit.Var()]) > 1*/ { learned[sz] = learned[i] sz++ break diff --git a/vendor/github.com/crillab/gophersat/solver/parser.go b/vendor/github.com/crillab/gophersat/solver/parser.go index 050eaa66..e0903a16 100644 --- a/vendor/github.com/crillab/gophersat/solver/parser.go +++ b/vendor/github.com/crillab/gophersat/solver/parser.go @@ -12,11 +12,25 @@ import ( // The argument is supposed to be a well-formed CNF. func ParseSlice(cnf [][]int) *Problem { var pb Problem + pb.parseSlice(cnf) + return &pb +} + +// ParseSliceNb parse a slice of slice of lits and returns the equivalent problem. +// The argument is supposed to be a well-formed CNF. +// The number of vars is provided because clauses might be added to it later. +func ParseSliceNb(cnf [][]int, nbVars int) *Problem { + pb := Problem{NbVars: nbVars} + pb.parseSlice(cnf) + return &pb +} + +func (pb *Problem) parseSlice(cnf [][]int) { for _, line := range cnf { switch len(line) { case 0: pb.Status = Unsat - return &pb + return case 1: if line[0] == 0 { panic("null unit clause") @@ -31,7 +45,7 @@ func ParseSlice(cnf [][]int) *Problem { lits := make([]Lit, len(line)) for j, val := range line { if val == 0 { - panic("null literal in clause %q") + panic(fmt.Sprintf("null literal in clause %v", lits)) } lits[j] = IntToLit(int32(val)) if v := int(lits[j].Var()); v >= pb.NbVars { @@ -52,11 +66,10 @@ func ParseSlice(cnf [][]int) *Problem { } } else if pb.Model[v] > 0 != unit.IsPositive() { pb.Status = Unsat - return &pb + return } } pb.simplify2() - return &pb } func isSpace(b byte) bool { diff --git a/vendor/github.com/crillab/gophersat/solver/problem.go b/vendor/github.com/crillab/gophersat/solver/problem.go index 69eecf6b..84edd15c 100644 --- a/vendor/github.com/crillab/gophersat/solver/problem.go +++ b/vendor/github.com/crillab/gophersat/solver/problem.go @@ -97,26 +97,6 @@ func (pb *Problem) updateStatus(nbClauses int) { } } -func (pb *Problem) simplify() { - idxClauses := make([][]int, pb.NbVars*2) // For each lit, indexes of clauses it appears in - removed := make([]bool, len(pb.Clauses)) // Clauses that have to be removed - for i := range pb.Clauses { - pb.simplifyClause(i, idxClauses, removed) - if pb.Status == Unsat { - return - } - } - for i := 0; i < len(pb.Units); i++ { - lit := pb.Units[i] - neg := lit.Negation() - clauses := idxClauses[neg] - for j := range clauses { - pb.simplifyClause(j, idxClauses, removed) - } - } - pb.rmClauses(removed) -} - func (pb *Problem) simplifyClause(idx int, idxClauses [][]int, removed []bool) { c := pb.Clauses[idx] k := 0 diff --git a/vendor/github.com/crillab/gophersat/solver/solver.go b/vendor/github.com/crillab/gophersat/solver/solver.go index ec014412..3d1662d8 100644 --- a/vendor/github.com/crillab/gophersat/solver/solver.go +++ b/vendor/github.com/crillab/gophersat/solver/solver.go @@ -54,15 +54,18 @@ func (m Model) String() string { // A Solver solves a given problem. It is the main data structure. type Solver struct { - Verbose bool // Indicates whether the solver should display information during solving or not. False by default - nbVars int - status Status - wl watcherList - trail []Lit // Current assignment stack - model Model // 0 means unbound, other value is a binding - lastModel Model // Placeholder for last model found, useful when looking for several models - activity []float64 // How often each var is involved in conflicts - polarity []bool // Preferred sign for each var + Verbose bool // Indicates whether the solver should display information during solving or not. False by default + Certified bool // Indicates whether a certificate should be generated during solving or not, using the RUP notation. This is useful to prove UNSAT instances. False by default. + CertChan chan string // Indicates where to write the certificate. If Certified is true but CertChan is nil, the certificate will be written on stdout. + nbVars int + status Status + wl watcherList + trail []Lit // Current assignment stack + model Model // 0 means unbound, other value is a binding + lastModel Model // Placeholder for last model found, useful when looking for several models + activity []float64 // How often each var is involved in conflicts + polarity []bool // Preferred sign for each var + assumptions []bool // True iff the var's binding is assumed // For each var, clause considered when it was unified // If the var is not bound yet, or if it was bound by a decision, value is nil. reason []*Clause @@ -73,7 +76,7 @@ type Solver struct { Stats Stats // Statistics about the solving process. minLits []Lit // Lits to minimize if the problem was an optimization problem. minWeights []int // Weight of each lit to minimize if the problem was an optimization problem. - asumptions []Lit // Literals that are, ideally, true. Useful when trying to minimize a function. + hypothesis []Lit // Literals that are, ideally, true. Useful when trying to minimize a function. localNbRestarts int // How many restarts since Solve() was called? varDecay float64 // On each var decay, how much the varInc should be decayed trailBuf []int // A buffer while cleaning bindings @@ -94,19 +97,20 @@ func New(problem *Problem) *Solver { } s := &Solver{ - nbVars: nbVars, - status: problem.Status, - trail: make([]Lit, len(problem.Units), trailCap), - model: problem.Model, - activity: make([]float64, nbVars), - polarity: make([]bool, nbVars), - reason: make([]*Clause, nbVars), - varInc: 1.0, - clauseInc: 1.0, - minLits: problem.minLits, - minWeights: problem.minWeights, - varDecay: defaultVarDecay, - trailBuf: make([]int, nbVars), + nbVars: nbVars, + status: problem.Status, + trail: make([]Lit, len(problem.Units), trailCap), + model: problem.Model, + activity: make([]float64, nbVars), + polarity: make([]bool, nbVars), + assumptions: make([]bool, nbVars), + reason: make([]*Clause, nbVars), + varInc: 1.0, + clauseInc: 1.0, + minLits: problem.minLits, + minWeights: problem.minWeights, + varDecay: defaultVarDecay, + trailBuf: make([]int, nbVars), } s.resetOptimPolarity() s.initOptimActivity() @@ -322,26 +326,11 @@ func (s *Solver) rebuildOrderHeap() { s.varQueue.build(ints) } -// satClause returns true iff c is satisfied by a literal assigned at top level. -func (s *Solver) satClause(c *Clause) bool { - if c.Len() == 2 || c.Cardinality() != 1 || c.PseudoBoolean() { - // TODO improve this, but it will be ok since we only call this function for removing useless clauses. - return false - } - for i := 0; i < c.Len(); i++ { - lit := c.Get(i) - assign := s.model[lit.Var()] - if assign == 1 && lit.IsPositive() || assign == -1 && !lit.IsPositive() { - return true - } - } - return false -} - // propagate binds the given lit, propagates it and searches for a solution, // until it is found or a restart is needed. func (s *Solver) propagateAndSearch(lit Lit, lvl decLevel) Status { for lit != -1 { + // log.Printf("picked %d at lvl %d", lit.Int(), lvl) if conflict := s.unifyLiteral(lit, lvl); conflict == nil { // Pick new branch or restart if s.lbdStats.mustRestart() { s.lbdStats.clear() @@ -363,15 +352,17 @@ func (s *Solver) propagateAndSearch(lit Lit, lvl decLevel) Status { s.lbdStats.addConflict(len(s.trail)) learnt, unit := s.learnClause(conflict, lvl) if learnt == nil { // Unit clause was learned: this lit is known for sure + if unit == -1 || (abs(s.model[unit.Var()]) == 1 && s.litStatus(unit) == Unsat) { // Top-level conflict + return s.setUnsat() + } s.Stats.NbUnitLearned++ s.lbdStats.addLbd(1) s.cleanupBindings(1) + s.addLearnedUnit(unit) s.model[unit.Var()] = lvlToSignedLvl(unit, 1) if conflict = s.unifyLiteral(unit, 1); conflict != nil { // top-level conflict - s.status = Unsat - return Unsat + return s.setUnsat() } - // s.rmSatClauses() s.rebuildOrderHeap() lit = s.chooseLit() lvl = 2 @@ -392,6 +383,19 @@ func (s *Solver) propagateAndSearch(lit Lit, lvl decLevel) Status { return Sat } +// Sets the status to unsat and do cleanup tasks. +func (s *Solver) setUnsat() Status { + if s.Certified { + if s.CertChan == nil { + fmt.Printf("0\n") + } else { + s.CertChan <- "0" + } + } + s.status = Unsat + return Unsat +} + // Searches until a restart is needed. func (s *Solver) search() Status { s.localNbRestarts++ @@ -455,6 +459,28 @@ func (s *Solver) Solve() Status { return s.status } +// Assume adds unit literals to the solver. +// This is useful when calling the solver several times, e.g to keep it "hot" while removing clauses. +func (s *Solver) Assume(lits []Lit) Status { + s.cleanupBindings(0) + s.trail = s.trail[:0] + s.assumptions = make([]bool, s.nbVars) + + for _, lit := range lits { + + s.addLearnedUnit(lit) + s.assumptions[lit.Var()] = true + s.trail = append(s.trail, lit) + } + s.status = Indet + if confl := s.propagate(0, 1); confl != nil { + // Conflict after unit propagation + s.status = Unsat + return s.status + } + return s.status +} + // Enumerate returns the total number of models for the given problems. // if "models" is non-nil, it will write models on it as soon as it discovers them. // models will be closed at the end of the method. @@ -474,10 +500,11 @@ func (s *Solver) Enumerate(models chan []bool, stop chan struct{}) int { } } if s.status == Sat { - nb++ + copy(s.lastModel, s.model) if models != nil { - copy(s.lastModel, s.model) - models <- s.Model() + nb += s.addCurrentModels(models) + } else { + nb += s.countCurrentModels() } s.status = Indet lits := s.decisionLits() @@ -543,7 +570,8 @@ func (s *Solver) CountModels() int { } } if s.status == Sat { - nb++ + s.lastModel = s.model + nb += s.countCurrentModels() if s.Verbose { fmt.Printf("c found %d model(s)\n", nb) } @@ -695,6 +723,52 @@ func (s *Solver) Model() []bool { return res } +// addCurrentModels is called when a model was found. +// It returns the total number of models from this point, and sends all models on ch. +// The number can be different of 1 if there are unbound variables. +// For instance, if there are 4 variables in the problem and only 1, 3 and 4 are bound, +// there are actually 2 models currently: one with 2 set to true, the other with 2 set to false. +func (s *Solver) addCurrentModels(ch chan []bool) int { + unbound := make([]int, 0, s.nbVars) // indices of unbound variables + var nb uint64 = 1 // total number of models found + model := make([]bool, s.nbVars) // partial model + for i, lvl := range s.lastModel { + if lvl == 0 { + unbound = append(unbound, i) + nb *= 2 + } else { + model[i] = lvl > 0 + } + } + for i := uint64(0); i < nb; i++ { + for j := range unbound { + mask := uint64(1 << j) + cur := i & mask + idx := unbound[j] + model[idx] = cur != 0 + } + model2 := make([]bool, len(model)) + copy(model2, model) + ch <- model2 + } + return int(nb) +} + +// countCurrentModels is called when a model was found. +// It returns the total number of models from this point. +// The number can be different of 1 if there are unbound variables. +// For instance, if there are 4 variables in the problem and only 1, 3 and 4 are bound, +// there are actually 2 models currently: one with 2 set to true, the other with 2 set to false. +func (s *Solver) countCurrentModels() int { + var nb uint64 = 1 // total number of models found + for _, lvl := range s.lastModel { + if lvl == 0 { + nb *= 2 + } + } + return int(nb) +} + // Optimal returns the optimal solution, if any. // If results is non-nil, all solutions will be written to it. // In any case, results will be closed at the end of the call. @@ -731,13 +805,13 @@ func (s *Solver) Optimal(results chan Result, stop chan struct{}) (res Result) { maxCost += w } } - s.asumptions = make([]Lit, len(s.minLits)) + s.hypothesis = make([]Lit, len(s.minLits)) for i, lit := range s.minLits { - s.asumptions[i] = lit.Negation() + s.hypothesis[i] = lit.Negation() } weights := make([]int, len(s.minWeights)) copy(weights, s.minWeights) - sort.Sort(wLits{lits: s.asumptions, weights: weights}) + sort.Sort(wLits{lits: s.hypothesis, weights: weights}) s.lastModel = make(Model, len(s.model)) var cost int for status == Sat { @@ -766,7 +840,7 @@ func (s *Solver) Optimal(results chan Result, stop chan struct{}) (res Result) { // Add a constraint incrementing current best cost lits2 := make([]Lit, len(s.minLits)) weights2 := make([]int, len(s.minWeights)) - copy(lits2, s.asumptions) + copy(lits2, s.hypothesis) copy(weights2, weights) s.AppendClause(NewPBClause(lits2, weights2, maxCost-cost+1)) s.rebuildOrderHeap() @@ -796,13 +870,13 @@ func (s *Solver) Minimize() int { maxCost += w } } - s.asumptions = make([]Lit, len(s.minLits)) + s.hypothesis = make([]Lit, len(s.minLits)) for i, lit := range s.minLits { - s.asumptions[i] = lit.Negation() + s.hypothesis[i] = lit.Negation() } weights := make([]int, len(s.minWeights)) copy(weights, s.minWeights) - sort.Sort(wLits{lits: s.asumptions, weights: weights}) + sort.Sort(wLits{lits: s.hypothesis, weights: weights}) s.lastModel = make(Model, len(s.model)) var cost int for status == Sat { @@ -826,7 +900,7 @@ func (s *Solver) Minimize() int { // Add a constraint incrementing current best cost lits2 := make([]Lit, len(s.minLits)) weights2 := make([]int, len(s.minWeights)) - copy(lits2, s.asumptions) + copy(lits2, s.hypothesis) copy(weights2, weights) s.AppendClause(NewPBClause(lits2, weights2, maxCost-cost+1)) s.rebuildOrderHeap() @@ -835,7 +909,7 @@ func (s *Solver) Minimize() int { return cost } -// functions to sort asumptions for pseudo-boolean minimization clause. +// functions to sort hypothesis for pseudo-boolean minimization clause. type wLits struct { lits []Lit weights []int diff --git a/vendor/github.com/crillab/gophersat/solver/types.go b/vendor/github.com/crillab/gophersat/solver/types.go index 48c4624e..66017ba6 100644 --- a/vendor/github.com/crillab/gophersat/solver/types.go +++ b/vendor/github.com/crillab/gophersat/solver/types.go @@ -42,6 +42,17 @@ type Var int32 // Thus the CNF literal -3 is encoded as 2 * (3-1) + 1 = 5. type Lit int32 +// IntsToLits converts a list of CNF literals to a []Lit. +// This is a helper function as the same result can be achieved by calling +// IntToLit several times. +func IntsToLits(vals ...int32) []Lit { + res := make([]Lit, len(vals)) + for i, val := range vals { + res[i] = IntToLit(val) + } + return res +} + // IntToLit converts a CNF literal to a Lit. func IntToLit(i int32) Lit { if i < 0 { diff --git a/vendor/github.com/crillab/gophersat/solver/watcher.go b/vendor/github.com/crillab/gophersat/solver/watcher.go index 9d263ef2..2948fdc2 100644 --- a/vendor/github.com/crillab/gophersat/solver/watcher.go +++ b/vendor/github.com/crillab/gophersat/solver/watcher.go @@ -1,6 +1,9 @@ package solver -import "sort" +import ( + "fmt" + "sort" +) type watcher struct { other Lit // Another lit from the clause @@ -153,6 +156,26 @@ func (s *Solver) addLearned(c *Clause) { s.wl.learned = append(s.wl.learned, c) s.watchClause(c) s.clauseBumpActivity(c) + if s.Certified { + if s.CertChan == nil { + fmt.Printf("%s\n", c.CNF()) + } else { + s.CertChan <- c.CNF() + } + } +} + +// Adds the given unit literal to the model at the top level. +func (s *Solver) addLearnedUnit(unit Lit) { + + s.model[unit.Var()] = lvlToSignedLvl(unit, 1) + if s.Certified { + if s.CertChan == nil { + fmt.Printf("%d 0\n", unit.Int()) + } else { + s.CertChan <- fmt.Sprintf("%d 0", unit.Int()) + } + } } // If l is negative, -lvl is returned. Else, lvl is returned. diff --git a/vendor/github.com/stevenle/topsort/.gitignore b/vendor/github.com/mudler/topsort/.gitignore similarity index 100% rename from vendor/github.com/stevenle/topsort/.gitignore rename to vendor/github.com/mudler/topsort/.gitignore diff --git a/vendor/github.com/stevenle/topsort/LICENSE b/vendor/github.com/mudler/topsort/LICENSE similarity index 100% rename from vendor/github.com/stevenle/topsort/LICENSE rename to vendor/github.com/mudler/topsort/LICENSE diff --git a/vendor/github.com/stevenle/topsort/README.md b/vendor/github.com/mudler/topsort/README.md similarity index 100% rename from vendor/github.com/stevenle/topsort/README.md rename to vendor/github.com/mudler/topsort/README.md diff --git a/vendor/github.com/stevenle/topsort/topsort.go b/vendor/github.com/mudler/topsort/topsort.go similarity index 98% rename from vendor/github.com/stevenle/topsort/topsort.go rename to vendor/github.com/mudler/topsort/topsort.go index d53133a1..14498836 100644 --- a/vendor/github.com/stevenle/topsort/topsort.go +++ b/vendor/github.com/mudler/topsort/topsort.go @@ -16,6 +16,7 @@ package topsort import ( "fmt" + "sort" "strings" ) @@ -98,6 +99,7 @@ func (n node) edges() []string { for k := range n { keys = append(keys, k) } + sort.Strings(keys) return keys } diff --git a/vendor/modules.txt b/vendor/modules.txt index 38644cdb..89b493e5 100644 --- a/vendor/modules.txt +++ b/vendor/modules.txt @@ -59,7 +59,7 @@ github.com/containerd/continuity/syscallx github.com/containerd/continuity/sysx # github.com/cpuguy83/go-md2man/v2 v2.0.0 github.com/cpuguy83/go-md2man/v2/md2man -# github.com/crillab/gophersat v1.1.9-0.20200211102949-9a8bf7f2f0a3 +# github.com/crillab/gophersat v1.3.2-0.20201023142334-3fc2ac466765 github.com/crillab/gophersat/bf github.com/crillab/gophersat/solver # github.com/cyphar/filepath-securejoin v0.2.2 @@ -211,6 +211,8 @@ github.com/morikuni/aec github.com/mudler/cobra-extensions # github.com/mudler/docker-companion v0.4.6-0.20200418093252-41846f112d87 github.com/mudler/docker-companion/api +# github.com/mudler/topsort v0.0.0-20201103161459-db5c7901c290 +github.com/mudler/topsort # github.com/nxadm/tail v1.4.4 github.com/nxadm/tail github.com/nxadm/tail/ratelimiter @@ -303,8 +305,6 @@ github.com/spf13/jwalterweatherman github.com/spf13/pflag # github.com/spf13/viper v1.6.3 github.com/spf13/viper -# github.com/stevenle/topsort v0.0.0-20130922064739-8130c1d7596b -github.com/stevenle/topsort # github.com/subosito/gotenv v1.2.0 github.com/subosito/gotenv # github.com/urfave/cli v1.22.1