kairos/luet
1
0
Fork 0
mirror of https://github.com/mudler/luet.git synced 2025-09-02 07:45:02 +00:00
Code Issues Packages Projects Releases Wiki Activity

update vendor/

Browse Source
This commit is contained in:
Ettore Di Giacinto
2020-02-11 09:52:38 +01:00
parent ac6554c291
commit 7ce522110e
26 changed files with 324 additions and 23 deletions
Download Patch File Download Diff File Expand all files Collapse all files

27
vendor/github.com/crillab/gophersat/solver/card.go generated vendored
View File

@@ -1,27 +0,0 @@
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...)}
}

243
vendor/github.com/crillab/gophersat/solver/clause.go generated vendored
View File

@@ -1,243 +0,0 @@
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())
}

29
vendor/github.com/crillab/gophersat/solver/clause_alloc.go generated vendored
View File

@@ -1,29 +0,0 @@
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]
}

102
vendor/github.com/crillab/gophersat/solver/doc.go generated vendored
View File

@@ -1,102 +0,0 @@
/*
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

35
vendor/github.com/crillab/gophersat/solver/interface.go generated vendored
View File

@@ -1,35 +0,0 @@
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
}

89
vendor/github.com/crillab/gophersat/solver/lbd.go generated vendored
View File

@@ -1,89 +0,0 @@
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
}

121
vendor/github.com/crillab/gophersat/solver/learn.go generated vendored
View File

@@ -1,121 +0,0 @@
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
}

171
vendor/github.com/crillab/gophersat/solver/parser.go generated vendored
View File

@@ -1,171 +0,0 @@
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
}

262
vendor/github.com/crillab/gophersat/solver/parser_pb.go generated vendored
View File

@@ -1,262 +0,0 @@
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
}

101
vendor/github.com/crillab/gophersat/solver/pb.go generated vendored
View File

@@ -1,101 +0,0 @@
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
}

183
vendor/github.com/crillab/gophersat/solver/preprocess.go generated vendored
View File

@@ -1,183 +0,0 @@
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))
// }

347
vendor/github.com/crillab/gophersat/solver/problem.go generated vendored
View File

@@ -1,347 +0,0 @@
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)
}
}

146
vendor/github.com/crillab/gophersat/solver/queue.go generated vendored
View File

@@ -1,146 +0,0 @@
/******************************************************************************************[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)
}
}

844
vendor/github.com/crillab/gophersat/solver/solver.go generated vendored
View File

@@ -1,844 +0,0 @@
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]
}

23
vendor/github.com/crillab/gophersat/solver/sort.go generated vendored
View File

@@ -1,23 +0,0 @@
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)
}

95
vendor/github.com/crillab/gophersat/solver/types.go generated vendored
View File

@@ -1,95 +0,0 @@
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
}

448
vendor/github.com/crillab/gophersat/solver/watcher.go generated vendored
View File

@@ -1,448 +0,0 @@
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
}
}
}