Revert "update vendor/"

This reverts commit 7ce522110e.

vendor/github.com/crillab/gophersat/LICENSE

@@ -0,0 +1,7 @@
+Copyright (c) 2017 Centre de Recherche en Informatique de Lens  and contributors
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

vendor/github.com/crillab/gophersat/bf/bf.go

@@ -0,0 +1,480 @@
+package bf
+
+import (
+	"fmt"
+	"io"
+	"math"
+	"sort"
+	"strconv"
+	"strings"
+
+	"github.com/crillab/gophersat/solver"
+)
+
+// A Formula is any kind of boolean formula, not necessarily in CNF.
+type Formula interface {
+	nnf() Formula
+	String() string
+	Eval(model map[string]bool) bool
+}
+
+// Solve solves the given formula.
+// f is first converted as a CNF formula. It is then given to gophersat.
+// The function returns a model associating each variable name with its binding, or nil if the formula was not satisfiable.
+func Solve(f Formula) map[string]bool {
+	return asCnf(f).solve()
+}
+
+// Dimacs writes the DIMACS CNF version of the formula on w.
+// It is useful so as to feed it to any SAT solver.
+// The original names of variables is associated with their DIMACS integer counterparts
+// in comments, between the prolog and the set of clauses.
+// For instance, if the variable "a" is associated with the index 1, there will be a comment line
+// "c a=1".
+func Dimacs(f Formula, w io.Writer) error {
+	cnf := asCnf(f)
+	nbVars := len(cnf.vars.all)
+	nbClauses := len(cnf.clauses)
+	prefix := fmt.Sprintf("p cnf %d %d\n", nbVars, nbClauses)
+	if _, err := io.WriteString(w, prefix); err != nil {
+		return fmt.Errorf("could not write DIMACS output: %v", err)
+	}
+	var pbVars []string
+	for v := range cnf.vars.pb {
+		if !v.dummy {
+			pbVars = append(pbVars, v.name)
+		}
+	}
+	sort.Sort(sort.StringSlice(pbVars))
+	for _, v := range pbVars {
+		idx := cnf.vars.pb[pbVar(v)]
+		line := fmt.Sprintf("c %s=%d\n", v, idx)
+		if _, err := io.WriteString(w, line); err != nil {
+			return fmt.Errorf("could not write DIMACS output: %v", err)
+		}
+	}
+	for _, clause := range cnf.clauses {
+		strClause := make([]string, len(clause))
+		for i, lit := range clause {
+			strClause[i] = strconv.Itoa(lit)
+		}
+		line := fmt.Sprintf("%s 0\n", strings.Join(strClause, " "))
+		if _, err := io.WriteString(w, line); err != nil {
+			return fmt.Errorf("could not write DIMACS output: %v", err)
+		}
+	}
+	return nil
+}
+
+// The "true" constant.
+type trueConst struct{}
+
+// True is the constant denoting a tautology.
+var True Formula = trueConst{}
+
+func (t trueConst) nnf() Formula   { return t }
+func (t trueConst) String() string { return "⊤" }
+func (t trueConst) Eval(model map[string]bool) bool { return true }
+
+// The "false" constant.
+type falseConst struct{}
+
+// False is the constant denoting a contradiction.
+var False Formula = falseConst{}
+
+func (f falseConst) nnf() Formula   { return f }
+func (f falseConst) String() string { return "⊥" }
+func (f falseConst) Eval(model map[string]bool) bool { return false }
+
+// Var generates a named boolean variable in a formula.
+func Var(name string) Formula {
+	return pbVar(name)
+}
+
+func pbVar(name string) variable {
+	return variable{name: name, dummy: false}
+}
+
+func dummyVar(name string) variable {
+	return variable{name: name, dummy: true}
+}
+
+type variable struct {
+	name  string
+	dummy bool
+}
+
+func (v variable) nnf() Formula {
+	return lit{signed: false, v: v}
+}
+
+func (v variable) String() string {
+	return v.name
+}
+
+func (v variable) Eval(model map[string]bool) bool {
+	b, ok := model[v.name]
+	if !ok {
+		panic(fmt.Errorf("Model lacks binding for variable %s", v.name))
+	}
+	return b
+}
+
+type lit struct {
+	v      variable
+	signed bool
+}
+
+func (l lit) nnf() Formula {
+	return l
+}
+
+func (l lit) String() string {
+	if l.signed {
+		return "not(" + l.v.name + ")"
+	}
+	return l.v.name
+}
+
+func (l lit) Eval(model map[string]bool) bool {
+	b := l.v.Eval(model)
+	if l.signed {
+		return !b
+	}
+	return b
+}
+
+// Not represents a negation. It negates the given subformula.
+func Not(f Formula) Formula {
+	return not{f}
+}
+
+type not [1]Formula
+
+func (n not) nnf() Formula {
+	switch f := n[0].(type) {
+	case variable:
+		l := f.nnf().(lit)
+		l.signed = true
+		return l
+	case lit:
+		f.signed = !f.signed
+		return f
+	case not:
+		return f[0].nnf()
+	case and:
+		subs := make([]Formula, len(f))
+		for i, sub := range f {
+			subs[i] = not{sub}.nnf()
+		}
+		return or(subs).nnf()
+	case or:
+		subs := make([]Formula, len(f))
+		for i, sub := range f {
+			subs[i] = not{sub}.nnf()
+		}
+		return and(subs).nnf()
+	case trueConst:
+		return False
+	case falseConst:
+		return True
+	default:
+		panic("invalid formula type")
+	}
+}
+
+func (n not) String() string {
+	return "not(" + n[0].String() + ")"
+}
+
+func (n not) Eval(model map[string]bool) bool {
+	return !n[0].Eval(model)
+}
+
+// And generates a conjunction of subformulas.
+func And(subs ...Formula) Formula {
+	return and(subs)
+}
+
+type and []Formula
+
+func (a and) nnf() Formula {
+	var res and
+	for _, s := range a {
+		nnf := s.nnf()
+		switch nnf := nnf.(type) {
+		case and: // Simplify: "and"s in the "and" get to the higher level
+			res = append(res, nnf...)
+		case trueConst: // True is ignored
+		case falseConst:
+			return False
+		default:
+			res = append(res, nnf)
+		}
+	}
+	if len(res) == 1 {
+		return res[0]
+	}
+	if len(res) == 0 {
+		return False
+	}
+	return res
+}
+
+func (a and) String() string {
+	strs := make([]string, len(a))
+	for i, f := range a {
+		strs[i] = f.String()
+	}
+	return "and(" + strings.Join(strs, ", ") + ")"
+}
+
+func (a and) Eval(model map[string]bool) (res bool) {
+	for i, s := range a {
+		b := s.Eval(model)
+		if i == 0 {
+			res = b
+		} else {
+			res = res && b
+		}
+	}
+	return
+}
+
+// Or generates a disjunction of subformulas.
+func Or(subs ...Formula) Formula {
+	return or(subs)
+}
+
+type or []Formula
+
+func (o or) nnf() Formula {
+	var res or
+	for _, s := range o {
+		nnf := s.nnf()
+		switch nnf := nnf.(type) {
+		case or: // Simplify: "or"s in the "or" get to the higher level
+			res = append(res, nnf...)
+		case falseConst: // False is ignored
+		case trueConst:
+			return True
+		default:
+			res = append(res, nnf)
+		}
+	}
+	if len(res) == 1 {
+		return res[0]
+	}
+	if len(res) == 0 {
+		return True
+	}
+	return res
+}
+
+func (o or) String() string {
+	strs := make([]string, len(o))
+	for i, f := range o {
+		strs[i] = f.String()
+	}
+	return "or(" + strings.Join(strs, ", ") + ")"
+}
+
+func (o or) Eval(model map[string]bool) (res bool) {
+	for i, s := range o {
+		b := s.Eval(model)
+		if i == 0 {
+			res = b
+		} else {
+			res = res || b
+		}
+	}
+	return
+}
+
+// Implies indicates a subformula implies another one.
+func Implies(f1, f2 Formula) Formula {
+	return or{not{f1}, f2}
+}
+
+// Eq indicates a subformula is equivalent to another one.
+func Eq(f1, f2 Formula) Formula {
+	return and{or{not{f1}, f2}, or{f1, not{f2}}}
+}
+
+// Xor indicates exactly one of the two given subformulas is true.
+func Xor(f1, f2 Formula) Formula {
+	return and{or{not{f1}, not{f2}}, or{f1, f2}}
+}
+
+// Unique indicates exactly one of the given variables must be true.
+// It might create dummy variables to reduce the number of generated clauses.
+func Unique(vars ...string) Formula {
+	vars2 := make([]variable, len(vars))
+	for i, v := range vars {
+		vars2[i] = pbVar(v)
+	}
+	return uniqueRec(vars2...)
+}
+
+// uniqueSmall generates clauses indicating exactly one of the given variables is true.
+// It is suitable when the number of variables is small (typically, <= 4).
+func uniqueSmall(vars ...variable) Formula {
+	res := make([]Formula, 1, 1+(len(vars)*len(vars)-1)/2)
+	varsAsForms := make([]Formula, len(vars))
+	for i, v := range vars {
+		varsAsForms[i] = v
+	}
+	res[0] = Or(varsAsForms...)
+	for i := 0; i < len(vars)-1; i++ {
+		for j := i + 1; j < len(vars); j++ {
+			res = append(res, Or(Not(varsAsForms[i]), Not(varsAsForms[j])))
+		}
+	}
+	return And(res...)
+}
+
+func uniqueRec(vars ...variable) Formula {
+	nbVars := len(vars)
+	if nbVars <= 4 {
+		return uniqueSmall(vars...)
+	}
+	sqrt := math.Sqrt(float64(nbVars))
+	nbLines := int(sqrt + 0.5)
+	lines := make([]variable, nbLines)
+	linesF := make([][]Formula, nbLines)
+	allNames := make([]string, len(vars))
+	for i := range vars {
+		allNames[i] = vars[i].name
+	}
+	fullName := strings.Join(allNames, "-")
+	for i := range lines {
+		lines[i] = dummyVar(fmt.Sprintf("line-%d-%s", i, fullName))
+		linesF[i] = []Formula{}
+	}
+	nbCols := int(math.Ceil(sqrt))
+	cols := make([]variable, nbCols)
+	colsF := make([][]Formula, nbCols)
+	for i := range cols {
+		cols[i] = dummyVar(fmt.Sprintf("col-%d-%s", i, fullName))
+		colsF[i] = []Formula{}
+	}
+	res := make([]Formula, 0, 2*nbVars+1)
+	for i, v := range vars {
+		linesF[i/nbCols] = append(linesF[i/nbCols], v)
+		colsF[i%nbCols] = append(colsF[i%nbCols], v)
+	}
+	for i := range lines {
+		res = append(res, Eq(lines[i], Or(linesF[i]...)))
+	}
+	for i := range cols {
+		res = append(res, Eq(cols[i], Or(colsF[i]...)))
+	}
+
+	res = append(res, uniqueRec(lines...))
+	res = append(res, uniqueRec(cols...))
+	return And(res...)
+}
+
+// vars associate variable names with numeric indices.
+type vars struct {
+	all map[variable]int // all vars, including those created when converting the formula
+	pb  map[variable]int // Only the vars that appeared orinigally in the problem
+}
+
+// litValue returns the int value associated with the given problem var.
+// If the var was not referenced yet, it is created first.
+func (vars *vars) litValue(l lit) int {
+	val, ok := vars.all[l.v]
+	if !ok {
+		val = len(vars.all) + 1
+		vars.all[l.v] = val
+		vars.pb[l.v] = val
+	}
+	if l.signed {
+		return -val
+	}
+	return val
+}
+
+// Dummy creates a dummy variable and returns its associated index.
+func (vars *vars) dummy() int {
+	val := len(vars.all) + 1
+	vars.all[dummyVar(fmt.Sprintf("dummy-%d", val))] = val
+	return val
+}
+
+// A CNF is the representation of a boolean formula as a conjunction of disjunction.
+// It can be solved by a SAT solver.
+type cnf struct {
+	vars    vars
+	clauses [][]int
+}
+
+// solve solves the given formula.
+// cnf is given to gophersat.
+// If it is satisfiable, the function returns a model, associating each variable name with its binding.
+// Else, the function returns nil.
+func (cnf *cnf) solve() map[string]bool {
+	pb := solver.ParseSlice(cnf.clauses)
+	s := solver.New(pb)
+	if s.Solve() != solver.Sat {
+		return nil
+	}
+	m := s.Model()
+	vars := make(map[string]bool)
+	for v, idx := range cnf.vars.pb {
+		vars[v.name] = m[idx-1]
+	}
+	return vars
+}
+
+// asCnf returns a CNF representation of the given formula.
+func asCnf(f Formula) *cnf {
+	vars := vars{all: make(map[variable]int), pb: make(map[variable]int)}
+	clauses := cnfRec(f.nnf(), &vars)
+	return &cnf{vars: vars, clauses: clauses}
+}
+
+// transforms the f NNF formula into a CNF formula.
+// nbDummies is the current number of dummy variables created.
+// Note: code should be improved, there are a few useless allocs/deallocs
+// here and there.
+func cnfRec(f Formula, vars *vars) [][]int {
+	switch f := f.(type) {
+	case lit:
+		return [][]int{{vars.litValue(f)}}
+	case and:
+		var res [][]int
+		for _, sub := range f {
+			res = append(res, cnfRec(sub, vars)...)
+		}
+		return res
+	case or:
+		var res [][]int
+		var lits []int
+		for _, sub := range f {
+			switch sub := sub.(type) {
+			case lit:
+				lits = append(lits, vars.litValue(sub))
+			case and:
+				d := vars.dummy()
+				lits = append(lits, d)
+				for _, sub2 := range sub {
+					cnf := cnfRec(sub2, vars)
+					cnf[0] = append(cnf[0], -d)
+					res = append(res, cnf...)
+				}
+			default:
+				panic("unexpected or in or")
+			}
+		}
+		res = append(res, lits)
+		return res
+	case trueConst: // True clauses are ignored
+		return [][]int{}
+	case falseConst: // TODO: improve this. This should simply be declared to make the problem UNSAT.
+		return [][]int{{}}
+	default:
+		panic("invalid NNF formula")
+	}
+}

vendor/github.com/crillab/gophersat/bf/doc.go

@@ -0,0 +1,49 @@
+// Package bf offers facilities to test the satisfiability of generic boolean formula.
+//
+// SAT solvers usually expect as an input CNF formulas.
+// A CNF, or Conjunctive Normal Form, is a set of clauses that must all be true, each clause
+// being a set of potentially negated literals. For the clause to be true, at least one of
+// these literals must be true.
+//
+// However, manually translating a given boolean formula to an equivalent CNF is tedious and error-prone.
+// This package provides a set of logical connectors to define and solve generic logical formulas.
+// Those formulas are then automatically translated to CNF and passed to the gophersat solver.
+//
+// For example, the following boolean formula:
+//
+//     ¬(a ∧ b) → ((c ∨ ¬d) ∧ ¬(c ∧ (e ↔ ¬c)) ∧ ¬(a ⊻ b))
+//
+// Will be defined with the following code:
+//
+//     f := Not(Implies(And(Var("a"), Var("b")), And(Or(Var("c"), Not(Var("d"))), Not(And(Var("c"), Eq(Var("e"), Not(Var("c"))))), Not(Xor(Var("a"), Var("b"))))))
+//
+// When calling `Solve(f)`, the following equivalent CNF will be generated:
+//
+//     a ∧ b ∧ (¬c ∨ ¬x1) ∧ (d ∨ ¬x1) ∧ (c ∨ ¬x2) ∧ (¬e ∨ ¬c ∨ ¬x2) ∧ (e ∨ c ∨ ¬x2) ∧ (¬a ∨ ¬b ∨ ¬x3) ∧ (a ∨ b ∨ ¬x3) ∧ (x1 ∨ x2 ∨ x3)
+//
+// Note that this formula is longer than the original one and that some variables were added to it.
+// The translation is both polynomial in time and space.
+// When fed this CNF as an input, gophersat then returns the following map:
+//
+//     map[a:true b:true c:false d:true e:false]
+//
+// It is also possible to create boolean formulas using a dedicated syntax. The BNF grammar is as follows:
+//
+//    formula ::= clause { ';' clause }*
+//    clause  ::= implies { '=' implies }*
+//    implies ::= or { '->' or}*
+//    or      ::= and { '|' and}*
+//    and     ::= not { '&' not}*
+//    not     ::= '^'not | atom
+//    atom    ::= ident | '(' formula ')'
+//
+// So the formula
+//
+//     ¬(a ∧ b) → ((c ∨ ¬d) ∧ ¬(c ∧ (e ↔ ¬c)) ∧ ¬(a ⊻ b))
+//
+// would be written as
+//
+//    ^(a & b) -> ((c | ^d) & ^(c & (e = ^c)) & ^(a = ^b))
+//
+// a call to the `Parse` function will then create the associated Formula.
+package bf

