Merge pull request #11 from irifrance/m

activation lit support

Author: wsc1

gini.go

@@ -99,6 +99,9 @@ func (g *Gini) Lit() z.Lit {
 //  g.Add(z)
 //  g.Add(0)
 //
+// If Add is called under a test scope, then Add will panic
+// if `m` is 0/LitNull.
+//
 func (g *Gini) Add(m z.Lit) {
 	g.xo.Add(m)
 }
@@ -160,6 +163,10 @@ func (g *Gini) Why(ms []z.Lit) []z.Lit {
 //  - All assigned literals since last test if SAT or UNKNOWN
 //  - Either the literals of a clause which is unsat under BCP or an assumption
 //    which is false under BCP, whichever is found first.
+//
+// When g is under a test scope, many operations are not
+// possible, in particular: {Add,Activate,ActivateWith,Deactivate}
+// are unsupported operations under a test scope.
 func (g *Gini) Test(dst []z.Lit) (res int, out []z.Lit) {
 	return g.xo.Test(dst)
 }
@@ -189,3 +196,69 @@ func (g *Gini) Untest() int {
 func (g *Gini) Reasons(dst []z.Lit, m z.Lit) []z.Lit {
 	return g.xo.Reasons(dst, m)
 }
+
+// Create a clause from the last (non 0-terminated, non-empty) sequence of Adds and
+// `m.Not()`.  Activate panics if the last sequence of Adds since Add(0) is empty,
+// in other words, don't try to use an activation literal for the empty clause.
+//
+// Additionally, in this case subsequent behavior of `g` is undefined.  The caller
+// should verify a clause is not empty using `g.Value(m)` for all literals in in
+// the clause to activate.
+//
+// To active the clause, assume `m`.
+//
+// Example:
+//
+//  if g.Value(a) != false || g.Value(b) != false {
+//    g.Add(a)
+//    g.Add(b)
+//    m := g.Activate()  // don't call g.Add(0).
+//    g.Assume(m) // now the clause (a + b)  is active
+//    if g.Solve() == 1 {
+//       // do something
+//    }
+//    // now the clause (a+b) is not active.
+//    g.Deactivate(m)
+//    // now `m` can be re-used and the solver can ignore
+//    // clauses with `m`.
+//  }
+//
+// Activation of all clauses can be used in conjunction with cardinality constraints
+// to easily create a MAXSAT solver.
+//
+// Activate is an unsupported operation under a test scope
+// and will panic if called under a test scope.
+func (g *Gini) Activate() (m z.Lit) {
+	return g.xo.Activate()
+}
+
+// ActivateWith allows the caller to specify the activation literal.  It is
+// useful when the caller needs to activate many clauses with one literal.
+// However, please note that activation literals are volatile and will be
+// recycled on Deactivate.  As with Activate, ActivateWith should not
+// be used to activate the empty clause.  In this case, ActivateWith
+// panics and subsequent behavior of g is undefined.
+//
+// ActivateWith is an unsupported operation under a test scope
+// and will panic if called under a test scope.
+func (g *Gini) ActivateWith(act z.Lit) {
+	g.xo.ActivateWith(act)
+}
+
+// ActivationLit returns a new literal to be used with ActivateWith().
+//
+// ActivationLit is an unsupported operation under a test scope and will
+// panic if called under a test scope.
+func (g *Gini) ActivationLit() z.Lit {
+	return g.xo.ActivationLit()
+}
+
+// Deactivate deactivates a literal as returned by Activate.  Deactivation
+// frees the literal for future Activations and removes all clauses, including
+// learned clauses, which contain `m.Not()`.
+//
+// Deactivate is an unsupported operation under a test scope
+// and will panic if called under a test scope.
+func (g *Gini) Deactivate(m z.Lit) {
+	g.xo.Deactivate(m)
+}

inter/s.go

@@ -38,6 +38,10 @@ type Adder interface {
 	// is accessing the object implementing adder.  Other
 	// methods may provide safety in the presence of multiple
 	// goroutines.  Add in general does not.
+	//
+	// If the implemation of Add is a solver under a test scope
+	// then Add undoes the test.
+	//
 	Add(m z.Lit)
 }
 
@@ -85,8 +89,8 @@ type Testable interface {
 	Assumable
 
 	// Test the current assumptions under unit propagation.
-	// place the resulting propagated literals since the last
-	// test in dst and return
+	// append the resulting propagated literals since the last
+	// test in dst, if dst is not nil, and return
 	//
 	//  result: -1 for UNSAT, 1 for SAT, 0 for UNKNOWN
 	//  out: the propagated literals since last Test,
@@ -125,7 +129,8 @@ type S interface {
 	Model
 	Testable
 
-	// Can create a copy.
+	// Can create a copy.  A copy copies everything in the S interface
+	// and nothing more (such as simplifiers).
 	SCopy() S
 }
 
@@ -153,3 +158,39 @@ type Sc interface {
 	// is called all behavior of Sc is undefined.
 	Stop()
 }
+
+// Activatable provides support for recyclable activation literals
+//
+// Caveats: activation clauses must not be empty under unit propagtion
+// at level 0.  The caller should ensure this by construction.
+type Activatable interface {
+	// Activate should be called in place of Add(0) to activate a
+	// clause.  Activate returns the activation literal, which, if assigned
+	// activates the last added clause.
+	//
+	// If the last clause is empty, then Activate panics.  The caller
+	// should only activate non-empty clauses.  Note that in incremental
+	// settings, one may have to verify whether or not a clause is
+	// empty.
+	//
+	// like `Add()`, Activate should only be called at decision level 0.
+	Activate() z.Lit
+
+	// ActivateWith is like Activate but it allows the caller to specify
+	// the activation literal `act`.  The activation literal should
+	// be `pure`, meaning that `act.Not()` does not appear anywhere in
+	// any clause added.  Note that deactivation of literals passed to
+	// ActivateWith causes them to be recycled.
+	ActivateWith(act z.Lit)
+
+	// ActivationLit returns a literal to be used with ActivateWith.
+	// As all other Activation related methods, ActivationLit is
+	// not supported under test scopes.
+	ActivationLit() z.Lit
+
+	// Deactivate deactivates an activation literal as returned by
+	// Activate.
+	//
+	// like `Add()`, Deactivate should only be called at decision level 0.
+	Deactivate(m z.Lit)
+}

internal/xo/active.go

@@ -0,0 +1,121 @@
+package xo
+
+import (
+	"github.com/irifrance/gini/z"
+)
+
+type Active struct {
+	Free     []z.Lit
+	Occs     [][]z.C
+	IsActive []bool
+	Ms       []z.Lit
+}
+
+func newActive(vcap int) *Active {
+	return &Active{
+		Occs:     make([][]z.C, vcap),
+		IsActive: make([]bool, vcap)}
+}
+
+func (a *Active) Lit(s *S) z.Lit {
+	n := len(a.Free)
+	var act z.Lit
+	if n != 0 {
+		act = a.Free[n-1]
+		a.Free = a.Free[:n-1]
+	} else {
+		act = s.Lit()
+	}
+	return act
+}
+
+func (a *Active) ActivateWith(act z.Lit, s *S) {
+	a.IsActive[act.Var()] = true
+	s.Add(act.Not())
+	loc, u := s.Cdb.Add(0)
+	if u != z.LitNull {
+		panic("activated empty clause")
+	}
+	if loc == CInf {
+		panic("activated trivially true clause")
+		return
+	}
+	// add occs
+	ms := a.Ms
+	ms = s.Cdb.Lits(loc, ms)
+	is := a.IsActive
+	for _, m := range ms {
+		mv := m.Var()
+		if !is[mv] {
+			continue
+		}
+		if m.IsPos() {
+			panic("positive act lit")
+		}
+		a.Occs[mv] = append(a.Occs[mv], loc)
+	}
+	a.Ms = ms[:0]
+}
+
+func (a *Active) Deactivate(cdb *Cdb, m z.Lit) {
+	mv := m.Var()
+	m = mv.Pos()
+	sl := a.Occs[mv]
+	a.Occs[mv] = nil
+	cdb.Remove(sl...) // this might trigger CRemap below, so we update occs first.
+	a.Free = append(a.Free, m)
+	a.IsActive[mv] = false
+}
+
+func (a *Active) CRemap(rlm map[z.C]z.C) {
+	if len(rlm) == 0 {
+		return
+	}
+	for i := range a.Occs {
+		sl := a.Occs[i]
+		if len(sl) == 0 {
+			continue
+		}
+		j := 0
+		for _, c := range sl {
+			d, ok := rlm[c]
+			if !ok {
+				sl[j] = c
+				j++
+				continue
+			}
+			if d == CNull {
+				continue
+			}
+			sl[j] = d
+			j++
+		}
+		a.Occs[i] = sl[:j]
+	}
+}
+
+func (a *Active) growToVar(u z.Var) {
+	w := u + 1
+	oc := make([][]z.C, w)
+	copy(oc, a.Occs)
+	a.Occs = oc
+
+	ia := make([]bool, w)
+	copy(ia, a.IsActive)
+	a.IsActive = ia
+}
+
+func (a *Active) Copy() *Active {
+	res := &Active{
+		Free:     make([]z.Lit, len(a.Free), cap(a.Free)),
+		Occs:     make([][]z.C, len(a.Occs), cap(a.Occs)),
+		IsActive: make([]bool, len(a.IsActive), cap(a.IsActive))}
+	copy(res.IsActive, a.IsActive)
+	copy(res.Free, a.Free)
+	for i, asl := range a.Occs {
+		rsl := make([]z.C, len(asl), cap(asl))
+		copy(rsl, asl)
+		res.Occs[i] = rsl
+	}
+	return res
+}