diff --git a/gen/rands.go b/gen/rands.go index 9737e0e..3666715 100644 --- a/gen/rands.go +++ b/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() diff --git a/gini.go b/gini.go index 09c58ac..c9b70ab 100644 --- a/gini.go +++ b/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 { diff --git a/inter/s.go b/inter/s.go index 897ee9c..2afa962 100644 --- a/inter/s.go +++ b/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 diff --git a/internal/xo/cdb.go b/internal/xo/cdb.go index fbfd2ca..5853e9d 100644 --- a/internal/xo/cdb.go +++ b/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 } diff --git a/internal/xo/phases.go b/internal/xo/phases.go new file mode 100644 index 0000000..295fbbe --- /dev/null +++ b/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) +} diff --git a/internal/xo/s.go b/internal/xo/s.go index f6262e7..5ee39d8 100644 --- a/internal/xo/s.go +++ b/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("", 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 { diff --git a/sv.go b/sv.go index 8e5a1d3..58c6fc5 100644 --- a/sv.go +++ b/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() }