vendor/github.com/crillab/gophersat/bf/parser.go

@@ -0,0 +1,254 @@
+package bf
+
+import (
+	"fmt"
+	"go/token"
+	"io"
+	"text/scanner"
+)
+
+type parser struct {
+	s     scanner.Scanner
+	eof   bool   // Have we reached eof yet?
+	token string // Last token read
+}
+
+// Parse parses the formula from the given input Reader.
+// It returns the corresponding Formula.
+// Formulas are written using the following operators (from lowest to highest priority) :
+//
+// - for a conjunction of clauses ("and"), the ";" operator
+//
+// - for an equivalence, the "=" operator,
+//
+// - for an implication, the "->" operator,
+//
+// - for a disjunction ("or"), the "|" operator,
+//
+// - for a conjunction ("and"), the "&" operator,
+//
+// - for a negation, the "^" unary operator.
+//
+// - for an exactly-one constraint, names of variables between curly braces, eg "{a, b, c}" to specify
+// exactly one of the variable a, b or c must be true.
+//
+// Parentheses can be used to group subformulas.
+// Note there are two ways to write conjunctions, one with a low priority, one with a high priority.
+// The low-priority one is useful when the user wants to describe a whole formula as a set of smaller formulas
+// that must all be true.
+func Parse(r io.Reader) (Formula, error) {
+	var s scanner.Scanner
+	s.Init(r)
+	p := parser{s: s}
+	p.scan()
+	f, err := p.parseClause()
+	if err != nil {
+		return f, err
+	}
+	if !p.eof {
+		return nil, fmt.Errorf("expected EOF, found %q at %v", p.token, p.s.Pos())
+	}
+	return f, nil
+}
+
+func isOperator(token string) bool {
+	return token == "=" || token == "->" || token == "|" || token == "&" || token == ";"
+}
+
+func (p *parser) scan() {
+	p.eof = p.eof || (p.s.Scan() == scanner.EOF)
+	p.token = p.s.TokenText()
+}
+
+func (p *parser) parseClause() (f Formula, err error) {
+	if isOperator(p.token) {
+		return nil, fmt.Errorf("unexpected token %q at %s", p.token, p.s.Pos())
+	}
+	f, err = p.parseEquiv()
+	if err != nil {
+		return nil, err
+	}
+	if p.eof {
+		return f, nil
+	}
+	if p.token == ";" {
+		p.scan()
+		if p.eof {
+			return f, nil
+		}
+		f2, err := p.parseClause()
+		if err != nil {
+			return nil, err
+		}
+		return And(f, f2), nil
+	}
+	return f, nil
+}
+
+func (p *parser) parseEquiv() (f Formula, err error) {
+	if p.eof {
+		return nil, fmt.Errorf("At position %v, expected expression, found EOF", p.s.Pos())
+	}
+	if isOperator(p.token) {
+		return nil, fmt.Errorf("unexpected token %q at %s", p.token, p.s.Pos())
+	}
+	f, err = p.parseImplies()
+	if err != nil {
+		return nil, err
+	}
+	if p.eof {
+		return f, nil
+	}
+	if p.token == "=" {
+		p.scan()
+		if p.eof {
+			return nil, fmt.Errorf("unexpected EOF")
+		}
+		f2, err := p.parseEquiv()
+		if err != nil {
+			return nil, err
+		}
+		return Eq(f, f2), nil
+	}
+	return f, nil
+}
+
+func (p *parser) parseImplies() (f Formula, err error) {
+	f, err = p.parseOr()
+	if err != nil {
+		return nil, err
+	}
+	if p.eof {
+		return f, nil
+	}
+	if p.token == "-" {
+		p.scan()
+		if p.eof {
+			return nil, fmt.Errorf("unexpected EOF")
+		}
+		if p.token != ">" {
+			return nil, fmt.Errorf("invalid token %q at %v", "-"+p.token, p.s.Pos())
+		}
+		p.scan()
+		if p.eof {
+			return nil, fmt.Errorf("unexpected EOF")
+		}
+		f2, err := p.parseImplies()
+		if err != nil {
+			return nil, err
+		}
+		return Implies(f, f2), nil
+	}
+	return f, nil
+}
+
+func (p *parser) parseOr() (f Formula, err error) {
+	f, err = p.parseAnd()
+	if err != nil {
+		return nil, err
+	}
+	if p.eof {
+		return f, nil
+	}
+	if p.token == "|" {
+		p.scan()
+		if p.eof {
+			return nil, fmt.Errorf("unexpected EOF")
+		}
+		f2, err := p.parseOr()
+		if err != nil {
+			return nil, err
+		}
+		return Or(f, f2), nil
+	}
+	return f, nil
+}
+
+func (p *parser) parseAnd() (f Formula, err error) {
+	f, err = p.parseNot()
+	if err != nil {
+		return nil, err
+	}
+	if p.eof {
+		return f, nil
+	}
+	if p.token == "&" {
+		p.scan()
+		if p.eof {
+			return nil, fmt.Errorf("unexpected EOF")
+		}
+		f2, err := p.parseAnd()
+		if err != nil {
+			return nil, err
+		}
+		return And(f, f2), nil
+	}
+	return f, nil
+}
+
+func (p *parser) parseNot() (f Formula, err error) {
+	if isOperator(p.token) {
+		return nil, fmt.Errorf("unexpected token %q at %s", p.token, p.s.Pos())
+	}
+	if p.token == "^" {
+		p.scan()
+		if p.eof {
+			return nil, fmt.Errorf("unexpected EOF")
+		}
+		f, err = p.parseNot()
+		if err != nil {
+			return nil, err
+		}
+		return Not(f), nil
+	}
+	f, err = p.parseBasic()
+	if err != nil {
+		return nil, err
+	}
+	return f, nil
+}
+
+func (p *parser) parseBasic() (f Formula, err error) {
+	if isOperator(p.token) || p.token == ")" {
+		return nil, fmt.Errorf("unexpected token %q at %s", p.token, p.s.Pos())
+	}
+	if p.token == "(" {
+		p.scan()
+		f, err = p.parseEquiv()
+		if err != nil {
+			return nil, err
+		}
+		if p.eof {
+			return nil, fmt.Errorf("expected closing parenthesis, found EOF at %s", p.s.Pos())
+		}
+		if p.token != ")" {
+			return nil, fmt.Errorf("expected closing parenthesis, found %q at %s", p.token, p.s.Pos())
+		}
+		p.scan()
+		return f, nil
+	}
+	if p.token == "{" {
+		var vars []string
+		for p.token != "}" {
+			p.scan()
+			if p.eof {
+				return nil, fmt.Errorf("expected identifier, found EOF at %s", p.s.Pos())
+			}
+			if token.Lookup(p.token) != token.IDENT {
+				return nil, fmt.Errorf("expected variable name, found %q at %s", p.token, p.s.Pos())
+			}
+			vars = append(vars, p.token)
+			p.scan()
+			if p.eof {
+				return nil, fmt.Errorf("expected comma or closing brace, found EOF at %s", p.s.Pos())
+			}
+			if p.token != "}" && p.token != "," {
+				return nil, fmt.Errorf("expected comma or closing brace, found %q at %v", p.token, p.s.Pos())
+			}
+		}
+		p.scan()
+		return Unique(vars...), nil
+	}
+	defer p.scan()
+	return Var(p.token), nil
+}

vendor/github.com/crillab/gophersat/solver/card.go

@@ -0,0 +1,27 @@
+package solver
+
+// A CardConstr is a cardinality constraint, i.e a set of literals (represented with integer variables) associated with a minimal number of literals that must be true.
+// A propositional clause (i.e a disjunction of literals) is a cardinality constraint with a minimal cardinality of 1.
+type CardConstr struct {
+	Lits    []int
+	AtLeast int
+}
+
+// AtLeast1 returns a cardinality constraint stating that at least one of the given lits must be true.
+// This is the equivalent of a propositional clause.
+func AtLeast1(lits ...int) CardConstr {
+	return CardConstr{Lits: lits, AtLeast: 1}
+}
+
+// AtMost1 returns a cardinality constraint stating that at most one of the given lits can be true.
+func AtMost1(lits ...int) CardConstr {
+	for i, lit := range lits {
+		lits[i] = -lit
+	}
+	return CardConstr{Lits: lits, AtLeast: len(lits) - 1}
+}
+
+// Exactly1 returns two cardinality constraints stating that exactly one of the given lits must be true.
+func Exactly1(lits ...int) []CardConstr {
+	return []CardConstr{AtLeast1(lits...), AtMost1(lits...)}
+}

vendor/github.com/crillab/gophersat/solver/clause.go

@@ -0,0 +1,243 @@
+package solver
+
+import (
+	"fmt"
+	"sort"
+	"strings"
+)
+
+// data used in PB constraints.
+type pbData struct {
+	weights []int  // weight of each literal. If nil, weights are all 1.
+	watched []bool // indices of watched literals.
+}
+
+// A Clause is a list of Lit, associated with possible data (for learned clauses).
+type Clause struct {
+	lits []Lit
+	// lbdValue's bits are as follow:
+	// leftmost bit: learned flag.
+	// second bit: locked flag (if learned).
+	// last 30 bits: LBD value (if learned) or minimal cardinality - 1 (if !learned).
+	// NOTE: actual cardinality is value + 1, since this is the default value and go defaults to 0.
+	lbdValue uint32
+	activity float32
+	pbData   *pbData
+}
+
+const (
+	learnedMask uint32 = 1 << 31
+	lockedMask  uint32 = 1 << 30
+	bothMasks   uint32 = learnedMask | lockedMask
+)
+
+// NewClause returns a clause whose lits are given as an argument.
+func NewClause(lits []Lit) *Clause {
+	return &Clause{lits: lits}
+}
+
+// NewCardClause returns a clause whose lits are given as an argument and
+// for which at least 'card' literals must be true.
+// Note tha NewClause(lits) is equivalent to NewCardClause(lits, 1).
+func NewCardClause(lits []Lit, card int) *Clause {
+	if card < 1 || card > len(lits) {
+		panic("Invalid cardinality value")
+	}
+	return &Clause{lits: lits, lbdValue: uint32(card - 1)}
+}
+
+// Used to sort literals when constructing PB clause.
+type weightedLits struct {
+	lits    []Lit
+	weights []int
+}
+
+func (wl weightedLits) Less(i, j int) bool { return wl.weights != nil && wl.weights[i] > wl.weights[j] }
+func (wl weightedLits) Len() int           { return len(wl.lits) }
+func (wl *weightedLits) Swap(i, j int) {
+	wl.lits[i], wl.lits[j] = wl.lits[j], wl.lits[i]
+	if wl.weights != nil {
+		wl.weights[i], wl.weights[j] = wl.weights[j], wl.weights[i]
+	}
+}
+
+// NewPBClause returns a pseudo-boolean clause with the given lits, weights and minimal cardinality.
+func NewPBClause(lits []Lit, weights []int, card int) *Clause {
+	if card < 1 {
+		panic("Invalid cardinality value")
+	}
+	wl := &weightedLits{lits: lits, weights: weights}
+	sort.Sort(wl)
+	pbData := pbData{weights: weights, watched: make([]bool, len(lits))}
+	if pbData.weights == nil {
+		pbData.weights = make([]int, len(lits))
+		for i := range pbData.weights {
+			pbData.weights[i] = 1
+		}
+	}
+	return &Clause{lits: lits, lbdValue: uint32(card - 1), pbData: &pbData}
+}
+
+// NewLearnedClause returns a new clause marked as learned.
+func NewLearnedClause(lits []Lit) *Clause {
+	return &Clause{lits: lits, lbdValue: learnedMask}
+}
+
+// Cardinality returns the minimum number of literals that must be true to satisfy the clause.
+func (c *Clause) Cardinality() int {
+	if c.Learned() {
+		return 1
+	}
+	return int(c.lbdValue & ^bothMasks) + 1
+}
+
+// Learned returns true iff c was a learned clause.
+func (c *Clause) Learned() bool {
+	return c.lbdValue&learnedMask == learnedMask
+}
+
+// PseudoBoolean returns true iff c is a pseudo boolean constraint, and not
+// just a propositional clause or cardinality constraint.
+func (c *Clause) PseudoBoolean() bool {
+	return c.pbData != nil
+}
+
+func (c *Clause) lock() {
+	c.lbdValue = c.lbdValue | lockedMask
+}
+
+func (c *Clause) unlock() {
+	c.lbdValue = c.lbdValue & ^lockedMask
+}
+
+func (c *Clause) lbd() int {
+	return int(c.lbdValue & ^bothMasks)
+}
+
+func (c *Clause) setLbd(lbd int) {
+	c.lbdValue = (c.lbdValue & bothMasks) | uint32(lbd)
+}
+
+func (c *Clause) incLbd() {
+	c.lbdValue++
+}
+
+func (c *Clause) isLocked() bool {
+	return c.lbdValue&bothMasks == bothMasks
+}
+
+// Len returns the nb of lits in the clause.
+func (c *Clause) Len() int {
+	return len(c.lits)
+}
+
+// First returns the first lit from the clause.
+func (c *Clause) First() Lit {
+	return c.lits[0]
+}
+
+// Second returns the second lit from the clause.
+func (c *Clause) Second() Lit {
+	return c.lits[1]
+}
+
+// Get returns the ith literal from the clause.
+func (c *Clause) Get(i int) Lit {
+	return c.lits[i]
+}
+
+// Set sets the ith literal of the clause.
+func (c *Clause) Set(i int, l Lit) {
+	c.lits[i] = l
+}
+
+// Weight returns the weight of the ith literal.
+// In a propositional clause or a cardinality constraint, that value will always be 1.
+func (c *Clause) Weight(i int) int {
+	if c.pbData == nil {
+		return 1
+	}
+	return c.pbData.weights[i]
+}
+
+// WeightSum returns the sum of the PB weights.
+// If c is a propositional clause, the function will return the length of the clause.
+func (c *Clause) WeightSum() int {
+	if c.pbData == nil {
+		return len(c.lits)
+	}
+	res := 0
+	for _, w := range c.pbData.weights {
+		res += w
+	}
+	return res
+}
+
+// swap swaps the ith and jth lits from the clause.
+func (c *Clause) swap(i, j int) {
+	c.lits[i], c.lits[j] = c.lits[j], c.lits[i]
+	if c.pbData != nil {
+		c.pbData.weights[i], c.pbData.weights[j] = c.pbData.weights[j], c.pbData.weights[i]
+	}
+}
+
+// updateCardinality adds "add" to c's cardinality.
+// Must not be called on learned clauses!
+func (c *Clause) updateCardinality(add int) {
+	if add < 0 && uint32(-add) > c.lbdValue {
+		c.lbdValue = 0
+	} else {
+		c.lbdValue += uint32(add)
+	}
+}
+
+// removeLit remove the idx'th lit from c.
+// The order of literals might be updated, so this function
+// should not be called once the whole solver was created,
+// only during simplification of the problem.
+func (c *Clause) removeLit(idx int) {
+	c.lits[idx] = c.lits[len(c.lits)-1]
+	c.lits = c.lits[:len(c.lits)-1]
+	if c.pbData != nil {
+		c.pbData.weights[idx] = c.pbData.weights[len(c.pbData.weights)-1]
+		c.pbData.weights = c.pbData.weights[:len(c.pbData.weights)-1]
+	}
+}
+
+// Shrink reduces the length of the clauses, by removing all lits
+// starting from position newLen.
+func (c *Clause) Shrink(newLen int) {
+	c.lits = c.lits[:newLen]
+	if c.pbData != nil {
+		c.pbData.weights = c.pbData.weights[:newLen]
+		c.pbData.watched = c.pbData.watched[:newLen]
+	}
+}
+
+// CNF returns a DIMACS CNF representation of the clause.
+func (c *Clause) CNF() string {
+	res := ""
+	for _, lit := range c.lits {
+		res += fmt.Sprintf("%d ", lit.Int())
+	}
+	return fmt.Sprintf("%s0", res)
+}
+
+// PBString returns a string representation of c as a pseudo-boolean expression.
+func (c *Clause) PBString() string {
+	terms := make([]string, c.Len())
+	for i, lit := range c.lits {
+		weight := 1
+		if c.pbData != nil {
+			weight = c.pbData.weights[i]
+		}
+		val := lit.Int()
+		sign := ""
+		if val < 0 {
+			val = -val
+			sign = "~"
+		}
+		terms[i] = fmt.Sprintf("%d %sx%d", weight, sign, val)
+	}
+	return fmt.Sprintf("%s >= %d ;", strings.Join(terms, " +"), c.Cardinality())
+}

