Merge pull request #12 from irifrance/m

Incremental Performance Improvements

gen/rands.go

@@ -102,6 +102,13 @@ func (r *randS) Solve() int {
 	defer r.unlock()
 	return r.solve()
 }
+
+func (r *randS) Try(dur time.Duration) int {
+	r.lock()
+	defer r.unlock()
+	return r.solve()
+}
+
 func (r *randS) solve() int {
 	r.ms = r.ms[:0]
 	ns := r.dur.Nanoseconds()

gini.go

@@ -5,6 +5,7 @@ package gini
 
 import (
 	"io"
+	"time"
 
 	"github.com/irifrance/gini/dimacs"
 	"github.com/irifrance/gini/inter"
@@ -124,6 +125,14 @@ func (g *Gini) Solve() int {
 	return res
 }
 
+// Try solves with a timeout.  Try returns
+//  1  if sat
+//  -1 if unsat
+//  0  if timeout
+func (g *Gini) Try(dur time.Duration) int {
+	return g.xo.Try(dur)
+}
+
 // GoSolve provides a connection to a single background
 // solving goroutine, a goroutine which calls Solve()
 func (g *Gini) GoSolve() inter.Solve {

inter/s.go

@@ -3,20 +3,25 @@
 
 package inter
 
-import "github.com/irifrance/gini/z"
+import (
+	"time"
+
+	"github.com/irifrance/gini/z"
+)
 
 // Interface Solveable encapsulates a decision
 // procedure which may run for a long time.
 //
-// Solve returns
+// Solve/Try returns
 //
 //  1  If the problem is SAT
-//  0  If the problem is undetermined
+//  0  If the problem is undetermined (Try only)
 //  -1 If the problem is UNSAT
 //
 // These error codes are used throughout gini.
 type Solvable interface {
 	Solve() int
+	Try(dur time.Duration) int
 }
 
 // Interface GoSolvable encapsulates a handle

internal/xo/cdb.go

@@ -24,7 +24,8 @@ type Cdb struct {
 	Added   []z.C
 	Learnts []z.C
 
-	Tracer Tracer
+	Tracer     Tracer
+	checkModel bool
 
 	// for multi-scheduling gc frequency
 	gc *Cgc
@@ -46,15 +47,16 @@ func NewCdb(v *Vars, capHint int) *Cdb {
 		capHint = 3
 	}
 	clss := &Cdb{
-		Vars:    v,
-		CDat:    *NewCDat(capHint * 5),
-		AddLits: make([]z.Lit, 0, 24),
-		AddVals: make([]int8, v.Top),
-		Bot:     CNull,
-		Added:   make([]z.C, 0, capHint/3),
-		Learnts: make([]z.C, 0, capHint-capHint/3),
-		Tracer:  nil,
-		gc:      NewCgc()}
+		Vars:       v,
+		CDat:       *NewCDat(capHint * 5),
+		AddLits:    make([]z.Lit, 0, 24),
+		AddVals:    make([]int8, v.Top),
+		Bot:        CNull,
+		Added:      make([]z.C, 0, capHint/3),
+		Learnts:    make([]z.C, 0, capHint-capHint/3),
+		Tracer:     nil,
+		gc:         NewCgc(),
+		checkModel: true}
 	return clss
 }
 
@@ -409,6 +411,9 @@ func (c *Cdb) CheckWatches() []error {
 
 // by default, called when sat as a sanity check.
 func (c *Cdb) CheckModel() []error {
+	if !c.checkModel {
+		return nil
+	}
 	if c.Active != nil {
 		// deactivations and simplificaations remove Added clauses, which are unlinked
 		// until sufficiently large to compact.  compaction
@@ -453,6 +458,7 @@ func (c *Cdb) CopyWith(ov *Vars) *Cdb {
 	copy(other.Learnts, c.Learnts)
 	c.CDat.CopyTo(&other.CDat)
 	other.gc = c.gc.Copy()
+	other.checkModel = c.checkModel
 	return other
 }
 

internal/xo/phases.go

@@ -0,0 +1,43 @@
+package xo
+
+import "github.com/irifrance/gini/z"
+
+type phases z.Var
+
+func (p phases) init(s *S) phases {
+	if s.Vars.Max == z.Var(p) {
+		return p
+	}
+	M := s.Vars.Max
+	N := 2*M + 2
+	counts := make([]uint64, N)
+	L := uint64(16)
+	D := s.Cdb.CDat.D
+	for _, p := range s.Cdb.Added {
+		hd := Chd(D[p-1])
+		sz := uint64(hd.Size())
+		if sz >= L {
+			continue
+		}
+		var m z.Lit
+		q := p
+		for uint32(q-p) < uint32(sz) {
+			m = D[q]
+			if m == z.LitNull {
+				break
+			}
+			counts[m] += 1 << (L - sz)
+			q++
+		}
+	}
+	cache := s.Guess.cache
+	for i := z.Var(1); i <= M; i++ {
+		m, n := i.Pos(), i.Neg()
+		if counts[m] > counts[n] {
+			cache[i] = 1
+		} else {
+			cache[i] = -1
+		}
+	}
+	return phases(M)
+}

internal/xo/s.go

@@ -9,6 +9,7 @@ import (
 	"log"
 	"runtime"
 	"sync"
+	"time"
 
 	"github.com/irifrance/gini/dimacs"
 	"github.com/irifrance/gini/inter"
@@ -49,10 +50,13 @@ type S struct {
 	assumptLevel int
 	assumes      []z.Lit // only last set of requested assumptions before solve/test.
 	failed       []z.Lit
+	phases       phases
 
 	// Control
 	control          *Ctl
 	restartStopwatch int
+	startTime        time.Time
+	deadline         time.Time // synchronous (no pause)
 
 	// Stats (each object has its own, read by ReadStats())
 	stRestarts  int64
@@ -123,6 +127,8 @@ func NewSCdb(cdb *Cdb) *S {
 		return st
 	}
 	s.control.xo = s
+	s.startTime = time.Now()
+	s.deadline = s.startTime
 	return s
 }
 
@@ -139,6 +145,7 @@ func (s *S) Copy() *S {
 		other.Active = s.Active.Copy()
 		other.Cdb.Active = other.Active
 	}
+	other.phases = s.phases
 	luby := NewLuby()
 	*luby = *(s.luby)
 	other.luby = luby
@@ -158,6 +165,8 @@ func (s *S) Copy() *S {
 		other.ReadStats(st)
 		return st
 	}
+	other.startTime = s.startTime
+	other.deadline = s.deadline
 	return other
 }
 
@@ -180,6 +189,12 @@ func (s *S) String() string {
 	return fmt.Sprintf("<xo@%d>", s.Trail.Level)
 }
 
+func (s *S) Try(dur time.Duration) int {
+	s.startTime = time.Now()
+	s.deadline = s.startTime.Add(dur)
+	return s.Solve()
+}
+
 // Method Solve solves the problem added to the solver under
 // assumptions specified by Assume.
 //
@@ -237,6 +252,9 @@ func (s *S) Solve() int {
 			nxtTick += PropTick
 			tick++
 			if tick%CancelTicks == 0 {
+				if s.deadline != s.startTime && time.Until(s.deadline) <= 0 {
+					return 0
+				}
 				if !s.control.Tick() {
 					s.stEnded++
 					trail.Back(s.endTestLevel)
@@ -258,6 +276,9 @@ func (s *S) Solve() int {
 		m := guess.Guess(vars.Vals)
 		if m == z.LitNull {
 			errs := cdb.CheckModel()
+			if s.Active != nil {
+				s.Cdb.checkModel = false
+			}
 			if len(errs) != 0 {
 				for _, e := range errs {
 					log.Println(e)
@@ -266,7 +287,6 @@ func (s *S) Solve() int {
 				log.Println(s.Trail)
 
 				log.Printf("%p %p internal error: sat model\n", s, s.control)
-
 			}
 			s.stSat++
 			// don't do this, we store the model returned to the user
@@ -484,6 +504,7 @@ func (s *S) Add(m z.Lit) {
 	s.ensureLitCap(m)
 	if m == z.LitNull {
 		s.ensure0()
+		s.Cdb.checkModel = true
 	}
 	loc, u := s.Cdb.Add(m)
 	if u != z.LitNull {
@@ -610,7 +631,7 @@ func (s *S) solveInit() int {
 	//log.Printf("%s\n", s.Vars)
 
 	// initialize phase
-	s.phaseInit()
+	s.phases = s.phases.init(s)
 	return 0
 }
 
@@ -685,42 +706,6 @@ func (s *S) makeAssumptions() int {
 	return 0
 }
 
-// TBD: make this understand solved clauses
-// and assumptions.
-func (s *S) phaseInit() {
-	M := s.Vars.Max
-	N := 2*M + 2
-	L := uint64(16)
-	counts := make([]uint64, N, N)
-	D := s.Cdb.CDat.D
-	for _, p := range s.Cdb.Added {
-		hd := Chd(D[p-1])
-		sz := uint64(hd.Size())
-		if sz >= L {
-			continue
-		}
-		var m z.Lit
-		q := p
-		for uint32(q-p) < uint32(sz) {
-			m = D[q]
-			if m == z.LitNull {
-				break
-			}
-			counts[m] += 1 << (L - sz)
-			q++
-		}
-	}
-	cache := s.Guess.cache
-	for i := z.Var(1); i <= M; i++ {
-		m, n := i.Pos(), i.Neg()
-		if counts[m] > counts[n] {
-			cache[i] = 1
-		} else {
-			cache[i] = -1
-		}
-	}
-}
-
 func (s *S) final(ms []z.Lit) {
 	marks := make([]bool, s.Vars.Max+1)
 	for _, m := range ms {

sv.go

@@ -4,6 +4,8 @@
 package gini
 
 import (
+	"time"
+
 	"github.com/irifrance/gini/inter"
 	"github.com/irifrance/gini/z"
 )
@@ -67,6 +69,10 @@ func (w *svWrap) Solve() int {
 	return w.S.Solve()
 }
 
+func (w *svWrap) Try(dur time.Duration) int {
+	return w.S.Try(dur)
+}
+
 func (w *svWrap) GoSolve() inter.Solve {
 	return w.S.GoSolve()
 }