vendor/github.com/crillab/gophersat/solver/clause_alloc.go

@@ -0,0 +1,29 @@
+package solver
+
+// This file deals with an attempt for an efficient clause allocator/deallocator, to relax GC's work.
+
+const (
+	nbLitsAlloc = 5000000 // How many literals are initialized at first?
+)
+
+type allocator struct {
+	lits    []Lit // A list of lits, that will be sliced to make []Lit
+	ptrFree int   // Index of the first free item in lits
+}
+
+var alloc allocator
+
+// newLits returns a slice of lits containing the given literals.
+// It is taken from the preinitialized pool if possible,
+// or is created from scratch.
+func (a *allocator) newLits(lits ...Lit) []Lit {
+	if a.ptrFree+len(lits) > len(a.lits) {
+		a.lits = make([]Lit, nbLitsAlloc)
+		copy(a.lits, lits)
+		a.ptrFree = len(lits)
+		return a.lits[:len(lits)]
+	}
+	copy(a.lits[a.ptrFree:], lits)
+	a.ptrFree += len(lits)
+	return a.lits[a.ptrFree-len(lits) : a.ptrFree]
+}

vendor/github.com/crillab/gophersat/solver/doc.go

@@ -0,0 +1,102 @@
+/*
+Package solver gives access to a simple SAT and pseudo-boolean solver.
+Its input can be either a DIMACS CNF file, a PBS file or a solver.Problem object,
+containing the set of clauses to be solved. In the last case,
+the problem can be either a set of propositional clauses,
+or a set of pseudo-boolean constraints.
+
+No matter the input format,
+the solver.Solver will then solve the problem and indicate whether the problem is
+satisfiable or not. In the former case, it will be able to provide a model, i.e a set of bindings
+for all variables that makes the problem true.
+
+Describing a problem
+
+A problem can be described in several ways:
+
+1. parse a DIMACS stream (io.Reader). If the io.Reader produces the following content:
+
+    p cnf 6 7
+    1 2 3 0
+    4 5 6 0
+    -1 -4 0
+    -2 -5 0
+    -3 -6 0
+    -1 -3 0
+    -4 -6 0
+
+the programmer can create the Problem by doing:
+
+    pb, err := solver.ParseCNF(f)
+
+2. create the equivalent list of list of literals. The problem above can be created programatically this way:
+
+    clauses := [][]int{
+        []int{1, 2, 3},
+        []int{4, 5, 6},
+        []int{-1, -4},
+        []int{-2, -5},
+        []int{-3, -6},
+        []int{-1, -3},
+        []int{-4, -6},
+    }
+    pb := solver.ParseSlice(clauses)
+
+3. create a list of cardinality constraints (CardConstr), if the problem to be solved is better represented this way.
+For instance, the problem stating that at least two literals must be true among the literals 1, 2, 3 and 4 could be described as a set of clauses:
+
+    clauses := [][]int{
+        []int{1, 2, 3},
+        []int{2, 3, 4},
+        []int{1, 2, 4},
+        []int{1, 3, 4},
+    }
+    pb := solver.ParseSlice(clauses)
+
+The number of clauses necessary to describe such a constrain can grow exponentially. Alternatively, it is possible to describe the same this way:
+
+    constrs := []CardConstr{
+        {Lits: []int{1, 2, 3, 4}, AtLeast: 2},
+    }
+    pb := solver.ParseCardConstrs(clauses)
+
+Note that a propositional clause has an implicit cardinality constraint of 1, since at least one of its literals must be true.
+
+4. parse a PBS stream (io.Reader). If the io.Reader contains the following problem:
+
+    2 ~x1 +1 x2 +1 x3 >= 3 ;
+
+the programmer can create the Problem by doing:
+
+    pb, err := solver.ParsePBS(f)
+
+5. create a list of PBConstr. For instance, the following set of one PBConstrs will generate the same problem as above:
+
+    constrs := []PBConstr{GtEq([]int{1, 2, 3}, []int{2, 1, 1}, 3)}
+    pb := solver.ParsePBConstrs(constrs)
+
+Solving a problem
+
+To solve a problem, one simply creates a solver with said problem.
+The solve() method then solves the problem and returns the corresponding status: Sat or Unsat.
+
+    s := solver.New(pb)
+    status := s.Solve()
+
+If the status was Sat, the programmer can ask for a model, i.e an assignment that makes all the clauses of the problem true:
+
+    m := s.Model()
+
+For the above problem, the status will be Sat and the model can be {false, true, false, true, false, false}.
+
+Alternatively, one can display on stdout the result and model (if any):
+
+    s.OutputModel()
+
+For the above problem described in the DIMACS format, the output can be:
+
+    SATISFIABLE
+    -1 2 -3 4 -5 -6
+
+*/
+package solver

vendor/github.com/crillab/gophersat/solver/interface.go

@@ -0,0 +1,35 @@
+package solver
+
+// A Result is a status, either Sat, Unsat or Indet.
+// If the status is Sat, the Result also associates a ModelMap with an integer value.
+// This value is typically used in optimization processes.
+// If the weight is 0, that means all constraints could be solved.
+// By definition, in decision problems, the cost will always be 0.
+type Result struct {
+	Status Status
+	Model  []bool
+	Weight int
+}
+
+// Interface is any type implementing a solver.
+// The basic Solver defined in this package implements it.
+// Any solver that uses the basic solver to solve more complex problems
+// (MAXSAT, MUS extraction, etc.) can implement it, too.
+type Interface interface {
+	// Optimal solves or optimizes the problem and returns the best result.
+	// If the results chan is non nil, it will write the associated model each time one is found.
+	// It will stop as soon as a model of cost 0 is found, or the problem is not satisfiable anymore.
+	// The last satisfying model, if any, will be returned with the Sat status.
+	// If no model at all could be found, the Unsat status will be returned.
+	// If the solver prematurely stopped, the Indet status will be returned.
+	// If data is sent to stop, the method may stop prematurely.
+	// In any case, results will be closed before the function returns.
+	// NOTE: data sent on stop may be ignored by an implementation.
+	Optimal(results chan Result, stop chan struct{}) Result
+	// Enumerate returns the number of models for the problem.
+	// If the models chan is non nil, it will write the associated model each time one is found.
+	// If data is sent to stop, the method may stop prematurely.
+	// In any case, models will be closed before the function returns.
+	// NOTE: data sent on stop may be ignored by an implementation.
+	Enumerate(models chan []bool, stop chan struct{}) int
+}

vendor/github.com/crillab/gophersat/solver/lbd.go

@@ -0,0 +1,89 @@
+package solver
+
+const (
+	nbMaxRecent      = 50 // How many recent LBD values we consider; "X" in papers about LBD.
+	triggerRestartK  = 0.8
+	nbMaxTrail       = 5000 // How many elements in queueTrail we consider; "Y" in papers about LBD.
+	postponeRestartT = 1.4
+)
+
+type queueData struct {
+	totalNb   int     // Current total nb of values considered
+	totalSum  int     // Sum of all values so far
+	nbRecent  int     // NB of values used in the array
+	ptr       int     // current index of oldest value in the array
+	recentAvg float64 // Average value
+}
+
+// lbdStats is a structure dealing with recent LBD evolutions.
+type lbdStats struct {
+	lbdData      queueData
+	trailData    queueData
+	recentVals   [nbMaxRecent]int // Last LBD values
+	recentTrails [nbMaxTrail]int  // Last trail lengths
+}
+
+// mustRestart is true iff recent LBDs are much smaller on average than average of all LBDs.
+func (l *lbdStats) mustRestart() bool {
+	if l.lbdData.nbRecent < nbMaxRecent {
+		return false
+	}
+	return l.lbdData.recentAvg*triggerRestartK > float64(l.lbdData.totalSum)/float64(l.lbdData.totalNb)
+}
+
+// addConflict adds information about a conflict that just happened.
+func (l *lbdStats) addConflict(trailSz int) {
+	td := &l.trailData
+	td.totalNb++
+	td.totalSum += trailSz
+	if td.nbRecent < nbMaxTrail {
+		l.recentTrails[td.nbRecent] = trailSz
+		old := float64(td.nbRecent)
+		new := old + 1
+		td.recentAvg = (td.recentAvg*old)/new + float64(trailSz)/new
+		td.nbRecent++
+	} else {
+		old := l.recentTrails[td.ptr]
+		l.recentTrails[td.ptr] = trailSz
+		td.ptr++
+		if td.ptr == nbMaxTrail {
+			td.ptr = 0
+		}
+		td.recentAvg = td.recentAvg - float64(old)/nbMaxTrail + float64(trailSz)/nbMaxTrail
+	}
+	if td.nbRecent == nbMaxTrail && l.lbdData.nbRecent == nbMaxRecent && trailSz > int(postponeRestartT*td.recentAvg) {
+		// Too many good assignments: postpone restart
+		l.clear()
+	}
+
+}
+
+// addLbd adds information about a recent learned clause's LBD.
+// TODO: this is very close to addConflicts's code, this should probably be rewritten/merged.
+func (l *lbdStats) addLbd(lbd int) {
+	ld := &l.lbdData
+	ld.totalNb++
+	ld.totalSum += lbd
+	if ld.nbRecent < nbMaxRecent {
+		l.recentVals[ld.nbRecent] = lbd
+		old := float64(ld.nbRecent)
+		new := old + 1
+		ld.recentAvg = (ld.recentAvg*old)/new + float64(lbd)/new
+		ld.nbRecent++
+	} else {
+		old := l.recentVals[ld.ptr]
+		l.recentVals[ld.ptr] = lbd
+		ld.ptr++
+		if ld.ptr == nbMaxRecent {
+			ld.ptr = 0
+		}
+		ld.recentAvg = ld.recentAvg - float64(old)/nbMaxRecent + float64(lbd)/nbMaxRecent
+	}
+}
+
+// clear clears last values. It should be called after a restart.
+func (l *lbdStats) clear() {
+	l.lbdData.ptr = 0
+	l.lbdData.nbRecent = 0
+	l.lbdData.recentAvg = 0.0
+}

vendor/github.com/crillab/gophersat/solver/learn.go

@@ -0,0 +1,121 @@
+package solver
+
+// computeLbd computes and sets c's LBD (Literal Block Distance).
+func (c *Clause) computeLbd(model Model) {
+	c.setLbd(1)
+	curLvl := abs(model[c.Get(0).Var()])
+	for i := 0; i < c.Len(); i++ {
+		lit := c.Get(i)
+		if lvl := abs(model[lit.Var()]); lvl != curLvl {
+			curLvl = lvl
+			c.incLbd()
+		}
+	}
+}
+
+// addClauseLits is a helper function for learnClause.
+// It deals with lits from the conflict clause.
+func (s *Solver) addClauseLits(confl *Clause, lvl decLevel, met, metLvl []bool, lits *[]Lit) int {
+	nbLvl := 0
+	for i := 0; i < confl.Len(); i++ {
+		l := confl.Get(i)
+		v := l.Var()
+		if s.litStatus(l) != Unsat {
+			// In clauses where cardinality > 1, some lits might be true in the conflict clause: ignore them
+			continue
+		}
+		met[v] = true
+		s.varBumpActivity(v)
+		if abs(s.model[v]) == lvl {
+			metLvl[v] = true
+			nbLvl++
+		} else if abs(s.model[v]) != 1 {
+			*lits = append(*lits, l)
+		}
+	}
+	return nbLvl
+}
+
+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.
+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
+	buf := make([]bool, s.nbVars*2) // Buffer for met and metLvl; reduces allocs/deallocs
+	met := buf[:s.nbVars]           // List of all vars already met
+	metLvl := buf[s.nbVars:]        // List of all vars from current level to deal with
+	// nbLvl is the nb of vars in lvl currently used
+	nbLvl := s.addClauseLits(confl, lvl, met, metLvl, &lits)
+	ptr := len(s.trail) - 1 // Pointer in propagation trail
+	for nbLvl > 1 {         // We will stop once we only have one lit from current level.
+		for !metLvl[s.trail[ptr].Var()] {
+			if abs(s.model[s.trail[ptr].Var()]) == lvl { // This var was deduced afterwards and was not a reason for the conflict
+				met[s.trail[ptr].Var()] = true
+			}
+			ptr--
+		}
+		v := s.trail[ptr].Var()
+		ptr--
+		nbLvl--
+		if reason := s.reason[v]; reason != nil {
+			s.clauseBumpActivity(reason)
+			for i := 0; i < reason.Len(); i++ {
+				lit := reason.Get(i)
+				if v2 := lit.Var(); !met[v2] {
+					if s.litStatus(lit) != Unsat {
+						continue
+					}
+					met[v2] = true
+					s.varBumpActivity(v2)
+					if abs(s.model[v2]) == lvl {
+						metLvl[v2] = true
+						nbLvl++
+					} else if abs(s.model[v2]) != 1 {
+						lits = append(lits, lit)
+					}
+				}
+			}
+		}
+	}
+	for _, l := range s.trail { // Look for last lit from lvl and use it as asserting lit
+		if metLvl[l.Var()] {
+			lits[0] = l.Negation()
+			break
+		}
+	}
+	s.varDecayActivity()
+	s.clauseDecayActivity()
+	sortLiterals(lits, s.model)
+	sz := s.minimizeLearned(met, lits)
+	if sz == 1 {
+		return nil, lits[0]
+	}
+	learned = NewLearnedClause(alloc.newLits(lits[0:sz]...))
+	learned.computeLbd(s.model)
+	return learned, -1
+}
+
+// minimizeLearned reduces (if possible) the length of the learned clause and returns the size
+// of the new list of lits.
+func (s *Solver) minimizeLearned(met []bool, learned []Lit) int {
+	sz := 1
+	for i := 1; i < len(learned); i++ {
+		if reason := s.reason[learned[i].Var()]; reason == nil {
+			learned[sz] = learned[i]
+			sz++
+		} else {
+			for k := 0; k < reason.Len(); k++ {
+				lit := reason.Get(k)
+				if !met[lit.Var()] && abs(s.model[lit.Var()]) > 1 {
+					learned[sz] = learned[i]
+					sz++
+					break
+				}
+			}
+		}
+	}
+	return sz
+}

vendor/github.com/crillab/gophersat/solver/parser.go

@@ -0,0 +1,171 @@
+package solver
+
+import (
+	"bufio"
+	"fmt"
+	"io"
+	"strconv"
+	"strings"
+)
+
+// ParseSlice parse a slice of slice of lits and returns the equivalent problem.
+// The argument is supposed to be a well-formed CNF.
+func ParseSlice(cnf [][]int) *Problem {
+	var pb Problem
+	for _, line := range cnf {
+		switch len(line) {
+		case 0:
+			pb.Status = Unsat
+			return &pb
+		case 1:
+			if line[0] == 0 {
+				panic("null unit clause")
+			}
+			lit := IntToLit(int32(line[0]))
+			v := lit.Var()
+			if int(v) >= pb.NbVars {
+				pb.NbVars = int(v) + 1
+			}
+			pb.Units = append(pb.Units, lit)
+		default:
+			lits := make([]Lit, len(line))
+			for j, val := range line {
+				if val == 0 {
+					panic("null literal in clause %q")
+				}
+				lits[j] = IntToLit(int32(val))
+				if v := int(lits[j].Var()); v >= pb.NbVars {
+					pb.NbVars = v + 1
+				}
+			}
+			pb.Clauses = append(pb.Clauses, NewClause(lits))
+		}
+	}
+	pb.Model = make([]decLevel, pb.NbVars)
+	for _, unit := range pb.Units {
+		v := unit.Var()
+		if pb.Model[v] == 0 {
+			if unit.IsPositive() {
+				pb.Model[v] = 1
+			} else {
+				pb.Model[v] = -1
+			}
+		} else if pb.Model[v] > 0 != unit.IsPositive() {
+			pb.Status = Unsat
+			return &pb
+		}
+	}
+	pb.simplify()
+	return &pb
+}
+
+// readInt reads an int from r.
+// 'b' is the last read byte. It can be a space, a '-' or a digit.
+// The int can be negated.
+// All spaces before the int value are ignored.
+// Can return EOF.
+func readInt(b *byte, r *bufio.Reader) (res int, err error) {
+	for err == nil && (*b == ' ' || *b == '\t' || *b == '\n' || *b == '\r') {
+		*b, err = r.ReadByte()
+	}
+	if err == io.EOF {
+		return res, io.EOF
+	}
+	if err != nil {
+		return res, fmt.Errorf("could not read digit: %v", err)
+	}
+	neg := 1
+	if *b == '-' {
+		neg = -1
+		*b, err = r.ReadByte()
+		if err != nil {
+			return 0, fmt.Errorf("cannot read int: %v", err)
+		}
+	}
+	for err == nil {
+		if *b < '0' || *b > '9' {
+			return 0, fmt.Errorf("cannot read int: %q is not a digit", *b)
+		}
+		res = 10*res + int(*b-'0')
+		*b, err = r.ReadByte()
+		if *b == ' ' || *b == '\t' || *b == '\n' || *b == '\r' {
+			break
+		}
+	}
+	res *= neg
+	return res, err
+}
+
+func parseHeader(r *bufio.Reader) (nbVars, nbClauses int, err error) {
+	line, err := r.ReadString('\n')
+	if err != nil {
+		return 0, 0, fmt.Errorf("cannot read header: %v", err)
+	}
+	fields := strings.Fields(line)
+	if len(fields) < 3 {
+		return 0, 0, fmt.Errorf("invalid syntax %q in header", line)
+	}
+	nbVars, err = strconv.Atoi(fields[1])
+	if err != nil {
+		return 0, 0, fmt.Errorf("nbvars not an int : %q", fields[1])
+	}
+	nbClauses, err = strconv.Atoi(fields[2])
+	if err != nil {
+		return 0, 0, fmt.Errorf("nbClauses not an int : '%s'", fields[2])
+	}
+	return nbVars, nbClauses, nil
+}
+
+// ParseCNF parses a CNF file and returns the corresponding Problem.
+func ParseCNF(f io.Reader) (*Problem, error) {
+	r := bufio.NewReader(f)
+	var (
+		nbClauses int
+		pb        Problem
+	)
+	b, err := r.ReadByte()
+	for err == nil {
+		if b == 'c' { // Ignore comment
+			b, err = r.ReadByte()
+			for err == nil && b != '\n' {
+				b, err = r.ReadByte()
+			}
+		} else if b == 'p' { // Parse header
+			pb.NbVars, nbClauses, err = parseHeader(r)
+			if err != nil {
+				return nil, fmt.Errorf("cannot parse CNF header: %v", err)
+			}
+			pb.Model = make([]decLevel, pb.NbVars)
+			pb.Clauses = make([]*Clause, 0, nbClauses)
+		} else {
+			lits := make([]Lit, 0, 3) // Make room for some lits to improve performance
+			for {
+				val, err := readInt(&b, r)
+				if err == io.EOF {
+					if len(lits) != 0 { // This is not a trailing space at the end...
+						return nil, fmt.Errorf("unfinished clause while EOF found")
+					}
+					break // When there are only several useless spaces at the end of the file, that is ok
+				}
+				if err != nil {
+					return nil, fmt.Errorf("cannot parse clause: %v", err)
+				}
+				if val == 0 {
+					pb.Clauses = append(pb.Clauses, NewClause(lits))
+					break
+				} else {
+					if val > pb.NbVars || -val > pb.NbVars {
+						return nil, fmt.Errorf("invalid literal %d for problem with %d vars only", val, pb.NbVars)
+					}
+					lits = append(lits, IntToLit(int32(val)))
+				}
+			}
+		}
+		b, err = r.ReadByte()
+	}
+	if err != io.EOF {
+		return nil, err
+	}
+	pb.simplify2()
+	return &pb, nil
+}

vendor/github.com/crillab/gophersat/solver/parser_pb.go

@@ -0,0 +1,262 @@
+package solver
+
+import (
+	"bufio"
+	"fmt"
+	"io"
+	"strconv"
+	"strings"
+)
+
+// ParseCardConstrs parses the given cardinality constraints.
+// Will panic if a zero value appears in the literals.
+func ParseCardConstrs(constrs []CardConstr) *Problem {
+	var pb Problem
+	for _, constr := range constrs {
+		card := constr.AtLeast
+		if card <= 0 { // Clause is trivially SAT, ignore
+			continue
+		}
+		if len(constr.Lits) < card { // Clause cannot be satsfied
+			pb.Status = Unsat
+			return &pb
+		}
+		if len(constr.Lits) == card { // All lits must be true
+			for i := range constr.Lits {
+				if constr.Lits[i] == 0 {
+					panic("literal 0 found in clause")
+				}
+				lit := IntToLit(int32(constr.Lits[i]))
+				v := lit.Var()
+				if int(v) >= pb.NbVars {
+					pb.NbVars = int(v) + 1
+				}
+				pb.Units = append(pb.Units, lit)
+			}
+		} else {
+			lits := make([]Lit, len(constr.Lits))
+			for j, val := range constr.Lits {
+				if val == 0 {
+					panic("literal 0 found in clause")
+				}
+				lits[j] = IntToLit(int32(val))
+				if v := int(lits[j].Var()); v >= pb.NbVars {
+					pb.NbVars = v + 1
+				}
+			}
+			pb.Clauses = append(pb.Clauses, NewCardClause(lits, card))
+		}
+	}
+	pb.Model = make([]decLevel, pb.NbVars)
+	for _, unit := range pb.Units {
+		v := unit.Var()
+		if pb.Model[v] == 0 {
+			if unit.IsPositive() {
+				pb.Model[v] = 1
+			} else {
+				pb.Model[v] = -1
+			}
+		} else if pb.Model[v] > 0 != unit.IsPositive() {
+			pb.Status = Unsat
+			return &pb
+		}
+	}
+	pb.simplifyCard()
+	return &pb
+}
+
+// ParsePBConstrs parses and returns a PB problem from PBConstr values.
+func ParsePBConstrs(constrs []PBConstr) *Problem {
+	var pb Problem
+	for _, constr := range constrs {
+		for i := range constr.Lits {
+			lit := IntToLit(int32(constr.Lits[i]))
+			v := lit.Var()
+			if int(v) >= pb.NbVars {
+				pb.NbVars = int(v) + 1
+			}
+		}
+		card := constr.AtLeast
+		if card <= 0 { // Clause is trivially SAT, ignore
+			continue
+		}
+		sumW := constr.WeightSum()
+		if sumW < card { // Clause cannot be satsfied
+			pb.Status = Unsat
+			return &pb
+		}
+		if sumW == card { // All lits must be true
+			for i := range constr.Lits {
+				lit := IntToLit(int32(constr.Lits[i]))
+				found := false
+				for _, u := range pb.Units {
+					if u == lit {
+						found = true
+						break
+					}
+				}
+				if !found {
+					pb.Units = append(pb.Units, lit)
+				}
+			}
+		} else {
+			lits := make([]Lit, len(constr.Lits))
+			for j, val := range constr.Lits {
+				lits[j] = IntToLit(int32(val))
+			}
+			pb.Clauses = append(pb.Clauses, NewPBClause(lits, constr.Weights, card))
+		}
+	}
+	pb.Model = make([]decLevel, pb.NbVars)
+	for _, unit := range pb.Units {
+		v := unit.Var()
+		if pb.Model[v] == 0 {
+			if unit.IsPositive() {
+				pb.Model[v] = 1
+			} else {
+				pb.Model[v] = -1
+			}
+		} else if pb.Model[v] > 0 != unit.IsPositive() {
+			pb.Status = Unsat
+			return &pb
+		}
+	}
+	pb.simplifyPB()
+	return &pb
+}
+
+// parsePBOptim parses the "min:" instruction.
+func (pb *Problem) parsePBOptim(fields []string, line string) error {
+	weights, lits, err := pb.parseTerms(fields[1:], line)
+	if err != nil {
+		return err
+	}
+	pb.minLits = make([]Lit, len(lits))
+	for i, lit := range lits {
+		pb.minLits[i] = IntToLit(int32(lit))
+	}
+	pb.minWeights = weights
+	return nil
+}
+
+func (pb *Problem) parsePBLine(line string) error {
+	if line[len(line)-1] != ';' {
+		return fmt.Errorf("line %q does not end with semicolon", line)
+	}
+	fields := strings.Fields(line[:len(line)-1])
+	if len(fields) == 0 {
+		return fmt.Errorf("empty line in file")
+	}
+	if fields[0] == "min:" { // Optimization constraint
+		return pb.parsePBOptim(fields, line)
+	}
+	return pb.parsePBConstrLine(fields, line)
+}
+
+func (pb *Problem) parsePBConstrLine(fields []string, line string) error {
+	if len(fields) < 3 {
+		return fmt.Errorf("invalid syntax %q", line)
+	}
+	operator := fields[len(fields)-2]
+	if operator != ">=" && operator != "=" {
+		return fmt.Errorf("invalid operator %q in %q: expected \">=\" or \"=\"", operator, line)
+	}
+	rhs, err := strconv.Atoi(fields[len(fields)-1])
+	if err != nil {
+		return fmt.Errorf("invalid value %q in %q: %v", fields[len(fields)-1], line, err)
+	}
+	weights, lits, err := pb.parseTerms(fields[:len(fields)-2], line)
+	if err != nil {
+		return err
+	}
+	var constrs []PBConstr
+	if operator == ">=" {
+		constrs = []PBConstr{GtEq(lits, weights, rhs)}
+	} else {
+		constrs = Eq(lits, weights, rhs)
+	}
+	for _, constr := range constrs {
+		card := constr.AtLeast
+		sumW := constr.WeightSum()
+		if sumW < card { // Clause cannot be satsfied
+			pb.Status = Unsat
+			return nil
+		}
+		if sumW == card { // All lits must be true
+			for i := range constr.Lits {
+				lit := IntToLit(int32(constr.Lits[i]))
+				pb.Units = append(pb.Units, lit)
+			}
+		} else {
+			lits := make([]Lit, len(constr.Lits))
+			for j, val := range constr.Lits {
+				lits[j] = IntToLit(int32(val))
+			}
+			pb.Clauses = append(pb.Clauses, NewPBClause(lits, constr.Weights, card))
+		}
+	}
+	return nil
+}
+
+func (pb *Problem) parseTerms(terms []string, line string) (weights []int, lits []int, err error) {
+	weights = make([]int, 0, len(terms)/2)
+	lits = make([]int, 0, len(terms)/2)
+	i := 0
+	for i < len(terms) {
+		var l string
+		w, err := strconv.Atoi(terms[i])
+		if err != nil {
+			l = terms[i]
+			if !strings.HasPrefix(l, "x") && !strings.HasPrefix(l, "~x") {
+				return nil, nil, fmt.Errorf("invalid weight %q in %q: %v", terms[i*2], line, err)
+			}
+			// This is a weightless lit, i.e a lit with weight 1.
+			weights = append(weights, 1)
+		} else {
+			weights = append(weights, w)
+			i++
+			l = terms[i]
+			if !strings.HasPrefix(l, "x") && !strings.HasPrefix(l, "~x") || len(l) < 2 {
+				return nil, nil, fmt.Errorf("invalid variable name %q in %q", l, line)
+			}
+		}
+		var lit int
+		if l[0] == '~' {
+			lit, err = strconv.Atoi(l[2:])
+			lits = append(lits, -lit)
+		} else {
+			lit, err = strconv.Atoi(l[1:])
+			lits = append(lits, lit)
+		}
+		if err != nil {
+			return nil, nil, fmt.Errorf("invalid variable %q in %q: %v", l, line, err)
+		}
+		if lit > pb.NbVars {
+			pb.NbVars = lit
+		}
+		i++
+	}
+	return weights, lits, nil
+}
+
+// ParseOPB parses a file corresponding to the OPB syntax.
+// See http://www.cril.univ-artois.fr/PB16/format.pdf for more details.
+func ParseOPB(f io.Reader) (*Problem, error) {
+	scanner := bufio.NewScanner(f)
+	var pb Problem
+	for scanner.Scan() {
+		line := scanner.Text()
+		if line == "" || line[0] == '*' {
+			continue
+		}
+		if err := pb.parsePBLine(line); err != nil {
+			return nil, err
+		}
+	}
+	if err := scanner.Err(); err != nil {
+		return nil, fmt.Errorf("could not parse OPB: %v", err)
+	}
+	pb.Model = make([]decLevel, pb.NbVars)
+	pb.simplifyPB()
+	return &pb, nil
+}

vendor/github.com/crillab/gophersat/solver/pb.go

@@ -0,0 +1,101 @@
+package solver
+
+// A PBConstr is a Pseudo-Boolean constraint.
+type PBConstr struct {
+	Lits    []int // List of literals, designed with integer values. A positive value means the literal is true, a negative one it is false.
+	Weights []int // Weight of each lit from Lits. If nil, all lits == 1
+	AtLeast int   // Sum of all lits must be at least this value
+}
+
+// WeightSum returns the sum of the weight of all terms.
+func (c PBConstr) WeightSum() int {
+	if c.Weights == nil { // All weights = 1
+		return len(c.Lits)
+	}
+	res := 0
+	for _, w := range c.Weights {
+		res += w
+	}
+	return res
+}
+
+// Clause returns the clause associated with the given constraint.
+func (c PBConstr) Clause() *Clause {
+	lits := make([]Lit, len(c.Lits))
+	for i, val := range c.Lits {
+		lits[i] = IntToLit(int32(val))
+	}
+	return NewPBClause(lits, c.Weights, c.AtLeast)
+}
+
+// PropClause returns a PB constraint equivalent to a propositional clause: at least one of the given
+// literals must be true.
+// It takes ownership of lits.
+func PropClause(lits ...int) PBConstr {
+	return PBConstr{Lits: lits, AtLeast: 1}
+}
+
+// AtLeast returns a PB constraint stating that at least n literals must be true.
+// It takes ownership of lits.
+func AtLeast(lits []int, n int) PBConstr {
+	return PBConstr{Lits: lits, AtLeast: n}
+}
+
+// AtMost returns a PB constraint stating that at most n literals can be true.
+// It takes ownership of lits.
+func AtMost(lits []int, n int) PBConstr {
+	for i := range lits {
+		lits[i] = -lits[i]
+	}
+	return PBConstr{Lits: lits, AtLeast: len(lits) - n}
+}
+
+// GtEq returns a PB constraint stating that the sum of all literals multiplied by their weight
+// must be at least n.
+// Will panic if len(weights) != len(lits).
+func GtEq(lits []int, weights []int, n int) PBConstr {
+	if len(weights) != 0 && len(lits) != len(weights) {
+		panic("not as many lits as weights")
+	}
+	for i := range weights {
+		if weights[i] < 0 {
+			weights[i] = -weights[i]
+			n += weights[i]
+			lits[i] = -lits[i]
+		}
+	}
+	return PBConstr{Lits: lits, Weights: weights, AtLeast: n}
+}
+
+// LtEq returns a PB constraint stating that the sum of all literals multiplied by their weight
+// must be at most n.
+// Will panic if len(weights) != len(lits).
+func LtEq(lits []int, weights []int, n int) PBConstr {
+	sum := 0
+	for i := range lits {
+		lits[i] = -lits[i]
+		sum += weights[i]
+	}
+	n = sum - n
+	return GtEq(lits, weights, n)
+}
+
+// Eq returns a set of PB constraints stating that the sum of all literals multiplied by their weight
+// must be exactly n.
+// Will panic if len(weights) != len(lits).
+func Eq(lits []int, weights []int, n int) []PBConstr {
+	lits2 := make([]int, len(lits))
+	weights2 := make([]int, len(weights))
+	copy(lits2, lits)
+	copy(weights2, weights)
+	ge := GtEq(lits2, weights2, n)
+	le := LtEq(lits, weights, n)
+	var res []PBConstr
+	if ge.AtLeast > 0 {
+		res = append(res, ge)
+	}
+	if le.AtLeast > 0 {
+		res = append(res, le)
+	}
+	return res
+}

vendor/github.com/crillab/gophersat/solver/preprocess.go

@@ -0,0 +1,183 @@
+package solver
+
+//
+// import "log"
+//
+// // Subsumes returns true iff c subsumes c2.
+// func (c *Clause) Subsumes(c2 *Clause) bool {
+// 	if c.Len() > c2.Len() {
+// 		return false
+// 	}
+// 	for _, lit := range c.lits {
+// 		found := false
+// 		for _, lit2 := range c2.lits {
+// 			if lit == lit2 {
+// 				found = true
+// 				break
+// 			}
+// 			if lit2 > lit {
+// 				return false
+// 			}
+// 		}
+// 		if !found {
+// 			return false
+// 		}
+// 	}
+// 	return true
+// }
+//
+// // SelfSubsumes returns true iff c self-subsumes c2.
+// func (c *Clause) SelfSubsumes(c2 *Clause) bool {
+// 	oneNeg := false
+// 	for _, lit := range c.lits {
+// 		found := false
+// 		for _, lit2 := range c2.lits {
+// 			if lit == lit2 {
+// 				found = true
+// 				break
+// 			}
+// 			if lit == lit2.Negation() {
+// 				if oneNeg { // We want exactly one, but this is the second
+// 					return false
+// 				}
+// 				oneNeg = true
+// 				found = true
+// 				break
+// 			}
+// 			if lit2 > lit { // We won't find it anymore
+// 				return false
+// 			}
+// 		}
+// 		if !found {
+// 			return false
+// 		}
+// 	}
+// 	return oneNeg
+// }
+//
+// // Simplify simplifies the given clause by removing redundant lits.
+// // If the clause is trivially satisfied (i.e contains both a lit and its negation),
+// // true is returned. Otherwise, false is returned.
+// func (c *Clause) Simplify() (isSat bool) {
+// 	c.Sort()
+// 	lits := make([]Lit, 0, len(c.lits))
+// 	i := 0
+// 	for i < len(c.lits) {
+// 		if i < len(c.lits)-1 && c.lits[i] == c.lits[i+1].Negation() {
+// 			return true
+// 		}
+// 		lit := c.lits[i]
+// 		lits = append(lits, lit)
+// 		i++
+// 		for i < len(c.lits) && c.lits[i] == lit {
+// 			i++
+// 		}
+// 	}
+// 	if len(lits) < len(c.lits) {
+// 		c.lits = lits
+// 	}
+// 	return false
+// }
+//
+// // Generate returns a subsumed clause from c and c2, by removing v.
+// func (c *Clause) Generate(c2 *Clause, v Var) *Clause {
+// 	c3 := &Clause{lits: make([]Lit, 0, len(c.lits)+len(c2.lits)-2)}
+// 	for _, lit := range c.lits {
+// 		if lit.Var() != v {
+// 			c3.lits = append(c3.lits, lit)
+// 		}
+// 	}
+// 	for _, lit2 := range c2.lits {
+// 		if lit2.Var() != v {
+// 			c3.lits = append(c3.lits, lit2)
+// 		}
+// 	}
+// 	return c3
+// }
+//
+// func (pb *Problem) preprocess() {
+// 	log.Printf("Preprocessing... %d clauses currently", len(pb.Clauses))
+// 	occurs := make([][]int, pb.NbVars*2)
+// 	for i, c := range pb.Clauses {
+// 		for j := 0; j < c.Len(); j++ {
+// 			occurs[c.Get(j)] = append(occurs[c.Get(j)], i)
+// 		}
+// 	}
+// 	modified := true
+// 	neverModified := true
+// 	for modified {
+// 		modified = false
+// 		for i := 0; i < pb.NbVars; i++ {
+// 			if pb.Model[i] != 0 {
+// 				continue
+// 			}
+// 			v := Var(i)
+// 			lit := v.Lit()
+// 			nbLit := len(occurs[lit])
+// 			nbLit2 := len(occurs[lit.Negation()])
+// 			if (nbLit < 10 || nbLit2 < 10) && (nbLit != 0 || nbLit2 != 0) {
+// 				modified = true
+// 				neverModified = false
+// 				// pb.deleted[v] = true
+// 				log.Printf("%d can be removed: %d and %d", lit.Int(), len(occurs[lit]), len(occurs[lit.Negation()]))
+// 				for _, idx1 := range occurs[lit] {
+// 					for _, idx2 := range occurs[lit.Negation()] {
+// 						c1 := pb.Clauses[idx1]
+// 						c2 := pb.Clauses[idx2]
+// 						newC := c1.Generate(c2, v)
+// 						if !newC.Simplify() {
+// 							switch newC.Len() {
+// 							case 0:
+// 								log.Printf("Inferred UNSAT")
+// 								pb.Status = Unsat
+// 								return
+// 							case 1:
+// 								log.Printf("Unit %d", newC.First().Int())
+// 								lit2 := newC.First()
+// 								if lit2.IsPositive() {
+// 									if pb.Model[lit2.Var()] == -1 {
+// 										pb.Status = Unsat
+// 										return
+// 									}
+// 									pb.Model[lit2.Var()] = 1
+// 								} else {
+// 									if pb.Model[lit2.Var()] == 1 {
+// 										pb.Status = Unsat
+// 										return
+// 									}
+// 									pb.Model[lit2.Var()] = -1
+// 								}
+// 								pb.Units = append(pb.Units, lit2)
+// 							default:
+// 								pb.Clauses = append(pb.Clauses, newC)
+// 							}
+// 						}
+// 					}
+// 				}
+// 				nbRemoved := 0
+// 				for _, idx := range occurs[lit] {
+// 					pb.Clauses[idx] = pb.Clauses[len(pb.Clauses)-nbRemoved-1]
+// 					nbRemoved++
+// 				}
+// 				for _, idx := range occurs[lit.Negation()] {
+// 					pb.Clauses[idx] = pb.Clauses[len(pb.Clauses)-nbRemoved-1]
+// 					nbRemoved++
+// 				}
+// 				pb.Clauses = pb.Clauses[:len(pb.Clauses)-nbRemoved]
+// 				log.Printf("clauses=%s", pb.CNF())
+// 				// Redo occurs
+// 				occurs = make([][]int, pb.NbVars*2)
+// 				for i, c := range pb.Clauses {
+// 					for j := 0; j < c.Len(); j++ {
+// 						occurs[c.Get(j)] = append(occurs[c.Get(j)], i)
+// 					}
+// 				}
+// 				continue
+// 			}
+// 		}
+// 	}
+// 	if !neverModified {
+// 		pb.simplify()
+// 	}
+// 	log.Printf("Done. %d clauses now", len(pb.Clauses))
+// }

vendor/github.com/crillab/gophersat/solver/problem.go

@@ -0,0 +1,347 @@
+package solver
+
+import (
+	"fmt"
+)
+
+// A Problem is a list of clauses & a nb of vars.
+type Problem struct {
+	NbVars     int        // Total nb of vars
+	Clauses    []*Clause  // List of non-empty, non-unit clauses
+	Status     Status     // Status of the problem. Can be trivially UNSAT (if empty clause was met or inferred by UP) or Indet.
+	Units      []Lit      // List of unit literal found in the problem.
+	Model      []decLevel // For each var, its inferred binding. 0 means unbound, 1 means bound to true, -1 means bound to false.
+	minLits    []Lit      // For an optimisation problem, the list of lits whose sum must be minimized
+	minWeights []int      // For an optimisation problem, the weight of each lit.
+}
+
+// Optim returns true iff pb is an optimisation problem, ie
+// a problem for which we not only want to find a model, but also
+// the best possible model according to an optimization constraint.
+func (pb *Problem) Optim() bool {
+	return pb.minLits != nil
+}
+
+// CNF returns a DIMACS CNF representation of the problem.
+func (pb *Problem) CNF() string {
+	res := fmt.Sprintf("p cnf %d %d\n", pb.NbVars, len(pb.Clauses)+len(pb.Units))
+	for _, unit := range pb.Units {
+		res += fmt.Sprintf("%d 0\n", unit.Int())
+	}
+	for _, clause := range pb.Clauses {
+		res += fmt.Sprintf("%s\n", clause.CNF())
+	}
+	return res
+}
+
+// PBString returns a representation of the problem as a pseudo-boolean problem.
+func (pb *Problem) PBString() string {
+	res := pb.costFuncString()
+	for _, unit := range pb.Units {
+		sign := ""
+		if !unit.IsPositive() {
+			sign = "~"
+			unit = unit.Negation()
+		}
+		res += fmt.Sprintf("1 %sx%d = 1 ;\n", sign, unit.Int())
+	}
+	for _, clause := range pb.Clauses {
+		res += fmt.Sprintf("%s\n", clause.PBString())
+	}
+	return res
+}
+
+// SetCostFunc sets the function to minimize when optimizing the problem.
+// If all weights are 1, weights can be nil.
+// In all other cases, len(lits) must be the same as len(weights).
+func (pb *Problem) SetCostFunc(lits []Lit, weights []int) {
+	if weights != nil && len(lits) != len(weights) {
+		panic("length of lits and of weights don't match")
+	}
+	pb.minLits = lits
+	pb.minWeights = weights
+}
+
+// costFuncString returns a string representation of the cost function of the problem, if any, followed by a \n.
+// If there is no cost function, the empty string will be returned.
+func (pb *Problem) costFuncString() string {
+	if pb.minLits == nil {
+		return ""
+	}
+	res := "min: "
+	for i, lit := range pb.minLits {
+		w := 1
+		if pb.minWeights != nil {
+			w = pb.minWeights[i]
+		}
+		sign := ""
+		if w >= 0 && i != 0 { // No plus sign for the first term or for negative terms.
+			sign = "+"
+		}
+		val := lit.Int()
+		neg := ""
+		if val < 0 {
+			val = -val
+			neg = "~"
+		}
+		res += fmt.Sprintf("%s%d %sx%d", sign, w, neg, val)
+	}
+	res += " ;\n"
+	return res
+}
+
+func (pb *Problem) updateStatus(nbClauses int) {
+	pb.Clauses = pb.Clauses[:nbClauses]
+	if pb.Status == Indet && nbClauses == 0 {
+		pb.Status = Sat
+	}
+}
+
+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
+	sat := false
+	for j := 0; j < c.Len(); j++ {
+		lit := c.Get(j)
+		v := lit.Var()
+		if pb.Model[v] == 0 {
+			c.Set(k, c.Get(j))
+			k++
+			idxClauses[lit] = append(idxClauses[lit], idx)
+		} else if (pb.Model[v] > 0) == lit.IsPositive() {
+			sat = true
+			break
+		}
+	}
+	if sat {
+		removed[idx] = true
+		return
+	}
+	if k == 0 {
+		pb.Status = Unsat
+		return
+	}
+	if k == 1 {
+		pb.addUnit(c.First())
+		if pb.Status == Unsat {
+			return
+		}
+		removed[idx] = true
+	}
+	c.Shrink(k)
+}
+
+// rmClauses removes clauses that are already satisfied after simplification.
+func (pb *Problem) rmClauses(removed []bool) {
+	j := 0
+	for i, rm := range removed {
+		if !rm {
+			pb.Clauses[j] = pb.Clauses[i]
+			j++
+		}
+	}
+	pb.Clauses = pb.Clauses[:j]
+}
+
+// simplify simplifies the pure SAT problem, i.e runs unit propagation if possible.
+func (pb *Problem) simplify2() {
+	nbClauses := len(pb.Clauses)
+	restart := true
+	for restart {
+		restart = false
+		i := 0
+		for i < nbClauses {
+			c := pb.Clauses[i]
+			nbLits := c.Len()
+			clauseSat := false
+			j := 0
+			for j < nbLits {
+				lit := c.Get(j)
+				if pb.Model[lit.Var()] == 0 {
+					j++
+				} else if (pb.Model[lit.Var()] == 1) == lit.IsPositive() {
+					clauseSat = true
+					break
+				} else {
+					nbLits--
+					c.Set(j, c.Get(nbLits))
+				}
+			}
+			if clauseSat {
+				nbClauses--
+				pb.Clauses[i] = pb.Clauses[nbClauses]
+			} else if nbLits == 0 {
+				pb.Status = Unsat
+				return
+			} else if nbLits == 1 { // UP
+				pb.addUnit(c.First())
+				if pb.Status == Unsat {
+					return
+				}
+				nbClauses--
+				pb.Clauses[i] = pb.Clauses[nbClauses]
+				restart = true // Must restart, since this lit might have made one more clause Unit or SAT.
+			} else { // nb lits unbound > cardinality
+				if c.Len() != nbLits {
+					c.Shrink(nbLits)
+				}
+				i++
+			}
+		}
+	}
+	pb.updateStatus(nbClauses)
+}
+
+// simplifyCard simplifies the problem, i.e runs unit propagation if possible.
+func (pb *Problem) simplifyCard() {
+	nbClauses := len(pb.Clauses)
+	restart := true
+	for restart {
+		restart = false
+		i := 0
+		for i < nbClauses {
+			c := pb.Clauses[i]
+			nbLits := c.Len()
+			card := c.Cardinality()
+			clauseSat := false
+			nbSat := 0
+			j := 0
+			for j < nbLits {
+				lit := c.Get(j)
+				if pb.Model[lit.Var()] == 0 {
+					j++
+				} else if (pb.Model[lit.Var()] == 1) == lit.IsPositive() {
+					nbSat++
+					if nbSat == card {
+						clauseSat = true
+						break
+					}
+				} else {
+					nbLits--
+					c.Set(j, c.Get(nbLits))
+				}
+			}
+			if clauseSat {
+				nbClauses--
+				pb.Clauses[i] = pb.Clauses[nbClauses]
+			} else if nbLits < card {
+				pb.Status = Unsat
+				return
+			} else if nbLits == card { // UP
+				pb.addUnits(c, nbLits)
+				if pb.Status == Unsat {
+					return
+				}
+				nbClauses--
+				pb.Clauses[i] = pb.Clauses[nbClauses]
+				restart = true // Must restart, since this lit might have made one more clause Unit or SAT.
+			} else { // nb lits unbound > cardinality
+				if c.Len() != nbLits {
+					c.Shrink(nbLits)
+				}
+				i++
+			}
+		}
+	}
+	pb.updateStatus(nbClauses)
+}
+
+func (pb *Problem) simplifyPB() {
+	modified := true
+	for modified {
+		modified = false
+		i := 0
+		for i < len(pb.Clauses) {
+			c := pb.Clauses[i]
+			j := 0
+			card := c.Cardinality()
+			wSum := c.WeightSum()
+			for j < c.Len() {
+				lit := c.Get(j)
+				v := lit.Var()
+				w := c.Weight(j)
+				if pb.Model[v] == 0 { // Literal not assigned: is it unit?
+					if wSum-w < card { // Lit must be true for the clause to be satisfiable
+						pb.addUnit(lit)
+						if pb.Status == Unsat {
+							return
+						}
+						c.removeLit(j)
+						card -= w
+						c.updateCardinality(-w)
+						wSum -= w
+						modified = true
+					} else {
+						j++
+					}
+				} else { // Bound literal: remove it and update, if needed, cardinality
+					wSum -= w
+					if (pb.Model[v] == 1) == lit.IsPositive() {
+						card -= w
+						c.updateCardinality(-w)
+					}
+					c.removeLit(j)
+					modified = true
+				}
+			}
+			if card <= 0 { // Clause is Sat
+				pb.Clauses[i] = pb.Clauses[len(pb.Clauses)-1]
+				pb.Clauses = pb.Clauses[:len(pb.Clauses)-1]
+				modified = true
+			} else if wSum < card {
+				pb.Clauses = nil
+				pb.Status = Unsat
+				return
+			} else {
+				i++
+			}
+		}
+	}
+	if pb.Status == Indet && len(pb.Clauses) == 0 {
+		pb.Status = Sat
+	}
+}
+
+func (pb *Problem) addUnit(lit Lit) {
+	if lit.IsPositive() {
+		if pb.Model[lit.Var()] == -1 {
+			pb.Status = Unsat
+			return
+		}
+		pb.Model[lit.Var()] = 1
+	} else {
+		if pb.Model[lit.Var()] == 1 {
+			pb.Status = Unsat
+			return
+		}
+		pb.Model[lit.Var()] = -1
+	}
+	pb.Units = append(pb.Units, lit)
+}
+
+func (pb *Problem) addUnits(c *Clause, nbLits int) {
+	for i := 0; i < nbLits; i++ {
+		lit := c.Get(i)
+		pb.addUnit(lit)
+	}
+}

vendor/github.com/crillab/gophersat/solver/queue.go

@@ -0,0 +1,146 @@
+/******************************************************************************************[Heap.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+package solver
+
+// A heap implementation with support for decrease/increase key. This is
+// strongly inspired from Minisat's mtl/Heap.h.
+
+type queue struct {
+	activity []float64 // Activity of each variable. This should be the solver's slice, not a copy.
+	content  []int     // Actual content.
+	indices  []int     // Reverse queue, i.e position of each item in content; -1 means absence.
+}
+
+func newQueue(activity []float64) queue {
+	q := queue{
+		activity: activity,
+	}
+	for i := range q.activity {
+		q.insert(i)
+	}
+	return q
+}
+
+func (q *queue) lt(i, j int) bool {
+	return q.activity[i] > q.activity[j]
+}
+
+// Traversal functions.
+func left(i int) int   { return i*2 + 1 }
+func right(i int) int  { return (i + 1) * 2 }
+func parent(i int) int { return (i - 1) >> 1 }
+
+func (q *queue) percolateUp(i int) {
+	x := q.content[i]
+	p := parent(i)
+	for i != 0 && q.lt(x, q.content[p]) {
+		q.content[i] = q.content[p]
+		q.indices[q.content[p]] = i
+		i = p
+		p = parent(p)
+	}
+	q.content[i] = x
+	q.indices[x] = i
+}
+
+func (q *queue) percolateDown(i int) {
+	x := q.content[i]
+	for left(i) < len(q.content) {
+		var child int
+		if right(i) < len(q.content) && q.lt(q.content[right(i)], q.content[left(i)]) {
+			child = right(i)
+		} else {
+			child = left(i)
+		}
+		if !q.lt(q.content[child], x) {
+			break
+		}
+		q.content[i] = q.content[child]
+		q.indices[q.content[i]] = i
+		i = child
+	}
+	q.content[i] = x
+	q.indices[x] = i
+}
+
+func (q *queue) len() int    { return len(q.content) }
+func (q *queue) empty() bool { return len(q.content) == 0 }
+
+func (q *queue) contains(n int) bool {
+	return n < len(q.indices) && q.indices[n] >= 0
+}
+
+func (q *queue) get(index int) int {
+	return q.content[index]
+}
+
+func (q *queue) decrease(n int) {
+	q.percolateUp(q.indices[n])
+}
+
+func (q *queue) increase(n int) {
+	q.percolateDown(q.indices[n])
+}
+
+func (q *queue) update(n int) {
+	if !q.contains(n) {
+		q.insert(n)
+	} else {
+		q.percolateUp(q.indices[n])
+		q.percolateDown(q.indices[n])
+	}
+}
+
+func (q *queue) insert(n int) {
+	for i := len(q.indices); i <= n; i++ {
+		q.indices = append(q.indices, -1)
+	}
+	q.indices[n] = len(q.content)
+	q.content = append(q.content, n)
+	q.percolateUp(q.indices[n])
+}
+
+func (q *queue) removeMin() int {
+	x := q.content[0]
+	q.content[0] = q.content[len(q.content)-1]
+	q.indices[q.content[0]] = 0
+	q.indices[x] = -1
+	q.content = q.content[:len(q.content)-1]
+	if len(q.content) > 1 {
+		q.percolateDown(0)
+	}
+	return x
+}
+
+// Rebuild the heap from scratch, using the elements in 'ns':
+func (q *queue) build(ns []int) {
+	for i := range q.content {
+		q.indices[q.content[i]] = -1
+	}
+	q.content = q.content[:0]
+	for i, val := range ns {
+		q.indices[val] = i
+		q.content = append(q.content, val)
+	}
+	for i := len(q.content)/2 - 1; i >= 0; i-- {
+		q.percolateDown(i)
+	}
+}

vendor/github.com/crillab/gophersat/solver/solver.go

@@ -0,0 +1,844 @@
+package solver
+
+import (
+	"fmt"
+	"sort"
+	"strings"
+	"time"
+)
+
+const (
+	initNbMaxClauses  = 2000  // Maximum # of learned clauses, at first.
+	incrNbMaxClauses  = 300   // By how much # of learned clauses is incremented at each conflict.
+	incrPostponeNbMax = 1000  // By how much # of learned is increased when lots of good clauses are currently learned.
+	clauseDecay       = 0.999 // By how much clauses bumping decays over time.
+	defaultVarDecay   = 0.8   // On each var decay, how much the varInc should be decayed at startup
+)
+
+// Stats are statistics about the resolution of the problem.
+// They are provided for information purpose only.
+type Stats struct {
+	NbRestarts      int
+	NbConflicts     int
+	NbDecisions     int
+	NbUnitLearned   int // How many unit clauses were learned
+	NbBinaryLearned int // How many binary clauses were learned
+	NbLearned       int // How many clauses were learned
+	NbDeleted       int // How many clauses were deleted
+}
+
+// The level a decision was made.
+// A negative value means "negative assignement at that level".
+// A positive value means "positive assignment at that level".
+type decLevel int
+
+// A Model is a binding for several variables.
+// It can be totally bound (i.e all vars have a true or false binding)
+// or only partially (i.e some vars have no binding yet or their binding has no impact).
+// Each var, in order, is associated with a binding. Binding are implemented as
+// decision levels:
+// - a 0 value means the variable is free,
+// - a positive value means the variable was set to true at the given decLevel,
+// - a negative value means the variable was set to false at the given decLevel.
+type Model []decLevel
+
+func (m Model) String() string {
+	bound := make(map[int]decLevel)
+	for i := range m {
+		if m[i] != 0 {
+			bound[i+1] = m[i]
+		}
+	}
+	return fmt.Sprintf("%v", bound)
+}
+
+// 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
+	// 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
+	varQueue        queue
+	varInc          float64 // On each var bump, how big the increment should be
+	clauseInc       float32 // On each var bump, how big the increment should be
+	lbdStats        lbdStats
+	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.
+	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
+}
+
+// New makes a solver, given a number of variables and a set of clauses.
+// nbVars should be consistent with the content of clauses, i.e.
+// the biggest variable in clauses should be >= nbVars.
+func New(problem *Problem) *Solver {
+	if problem.Status == Unsat {
+		return &Solver{status: Unsat}
+	}
+	nbVars := problem.NbVars
+	s := &Solver{
+		nbVars:     nbVars,
+		status:     problem.Status,
+		trail:      make([]Lit, len(problem.Units), nbVars),
+		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),
+	}
+	s.resetOptimPolarity()
+	s.initOptimActivity()
+	s.initWatcherList(problem.Clauses)
+	s.varQueue = newQueue(s.activity)
+	for i, lit := range problem.Units {
+		if lit.IsPositive() {
+			s.model[lit.Var()] = 1
+		} else {
+			s.model[lit.Var()] = -1
+		}
+		s.trail[i] = lit
+	}
+	return s
+}
+
+// sets initial activity for optimization variables, if any.
+func (s *Solver) initOptimActivity() {
+	for i, lit := range s.minLits {
+		w := 1
+		if s.minWeights != nil {
+			w = s.minWeights[i]
+		}
+		s.activity[lit.Var()] += float64(w)
+	}
+}
+
+// resets polarity of optimization lits so that they are negated by default.
+func (s *Solver) resetOptimPolarity() {
+	if s.minLits != nil {
+		for _, lit := range s.minLits {
+			s.polarity[lit.Var()] = !lit.IsPositive() // Try to make lits from the optimization clause false
+		}
+	}
+}
+
+// Optim returns true iff the underlying problem is an optimization problem (rather than a satisfaction one).
+func (s *Solver) Optim() bool {
+	return s.minLits != nil
+}
+
+// OutputModel outputs the model for the problem on stdout.
+func (s *Solver) OutputModel() {
+	if s.status == Sat || s.lastModel != nil {
+		fmt.Printf("s SATISFIABLE\nv ")
+		model := s.model
+		if s.lastModel != nil {
+			model = s.lastModel
+		}
+		for i, val := range model {
+			if val < 0 {
+				fmt.Printf("%d ", -i-1)
+			} else {
+				fmt.Printf("%d ", i+1)
+			}
+		}
+		fmt.Printf("\n")
+	} else if s.status == Unsat {
+		fmt.Printf("s UNSATISFIABLE\n")
+	} else {
+		fmt.Printf("s INDETERMINATE\n")
+	}
+}
+
+// litStatus returns whether the literal is made true (Sat) or false (Unsat) by the
+// current bindings, or if it is unbounded (Indet).
+func (s *Solver) litStatus(l Lit) Status {
+	assign := s.model[l.Var()]
+	if assign == 0 {
+		return Indet
+	}
+	if assign > 0 == l.IsPositive() {
+		return Sat
+	}
+	return Unsat
+}
+
+func (s *Solver) varDecayActivity() {
+	s.varInc *= 1 / s.varDecay
+}
+
+func (s *Solver) varBumpActivity(v Var) {
+	s.activity[v] += s.varInc
+	if s.activity[v] > 1e100 { // Rescaling is needed to avoid overflowing
+		for i := range s.activity {
+			s.activity[i] *= 1e-100
+		}
+		s.varInc *= 1e-100
+	}
+	if s.varQueue.contains(int(v)) {
+		s.varQueue.decrease(int(v))
+	}
+}
+
+// Decays each clause's activity
+func (s *Solver) clauseDecayActivity() {
+	s.clauseInc *= 1 / clauseDecay
+}
+
+// Bumps the given clause's activity.
+func (s *Solver) clauseBumpActivity(c *Clause) {
+	if c.Learned() {
+		c.activity += s.clauseInc
+		if c.activity > 1e30 { // Rescale to avoid overflow
+			for _, c2 := range s.wl.learned {
+				c2.activity *= 1e-30
+			}
+			s.clauseInc *= 1e-30
+		}
+	}
+}
+
+// Chooses an unbound literal to be tested, or -1
+// if all the variables are already bound.
+func (s *Solver) chooseLit() Lit {
+	v := Var(-1)
+	for v == -1 && !s.varQueue.empty() {
+		if v2 := Var(s.varQueue.removeMin()); s.model[v2] == 0 { // Ignore already bound vars
+			v = v2
+		}
+	}
+	if v == -1 {
+		return Lit(-1)
+	}
+	s.Stats.NbDecisions++
+	return v.SignedLit(!s.polarity[v])
+}
+
+func abs(val decLevel) decLevel {
+	if val < 0 {
+		return -val
+	}
+	return val
+}
+
+// Reinitializes bindings (both model & reason) for all variables bound at a decLevel >= lvl.
+// TODO: check this method as it has a weird behavior regarding performance.
+// TODO: clean-up commented-out code and understand underlying performance pattern.
+func (s *Solver) cleanupBindings(lvl decLevel) {
+	i := 0
+	for i < len(s.trail) && abs(s.model[s.trail[i].Var()]) <= lvl {
+		i++
+	}
+	/*
+		for j := len(s.trail) - 1; j >= i; j-- {
+				lit2 := s.trail[j]
+				v := lit2.Var()
+				s.model[v] = 0
+				if s.reason[v] != nil {
+					s.reason[v].unlock()
+					s.reason[v] = nil
+				}
+				s.polarity[v] = lit2.IsPositive()
+				if !s.varQueue.contains(int(v)) {
+					s.varQueue.insert(int(v))
+				}
+			}
+			s.trail = s.trail[:i]
+	*/
+	toInsert := s.trailBuf[:0] // make([]int, 0, len(s.trail)-i)
+	for j := i; j < len(s.trail); j++ {
+		lit2 := s.trail[j]
+		v := lit2.Var()
+		s.model[v] = 0
+		if s.reason[v] != nil {
+			s.reason[v].unlock()
+			s.reason[v] = nil
+		}
+		s.polarity[v] = lit2.IsPositive()
+		if !s.varQueue.contains(int(v)) {
+			toInsert = append(toInsert, int(v))
+			s.varQueue.insert(int(v))
+		}
+	}
+	s.trail = s.trail[:i]
+	for i := len(toInsert) - 1; i >= 0; i-- {
+		s.varQueue.insert(toInsert[i])
+	}
+	/*for i := len(s.trail) - 1; i >= 0; i-- {
+		lit := s.trail[i]
+		v := lit.Var()
+		if abs(s.model[v]) <= lvl { // All lits in trail before here must keep their status.
+			s.trail = s.trail[:i+1]
+			break
+		}
+		s.model[v] = 0
+		if s.reason[v] != nil {
+			s.reason[v].unlock()
+			s.reason[v] = nil
+		}
+		s.polarity[v] = lit.IsPositive()
+		if !s.varQueue.contains(int(v)) {
+			s.varQueue.insert(int(v))
+		}
+	}*/
+	s.resetOptimPolarity()
+}
+
+// Given the last learnt clause and the levels at which vars were bound,
+// Returns the level to bt to and the literal to bind
+func backtrackData(c *Clause, model []decLevel) (btLevel decLevel, lit Lit) {
+	btLevel = abs(model[c.Get(1).Var()])
+	return btLevel, c.Get(0)
+}
+
+func (s *Solver) rebuildOrderHeap() {
+	ints := make([]int, s.nbVars)
+	for v := 0; v < s.nbVars; v++ {
+		if s.model[v] == 0 {
+			ints = append(ints, int(v))
+		}
+	}
+	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 {
+		if conflict := s.unifyLiteral(lit, lvl); conflict == nil { // Pick new branch or restart
+			if s.lbdStats.mustRestart() {
+				s.lbdStats.clear()
+				s.cleanupBindings(1)
+				return Indet
+			}
+			if s.Stats.NbConflicts >= s.wl.idxReduce*s.wl.nbMax {
+				s.wl.idxReduce = (s.Stats.NbConflicts / s.wl.nbMax) + 1
+				s.reduceLearned()
+				s.bumpNbMax()
+			}
+			lvl++
+			lit = s.chooseLit()
+		} else { // Deal with conflict
+			s.Stats.NbConflicts++
+			if s.Stats.NbConflicts%5000 == 0 && s.varDecay < 0.95 {
+				s.varDecay += 0.01
+			}
+			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
+				s.Stats.NbUnitLearned++
+				s.lbdStats.addLbd(1)
+				s.cleanupBindings(1)
+				s.model[unit.Var()] = lvlToSignedLvl(unit, 1)
+				if conflict = s.unifyLiteral(unit, 1); conflict != nil { // top-level conflict
+					s.status = Unsat
+					return Unsat
+				}
+				// s.rmSatClauses()
+				s.rebuildOrderHeap()
+				lit = s.chooseLit()
+				lvl = 2
+			} else {
+				if learnt.Len() == 2 {
+					s.Stats.NbBinaryLearned++
+				}
+				s.Stats.NbLearned++
+				s.lbdStats.addLbd(learnt.lbd())
+				s.addLearned(learnt)
+				lvl, lit = backtrackData(learnt, s.model)
+				s.cleanupBindings(lvl)
+				s.reason[lit.Var()] = learnt
+				learnt.lock()
+			}
+		}
+	}
+	return Sat
+}
+
+// Searches until a restart is needed.
+func (s *Solver) search() Status {
+	s.localNbRestarts++
+	lvl := decLevel(2) // Level starts at 2, for implementation reasons : 1 is for top-level bindings; 0 means "no level assigned yet"
+	s.status = s.propagateAndSearch(s.chooseLit(), lvl)
+	return s.status
+}
+
+// Solve solves the problem associated with the solver and returns the appropriate status.
+func (s *Solver) Solve() Status {
+	if s.status == Unsat {
+		return s.status
+	}
+	s.status = Indet
+	//s.lbdStats.clear()
+	s.localNbRestarts = 0
+	var end chan struct{}
+	if s.Verbose {
+		end = make(chan struct{})
+		defer close(end)
+		go func() { // Function displaying stats during resolution
+			fmt.Printf("c ======================================================================================\n")
+			fmt.Printf("c | Restarts |  Conflicts  |  Learned  |  Deleted  | Del%% | Reduce |   Units learned   |\n")
+			fmt.Printf("c ======================================================================================\n")
+			ticker := time.NewTicker(3 * time.Second)
+			defer ticker.Stop()
+			for { // There might be concurrent access in a few places but this is okay since we are very conservative and don't modify state.
+				select {
+				case <-ticker.C:
+				case <-end:
+					return
+				}
+				if s.status == Indet {
+					iter := s.Stats.NbRestarts + 1
+					nbConfl := s.Stats.NbConflicts
+					nbReduce := s.wl.idxReduce - 1
+					nbLearned := len(s.wl.learned)
+					nbDel := s.Stats.NbDeleted
+					pctDel := int(100 * float64(nbDel) / float64(s.Stats.NbLearned))
+					nbUnit := s.Stats.NbUnitLearned
+					fmt.Printf("c | %8d | %11d | %9d | %9d | %3d%% | %6d | %8d/%8d |\n", iter, nbConfl, nbLearned, nbDel, pctDel, nbReduce, nbUnit, s.nbVars)
+				}
+			}
+		}()
+	}
+	for s.status == Indet {
+		s.search()
+		if s.status == Indet {
+			s.Stats.NbRestarts++
+			s.rebuildOrderHeap()
+		}
+	}
+	if s.status == Sat {
+		s.lastModel = make(Model, len(s.model))
+		copy(s.lastModel, s.model)
+	}
+	if s.Verbose {
+		end <- struct{}{}
+		fmt.Printf("c ======================================================================================\n")
+	}
+	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.
+func (s *Solver) Enumerate(models chan []bool, stop chan struct{}) int {
+	if models != nil {
+		defer close(models)
+	}
+	s.lastModel = make(Model, len(s.model))
+	nb := 0
+	lit := s.chooseLit()
+	var lvl decLevel
+	for s.status != Unsat {
+		for s.status == Indet {
+			s.search()
+			if s.status == Indet {
+				s.Stats.NbRestarts++
+			}
+		}
+		if s.status == Sat {
+			nb++
+			if models != nil {
+				copy(s.lastModel, s.model)
+				models <- s.Model()
+			}
+			s.status = Indet
+			lits := s.decisionLits()
+			switch len(lits) {
+			case 0:
+				s.status = Unsat
+			case 1:
+				s.propagateUnits(lits)
+			default:
+				c := NewClause(lits)
+				s.appendClause(c)
+				lit = lits[len(lits)-1]
+				v := lit.Var()
+				lvl = abs(s.model[v]) - 1
+				s.cleanupBindings(lvl)
+				s.reason[v] = c // Must do it here because it won't be made by propagateAndSearch
+				s.propagateAndSearch(lit, lvl)
+			}
+		}
+	}
+	return nb
+}
+
+// CountModels returns the total number of models for the given problem.
+func (s *Solver) CountModels() int {
+	var end chan struct{}
+	if s.Verbose {
+		end = make(chan struct{})
+		defer close(end)
+		go func() { // Function displaying stats during resolution
+			fmt.Printf("c ======================================================================================\n")
+			fmt.Printf("c | Restarts |  Conflicts  |  Learned  |  Deleted  | Del%% | Reduce |   Units learned   |\n")
+			fmt.Printf("c ======================================================================================\n")
+			ticker := time.NewTicker(3 * time.Second)
+			defer ticker.Stop()
+			for { // There might be concurrent access in a few places but this is okay since we are very conservative and don't modify state.
+				select {
+				case <-ticker.C:
+				case <-end:
+					return
+				}
+				if s.status == Indet {
+					iter := s.Stats.NbRestarts + 1
+					nbConfl := s.Stats.NbConflicts
+					nbReduce := s.wl.idxReduce - 1
+					nbLearned := len(s.wl.learned)
+					nbDel := s.Stats.NbDeleted
+					pctDel := int(100 * float64(nbDel) / float64(s.Stats.NbLearned))
+					nbUnit := s.Stats.NbUnitLearned
+					fmt.Printf("c | %8d | %11d | %9d | %9d | %3d%% | %6d | %8d/%8d |\n", iter, nbConfl, nbLearned, nbDel, pctDel, nbReduce, nbUnit, s.nbVars)
+				}
+			}
+		}()
+	}
+	nb := 0
+	lit := s.chooseLit()
+	var lvl decLevel
+	for s.status != Unsat {
+		for s.status == Indet {
+			s.search()
+			if s.status == Indet {
+				s.Stats.NbRestarts++
+			}
+		}
+		if s.status == Sat {
+			nb++
+			if s.Verbose {
+				fmt.Printf("c found %d model(s)\n", nb)
+			}
+			s.status = Indet
+			lits := s.decisionLits()
+			switch len(lits) {
+			case 0:
+				s.status = Unsat
+			case 1:
+				s.propagateUnits(lits)
+			default:
+				c := NewClause(lits)
+				s.appendClause(c)
+				lit = lits[len(lits)-1]
+				v := lit.Var()
+				lvl = abs(s.model[v]) - 1
+				s.cleanupBindings(lvl)
+				s.reason[v] = c // Must do it here because it won't be made by propagateAndSearch
+				s.propagateAndSearch(lit, lvl)
+			}
+		}
+	}
+	if s.Verbose {
+		end <- struct{}{}
+		fmt.Printf("c ======================================================================================\n")
+	}
+	return nb
+}
+
+// decisionLits returns the negation of all decision values once a model was found, ordered by decision levels.
+// This will allow for searching other models.
+func (s *Solver) decisionLits() []Lit {
+	lastLit := s.trail[len(s.trail)-1]
+	lvls := abs(s.model[lastLit.Var()])
+	lits := make([]Lit, lvls-1)
+	for i, r := range s.reason {
+		if lvl := abs(s.model[i]); r == nil && lvl > 1 {
+			if s.model[i] < 0 {
+				// lvl-2 : levels beside unit clauses start at 2, not 0 or 1!
+				lits[lvl-2] = IntToLit(int32(i + 1))
+			} else {
+				lits[lvl-2] = IntToLit(int32(-i - 1))
+			}
+		}
+	}
+	return lits
+}
+
+func (s *Solver) propagateUnits(units []Lit) {
+	for _, unit := range units {
+		s.lbdStats.addLbd(1)
+		s.Stats.NbUnitLearned++
+		s.cleanupBindings(1)
+		s.model[unit.Var()] = lvlToSignedLvl(unit, 1)
+		if s.unifyLiteral(unit, 1) != nil {
+			s.status = Unsat
+			return
+		}
+		s.rebuildOrderHeap()
+	}
+}
+
+// PBString returns a representation of the solver's state as a pseudo-boolean problem.
+func (s *Solver) PBString() string {
+	meta := fmt.Sprintf("* #variable= %d #constraint= %d #learned= %d\n", s.nbVars, len(s.wl.pbClauses), len(s.wl.learned))
+	minLine := ""
+	if s.minLits != nil {
+		terms := make([]string, len(s.minLits))
+		for i, lit := range s.minLits {
+			weight := 1
+			if s.minWeights != nil {
+				weight = s.minWeights[i]
+			}
+			val := lit.Int()
+			sign := ""
+			if val < 0 {
+				val = -val
+				sign = "~"
+			}
+			terms[i] = fmt.Sprintf("%d %sx%d", weight, sign, val)
+		}
+		minLine = fmt.Sprintf("min: %s ;\n", strings.Join(terms, " +"))
+	}
+	clauses := make([]string, len(s.wl.pbClauses)+len(s.wl.learned))
+	for i, c := range s.wl.pbClauses {
+		clauses[i] = c.PBString()
+	}
+	for i, c := range s.wl.learned {
+		clauses[i+len(s.wl.pbClauses)] = c.PBString()
+	}
+	for i := 0; i < len(s.model); i++ {
+		if s.model[i] == 1 {
+			clauses = append(clauses, fmt.Sprintf("1 x%d = 1 ;", i+1))
+		} else if s.model[i] == -1 {
+			clauses = append(clauses, fmt.Sprintf("1 x%d = 0 ;", i+1))
+		}
+	}
+	return meta + minLine + strings.Join(clauses, "\n")
+}
+
+// AppendClause appends a new clause to the set of clauses.
+// This is not a learned clause, but a clause that is part of the problem added afterwards (during model counting, for instance).
+func (s *Solver) AppendClause(clause *Clause) {
+	s.cleanupBindings(1)
+	card := clause.Cardinality()
+	minW := 0
+	maxW := 0
+	i := 0
+	for i < clause.Len() {
+		lit := clause.Get(i)
+		switch s.litStatus(lit) {
+		case Sat:
+			w := clause.Weight(i)
+			minW += w
+			maxW += w
+			clause.removeLit(i)
+			clause.updateCardinality(-w)
+		case Unsat:
+			clause.removeLit(i)
+		default:
+			maxW += clause.Weight(i)
+			i++
+		}
+	}
+	if minW >= card { // clause is already sat
+		return
+	}
+	if maxW < card { // clause cannot be satisfied
+		s.status = Unsat
+		return
+	}
+	if maxW == card { // Unit
+		s.propagateUnits(clause.lits)
+	} else {
+		s.appendClause(clause)
+	}
+}
+
+// Model returns a slice that associates, to each variable, its binding.
+// If s's status is not Sat, the method will panic.
+func (s *Solver) Model() []bool {
+	if s.lastModel == nil {
+		panic("cannot call Model() from a non-Sat solver")
+	}
+	res := make([]bool, s.nbVars)
+	for i, lvl := range s.lastModel {
+		res[i] = lvl > 0
+	}
+	return res
+}
+
+// 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.
+func (s *Solver) Optimal(results chan Result, stop chan struct{}) (res Result) {
+	if results != nil {
+		defer close(results)
+	}
+	status := s.Solve()
+	if status == Unsat { // Problem cannot be satisfied at all
+		res.Status = Unsat
+		if results != nil {
+			results <- res
+		}
+		return res
+	}
+	if s.minLits == nil { // No optimization clause: this is a decision problem, solution is optimal
+		s.lastModel = make(Model, len(s.model))
+		copy(s.lastModel, s.model)
+		res := Result{
+			Status: Sat,
+			Model:  s.Model(),
+			Weight: 0,
+		}
+		if results != nil {
+			results <- res
+		}
+		return res
+	}
+	maxCost := 0
+	if s.minWeights == nil {
+		maxCost = len(s.minLits)
+	} else {
+		for _, w := range s.minWeights {
+			maxCost += w
+		}
+	}
+	s.asumptions = make([]Lit, len(s.minLits))
+	for i, lit := range s.minLits {
+		s.asumptions[i] = lit.Negation()
+	}
+	weights := make([]int, len(s.minWeights))
+	copy(weights, s.minWeights)
+	sort.Sort(wLits{lits: s.asumptions, weights: weights})
+	s.lastModel = make(Model, len(s.model))
+	var cost int
+	for status == Sat {
+		copy(s.lastModel, s.model) // Save this model: it might be the last one
+		cost = 0
+		for i, lit := range s.minLits {
+			if (s.model[lit.Var()] > 0) == lit.IsPositive() {
+				if s.minWeights == nil {
+					cost++
+				} else {
+					cost += s.minWeights[i]
+				}
+			}
+		}
+		res = Result{
+			Status: Sat,
+			Model:  s.Model(),
+			Weight: cost,
+		}
+		if results != nil {
+			results <- res
+		}
+		if cost == 0 {
+			break
+		}
+		// Add a constraint incrementing current best cost
+		lits2 := make([]Lit, len(s.minLits))
+		weights2 := make([]int, len(s.minWeights))
+		copy(lits2, s.asumptions)
+		copy(weights2, weights)
+		s.AppendClause(NewPBClause(lits2, weights2, maxCost-cost+1))
+		s.rebuildOrderHeap()
+		status = s.Solve()
+	}
+	return res
+}
+
+// Minimize tries to find a model that minimizes the weight of the clause defined as the optimisation clause in the problem.
+// If no model can be found, it will return a cost of -1.
+// Otherwise, calling s.Model() afterwards will return the model that satisfy the formula, such that no other model with a smaller cost exists.
+// If this function is called on a non-optimization problem, it will either return -1, or a cost of 0 associated with a
+// satisfying model (ie any model is an optimal model).
+func (s *Solver) Minimize() int {
+	status := s.Solve()
+	if status == Unsat { // Problem cannot be satisfied at all
+		return -1
+	}
+	if s.minLits == nil { // No optimization clause: this is a decision problem, solution is optimal
+		return 0
+	}
+	maxCost := 0
+	if s.minWeights == nil {
+		maxCost = len(s.minLits)
+	} else {
+		for _, w := range s.minWeights {
+			maxCost += w
+		}
+	}
+	s.asumptions = make([]Lit, len(s.minLits))
+	for i, lit := range s.minLits {
+		s.asumptions[i] = lit.Negation()
+	}
+	weights := make([]int, len(s.minWeights))
+	copy(weights, s.minWeights)
+	sort.Sort(wLits{lits: s.asumptions, weights: weights})
+	s.lastModel = make(Model, len(s.model))
+	var cost int
+	for status == Sat {
+		copy(s.lastModel, s.model) // Save this model: it might be the last one
+		cost = 0
+		for i, lit := range s.minLits {
+			if (s.model[lit.Var()] > 0) == lit.IsPositive() {
+				if s.minWeights == nil {
+					cost++
+				} else {
+					cost += s.minWeights[i]
+				}
+			}
+		}
+		if cost == 0 {
+			return 0
+		}
+		if s.Verbose {
+			fmt.Printf("o %d\n", cost)
+		}
+		// Add a constraint incrementing current best cost
+		lits2 := make([]Lit, len(s.minLits))
+		weights2 := make([]int, len(s.minWeights))
+		copy(lits2, s.asumptions)
+		copy(weights2, weights)
+		s.AppendClause(NewPBClause(lits2, weights2, maxCost-cost+1))
+		s.rebuildOrderHeap()
+		status = s.Solve()
+	}
+	return cost
+}
+
+// functions to sort asumptions for pseudo-boolean minimization clause.
+type wLits struct {
+	lits    []Lit
+	weights []int
+}
+
+func (wl wLits) Len() int           { return len(wl.lits) }
+func (wl wLits) Less(i, j int) bool { return wl.weights[i] > wl.weights[j] }
+
+func (wl wLits) Swap(i, j int) {
+	wl.lits[i], wl.lits[j] = wl.lits[j], wl.lits[i]
+	wl.weights[i], wl.weights[j] = wl.weights[j], wl.weights[i]
+}

vendor/github.com/crillab/gophersat/solver/sort.go

@@ -0,0 +1,23 @@
+package solver
+
+import "sort"
+
+// clauseSorter is a structure to facilitate the sorting of lits in a learned clause
+// according to their respective decision levels.
+type clauseSorter struct {
+	lits  []Lit
+	model Model
+}
+
+func (cs *clauseSorter) Len() int { return len(cs.lits) }
+func (cs *clauseSorter) Less(i, j int) bool {
+	return abs(cs.model[cs.lits[i].Var()]) > abs(cs.model[cs.lits[j].Var()])
+}
+func (cs *clauseSorter) Swap(i, j int) { cs.lits[i], cs.lits[j] = cs.lits[j], cs.lits[i] }
+
+// sortLiterals sorts the literals depending on the decision level they were bound
+// i.e. abs(model[lits[i]]) <= abs(model[lits[i+1]]).
+func sortLiterals(lits []Lit, model []decLevel) {
+	cs := &clauseSorter{lits, model}
+	sort.Sort(cs)
+}

vendor/github.com/crillab/gophersat/solver/types.go

@@ -0,0 +1,95 @@
+package solver
+
+// Describes basic types and constants that are used in the solver
+
+// Status is the status of a given problem or clause at a given moment.
+type Status byte
+
+const (
+	// Indet means the problem is not proven sat or unsat yet.
+	Indet = Status(iota)
+	// Sat means the problem or clause is satisfied.
+	Sat
+	// Unsat means the problem or clause is unsatisfied.
+	Unsat
+	// Unit is a constant meaning the clause contains only one unassigned literal.
+	Unit
+	// Many is a constant meaning the clause contains at least 2 unassigned literals.
+	Many
+)
+
+func (s Status) String() string {
+	switch s {
+	case Indet:
+		return "INDETERMINATE"
+	case Sat:
+		return "SAT"
+	case Unsat:
+		return "UNSAT"
+	case Unit:
+		return "UNIT"
+	case Many:
+		return "MANY"
+	default:
+		panic("invalid status")
+	}
+}
+
+// Var start at 0 ; thus the CNF variable 1 is encoded as the Var 0.
+type Var int32
+
+// Lit start at 0 and are positive ; the sign is the last bit.
+// Thus the CNF literal -3 is encoded as 2 * (3-1) + 1 = 5.
+type Lit int32
+
+// IntToLit converts a CNF literal to a Lit.
+func IntToLit(i int32) Lit {
+	if i < 0 {
+		return Lit(2*(-i-1) + 1)
+	}
+	return Lit(2 * (i - 1))
+}
+
+// IntToVar converts a CNF variable to a Var.
+func IntToVar(i int32) Var {
+	return Var(i - 1)
+}
+
+// Lit returns the positive Lit associated to v.
+func (v Var) Lit() Lit {
+	return Lit(v * 2)
+}
+
+// SignedLit returns the Lit associated to v, negated if 'signed', positive else.
+func (v Var) SignedLit(signed bool) Lit {
+	if signed {
+		return Lit(v*2) + 1
+	}
+	return Lit(v * 2)
+}
+
+// Var returns the variable of l.
+func (l Lit) Var() Var {
+	return Var(l / 2)
+}
+
+// Int returns the equivalent CNF literal.
+func (l Lit) Int() int32 {
+	sign := l&1 == 1
+	res := int32((l / 2) + 1)
+	if sign {
+		return -res
+	}
+	return res
+}
+
+// IsPositive is true iff l is > 0
+func (l Lit) IsPositive() bool {
+	return l%2 == 0
+}
+
+// Negation returns -l, i.e the positive version of l if it is negative,
+// or the negative version otherwise.
+func (l Lit) Negation() Lit {
+	return l ^ 1
+}

vendor/github.com/crillab/gophersat/solver/watcher.go

@@ -0,0 +1,448 @@
+package solver
+
+import "sort"
+
+type watcher struct {
+	other  Lit // Another lit from the clause
+	clause *Clause
+}
+
+// A watcherList is a structure used to store clauses and propagate unit literals efficiently.
+type watcherList struct {
+	nbMax     int         // Max # of learned clauses at current moment
+	idxReduce int         // # of calls to reduce + 1
+	wlistBin  [][]watcher // For each literal, a list of binary clauses where its negation appears
+	wlist     [][]watcher // For each literal, a list of non-binary clauses where its negation appears atposition 1 or 2
+	wlistPb   [][]*Clause // For each literal a list of PB or cardinality constraints.
+	pbClauses []*Clause   // All the problem clauses.
+	learned   []*Clause
+}
+
+// initWatcherList makes a new watcherList for the solver.
+func (s *Solver) initWatcherList(clauses []*Clause) {
+	nbMax := initNbMaxClauses
+	newClauses := make([]*Clause, len(clauses))
+	copy(newClauses, clauses)
+	s.wl = watcherList{
+		nbMax:     nbMax,
+		idxReduce: 1,
+		wlistBin:  make([][]watcher, s.nbVars*2),
+		wlist:     make([][]watcher, s.nbVars*2),
+		wlistPb:   make([][]*Clause, s.nbVars*2),
+		pbClauses: newClauses,
+	}
+	for _, c := range clauses {
+		s.watchClause(c)
+	}
+}
+
+// appendClause appends the clause without checking whether the clause is already satisfiable, unit, or unsatisfiable.
+// To perform those checks, call s.AppendClause.
+// clause is supposed to be a problem clause, not a learned one.
+func (s *Solver) appendClause(clause *Clause) {
+	s.wl.pbClauses = append(s.wl.pbClauses, clause)
+	s.watchClause(clause)
+}
+
+// bumpNbMax increases the max nb of clauses used.
+// It is typically called after a restart.
+func (s *Solver) bumpNbMax() {
+	s.wl.nbMax += incrNbMaxClauses
+}
+
+// postponeNbMax increases the max nb of clauses used.
+// It is typically called when too many good clauses were learned and a cleaning was expected.
+func (s *Solver) postponeNbMax() {
+	s.wl.nbMax += incrPostponeNbMax
+}
+
+// Utilities for sorting according to clauses' LBD and activities.
+func (wl *watcherList) Len() int      { return len(wl.learned) }
+func (wl *watcherList) Swap(i, j int) { wl.learned[i], wl.learned[j] = wl.learned[j], wl.learned[i] }
+
+func (wl *watcherList) Less(i, j int) bool {
+	ci := wl.learned[i]
+	cj := wl.learned[j]
+	lbdI := ci.lbd()
+	lbdJ := cj.lbd()
+	// Sort by lbd, break ties by activity
+	return lbdI > lbdJ || (lbdI == lbdJ && wl.learned[i].activity < wl.learned[j].activity)
+}
+
+// Watches the provided clause.
+func (s *Solver) watchClause(c *Clause) {
+	if c.Len() == 2 {
+		first := c.First()
+		second := c.Second()
+		neg0 := first.Negation()
+		neg1 := second.Negation()
+		s.wl.wlistBin[neg0] = append(s.wl.wlistBin[neg0], watcher{clause: c, other: second})
+		s.wl.wlistBin[neg1] = append(s.wl.wlistBin[neg1], watcher{clause: c, other: first})
+	} else if c.PseudoBoolean() {
+		w := 0
+		i := 0
+		for i < 2 || w <= c.Cardinality() {
+			lit := c.Get(i)
+			neg := lit.Negation()
+			s.wl.wlistPb[neg] = append(s.wl.wlistPb[neg], c)
+			c.pbData.watched[i] = true
+			w += c.Weight(i)
+			i++
+		}
+	} else if c.Cardinality() > 1 {
+		for i := 0; i < c.Cardinality()+1; i++ {
+			lit := c.Get(i)
+			neg := lit.Negation()
+			s.wl.wlistPb[neg] = append(s.wl.wlistPb[neg], c)
+		}
+	} else { // Regular, propositional clause
+		first := c.First()
+		second := c.Second()
+		neg0 := first.Negation()
+		neg1 := second.Negation()
+		s.wl.wlist[neg0] = append(s.wl.wlist[neg0], watcher{clause: c, other: second})
+		s.wl.wlist[neg1] = append(s.wl.wlist[neg1], watcher{clause: c, other: first})
+	}
+}
+
+// unwatch the given learned clause.
+// NOTE: since it is only called when c.lbd() > 2, we know for sure
+// that c is not a binary clause.
+// We also know for sure this is a propositional clause, since only those are learned.
+func (s *Solver) unwatchClause(c *Clause) {
+	for i := 0; i < 2; i++ {
+		neg := c.Get(i).Negation()
+		j := 0
+		length := len(s.wl.wlist[neg])
+		// We're looking for the index of the clause.
+		// This will panic if c is not in wlist[neg], but this shouldn't happen.
+		for s.wl.wlist[neg][j].clause != c {
+			j++
+		}
+		s.wl.wlist[neg][j] = s.wl.wlist[neg][length-1]
+		s.wl.wlist[neg] = s.wl.wlist[neg][:length-1]
+	}
+}
+
+// reduceLearned removes a few learned clauses that are deemed useless.
+func (s *Solver) reduceLearned() {
+	sort.Sort(&s.wl)
+	nbLearned := len(s.wl.learned)
+	length := nbLearned / 2
+	if s.wl.learned[length].lbd() <= 3 { // Lots of good clauses, postpone reduction
+		s.postponeNbMax()
+	}
+	nbRemoved := 0
+	for i := 0; i < length; i++ {
+		c := s.wl.learned[i]
+		if c.lbd() <= 2 || c.isLocked() {
+			continue
+		}
+		nbRemoved++
+		s.Stats.NbDeleted++
+		s.wl.learned[i] = s.wl.learned[nbLearned-nbRemoved]
+		s.unwatchClause(c)
+	}
+	nbLearned -= nbRemoved
+	s.wl.learned = s.wl.learned[:nbLearned]
+}
+
+// Adds the given learned clause and updates watchers.
+// If too many clauses have been learned yet, one will be removed.
+func (s *Solver) addLearned(c *Clause) {
+	s.wl.learned = append(s.wl.learned, c)
+	s.watchClause(c)
+	s.clauseBumpActivity(c)
+}
+
+// If l is negative, -lvl is returned. Else, lvl is returned.
+func lvlToSignedLvl(l Lit, lvl decLevel) decLevel {
+	if l.IsPositive() {
+		return lvl
+	}
+	return -lvl
+}
+
+// Removes the first occurrence of c from lst.
+// The element *must* be present into lst.
+func removeFrom(lst []*Clause, c *Clause) []*Clause {
+	i := 0
+	for lst[i] != c {
+		i++
+	}
+	last := len(lst) - 1
+	lst[i] = lst[last]
+	return lst[:last]
+}
+
+// Propagates literals in the trail starting from the ptrth, and returns a conflict clause, or nil if none arose.
+func (s *Solver) propagate(ptr int, lvl decLevel) *Clause {
+	for ptr < len(s.trail) {
+		lit := s.trail[ptr]
+		for _, w := range s.wl.wlistBin[lit] {
+			v2 := w.other.Var()
+			if assign := s.model[v2]; assign == 0 { // Other was unbounded: propagate
+				s.reason[v2] = w.clause
+				w.clause.lock()
+				s.model[v2] = lvlToSignedLvl(w.other, lvl)
+				s.trail = append(s.trail, w.other)
+			} else if (assign > 0) != w.other.IsPositive() { // Conflict here
+				return w.clause
+			}
+		}
+		if confl := s.simplifyPropClauses(lit, lvl); confl != nil {
+			return confl
+		}
+		for _, c := range s.wl.wlistPb[lit] {
+			if c.PseudoBoolean() {
+				if !s.simplifyPseudoBool(c, lvl) {
+					return c
+				}
+			} else {
+				if !s.simplifyCardClause(c, lvl) {
+					return c
+				}
+			}
+		}
+		ptr++
+	}
+	// No unsat clause was met
+	return nil
+}
+
+// Unifies the given literal and returns a conflict clause, or nil if no conflict arose.
+func (s *Solver) unifyLiteral(lit Lit, lvl decLevel) *Clause {
+	s.model[lit.Var()] = lvlToSignedLvl(lit, lvl)
+	s.trail = append(s.trail, lit)
+	return s.propagate(len(s.trail)-1, lvl)
+}
+
+func (s *Solver) propagateUnit(c *Clause, lvl decLevel, unit Lit) {
+	v := unit.Var()
+	s.reason[v] = c
+	c.lock()
+	s.model[v] = lvlToSignedLvl(unit, lvl)
+	s.trail = append(s.trail, unit)
+}
+
+func (s *Solver) simplifyPropClauses(lit Lit, lvl decLevel) *Clause {
+	wl := s.wl.wlist[lit]
+	j := 0
+	for i, w := range wl {
+		if s.litStatus(w.other) == Sat { // blocking literal is SAT? Don't explore clause!
+			wl[j] = w
+			j++
+			continue
+		}
+		c := w.clause
+		// make sure c.Second() is lit
+		if c.First() == lit.Negation() {
+			c.swap(0, 1)
+		}
+		w2 := watcher{clause: c, other: c.First()}
+		firstStatus := s.litStatus(c.First())
+		if firstStatus == Sat { // Clause is already sat
+			wl[j] = w2
+			j++
+		} else {
+			found := false
+			for k := 2; k < c.Len(); k++ {
+				if litK := c.Get(k); s.litStatus(litK) != Unsat {
+					c.swap(1, k)
+					neg := litK.Negation()
+					s.wl.wlist[neg] = append(s.wl.wlist[neg], w2)
+					found = true
+					break
+				}
+			}
+			if !found { // No free lit found: unit propagation or UNSAT
+				wl[j] = w2
+				j++
+				if firstStatus == Unsat {
+					copy(wl[j:], wl[i+1:]) // Copy remaining clauses
+					s.wl.wlist[lit] = wl[:len(wl)-((i+1)-j)]
+					return c
+				}
+				s.propagateUnit(c, lvl, c.First())
+			}
+		}
+	}
+	s.wl.wlist[lit] = wl[:j]
+	return nil
+}
+
+// simplifyCardClauses simplifies a clause of cardinality > 1, but with all weights = 1.
+// returns false iff the clause cannot be satisfied.
+func (s *Solver) simplifyCardClause(clause *Clause, lvl decLevel) bool {
+	length := clause.Len()
+	card := clause.Cardinality()
+	nbTrue := 0
+	nbFalse := 0
+	nbUnb := 0
+	done := false
+	for i := 0; i < length && !done; i++ {
+		lit := clause.Get(i)
+		switch s.litStatus(lit) {
+		case Indet:
+			nbUnb++
+			if nbUnb+nbTrue > card {
+				done = true
+			}
+		case Sat:
+			nbTrue++
+			if nbTrue == card {
+				return true
+			}
+			if nbUnb+nbTrue > card {
+				done = true
+			}
+		case Unsat:
+			nbFalse++
+			if length-nbFalse < card {
+				return false
+			}
+		}
+	}
+	if nbTrue >= card {
+		return true
+	}
+	if nbUnb+nbTrue == card {
+		// All unbounded lits must be bound to make the clause true
+		i := 0
+		for nbUnb > 0 {
+			lit := clause.Get(i)
+			if s.model[lit.Var()] == 0 {
+				s.propagateUnit(clause, lvl, lit)
+				nbUnb--
+			} else {
+				i++
+			}
+		}
+		return true
+	}
+	s.swapFalse(clause)
+	return true
+}
+
+// swapFalse swaps enough literals from the clause so that all watching literals are either true or unbounded lits.
+// Must only be called when there a at least cardinality + 1 true and unbounded lits.
+func (s *Solver) swapFalse(clause *Clause) {
+	card := clause.Cardinality()
+	i := 0
+	j := card + 1
+	for i < card+1 {
+		lit := clause.Get(i)
+		for s.litStatus(lit) != Unsat {
+			i++
+			if i == card+1 {
+				return
+			}
+			lit = clause.Get(i)
+		}
+		lit = clause.Get(j)
+		for s.litStatus(lit) == Unsat {
+			j++
+			lit = clause.Get(j)
+		}
+		ni := &s.wl.wlistPb[clause.Get(i).Negation()]
+		nj := &s.wl.wlistPb[clause.Get(j).Negation()]
+		clause.swap(i, j)
+		*ni = removeFrom(*ni, clause)
+		*nj = append(*nj, clause)
+		i++
+		j++
+	}
+}
+
+// sumWeights returns the sum of weights of the given PB clause, if the clause is not SAT yet.
+// If the clause is already SAT, it returns true and the given sum value
+// is meaningless.
+func (s *Solver) sumWeights(c *Clause) (sum int, sat bool) {
+	sum = 0
+	sumSat := 0
+	card := c.Cardinality()
+	for i, v := range c.pbData.weights {
+		if status := s.litStatus(c.Get(i)); status == Indet {
+			sum += v
+		} else if status == Sat {
+			sum += v
+			sumSat += v
+			if sumSat >= card {
+				return sum, true
+			}
+		}
+	}
+	return sum, false
+}
+
+// propagateAll propagates all unbounded literals from c as unit literals
+func (s *Solver) propagateAll(c *Clause, lvl decLevel) {
+	for i := 0; i < c.Len(); i++ {
+		if lit := c.Get(i); s.litStatus(lit) == Indet {
+			s.propagateUnit(c, lvl, lit)
+		}
+	}
+}
+
+// simplifyPseudoBool simplifies a pseudo-boolean constraint.
+// propagates unit literals, if any.
+// returns false if the clause cannot be satisfied.
+func (s *Solver) simplifyPseudoBool(clause *Clause, lvl decLevel) bool {
+	card := clause.Cardinality()
+	foundUnit := true
+	for foundUnit {
+		sumW, sat := s.sumWeights(clause)
+		if sat {
+			return true
+		}
+		if sumW < card {
+			return false
+		}
+		if sumW == card {
+			s.propagateAll(clause, lvl)
+			return true
+		}
+		foundUnit = false
+		for i := 0; i < clause.Len(); i++ {
+			lit := clause.Get(i)
+			if s.litStatus(lit) == Indet && sumW-clause.Weight(i) < card { // lit can't be falsified
+				s.propagateUnit(clause, lvl, lit)
+				foundUnit = true
+			}
+		}
+	}
+	s.updateWatchPB(clause)
+	return true
+}
+
+func (s *Solver) updateWatchPB(clause *Clause) {
+	weightWatched := 0
+	i := 0
+	card := clause.Cardinality()
+	for weightWatched <= card && i < clause.Len() {
+		lit := clause.Get(i)
+		if s.litStatus(lit) == Unsat {
+			if clause.pbData.watched[i] {
+				ni := &s.wl.wlistPb[lit.Negation()]
+				*ni = removeFrom(*ni, clause)
+				clause.pbData.watched[i] = false
+			}
+		} else {
+			weightWatched += clause.Weight(i)
+			if !clause.pbData.watched[i] {
+				ni := &s.wl.wlistPb[lit.Negation()]
+				*ni = append(*ni, clause)
+				clause.pbData.watched[i] = true
+			}
+		}
+		i++
+	}
+	// If there are some more watched literals, they are now useless
+	for i := i; i < clause.Len(); i++ {
+		if clause.pbData.watched[i] {
+			ni := &s.wl.wlistPb[clause.Get(i).Negation()]
+			*ni = removeFrom(*ni, clause)
+			clause.pbData.watched[i] = false
+		}
+	}
+}