From abd902d58c8144da339c3700f407a4cc7f04cf79 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Aug 2018 18:14:32 -0700 Subject: [PATCH] n/a Signed-off-by: Nikolaj Bjorner --- src/smt/theory_jobscheduler.cpp | 396 ++++++++++++++++++++++++++------ src/smt/theory_jobscheduler.h | 58 ++++- 2 files changed, 372 insertions(+), 82 deletions(-) diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index d2cab8bf8..f12193c2e 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -78,6 +78,18 @@ namespace smt { } final_check_status theory_jobscheduler::final_check_eh() { + + // ensure that each job starts within an avaialable interval. + // ! (end_previous_interval < start(j) < start_of_next_interval) + + bool blocked = false; + for (unsigned r = 0; r < m_resources.size(); ++r) { + if (constrain_resource_energy(r)) { + blocked = true; + } + } + + if (blocked) return FC_CONTINUE; return FC_DONE; } @@ -85,13 +97,199 @@ namespace smt { return false; } - void theory_jobscheduler::propagate() { + literal theory_jobscheduler::mk_literal(expr * e) { + expr_ref _e(e, m); + context& ctx = get_context(); + if (!ctx.e_internalized(e)) { + ctx.internalize(e, false); + } + ctx.mark_as_relevant(ctx.get_enode(e)); + return ctx.get_literal(e); + } + + literal theory_jobscheduler::mk_ge_lit(expr* e, time_t t) { + return mk_literal(mk_ge(e, t)); + } + + expr* theory_jobscheduler::mk_ge(expr* e, time_t t) { + return a.mk_ge(e, a.mk_int(rational(t, rational::ui64()))); + } + + expr* theory_jobscheduler::mk_ge(enode* e, time_t t) { + return mk_ge(e->get_owner(), t); + } + + literal theory_jobscheduler::mk_le_lit(expr* e, time_t t) { + return mk_literal(mk_le(e, t)); + } + + expr* theory_jobscheduler::mk_le(expr* e, time_t t) { + return a.mk_le(e, a.mk_int(rational(t, rational::ui64()))); + } + + literal theory_jobscheduler::mk_le(enode* l, enode* r) { + context& ctx = get_context(); + expr_ref le(a.mk_le(l->get_owner(), r->get_owner()), m); + ctx.get_rewriter()(le); + return mk_literal(le); + } + + expr* theory_jobscheduler::mk_le(enode* e, time_t t) { + return mk_le(e->get_owner(), t); + } + + /** + * iterator of job overlaps. + */ + theory_jobscheduler::job_overlap::job_overlap(vector& starts, vector& ends): + m_starts(starts), m_ends(ends), s_idx(0), e_idx(0) { + job_time::compare cmp; + std::sort(starts.begin(), starts.end(), cmp); + std::sort(ends.begin(), ends.end(), cmp); + } + + bool theory_jobscheduler::job_overlap::next(time_t& start) { + if (s_idx == m_starts.size()) { + return false; + } + while (s_idx < m_starts.size() && m_starts[s_idx].m_time <= start) { + m_jobs.insert(m_starts[s_idx].m_job); + ++s_idx; + } + // remove jobs that end before start. + while (e_idx < m_ends.size() && m_ends[s_idx].m_time < start) { + m_jobs.remove(m_ends[e_idx].m_job); + ++e_idx; + } + // TBD: check logic + if (s_idx < m_starts.size()) { + start = m_starts[s_idx].m_time; + } + return true; + } + + + /** + * r = resource(j) & start(j) >= slb => end(j) >= ect(j, r, slb) + */ + void theory_jobscheduler::propagate_end_time(unsigned j, unsigned r) { + time_t slb = est(j); + time_t clb = ect(j, r, slb); + context& ctx = get_context(); + + if (clb > end(j)) { + job_info const& ji = m_jobs[j]; + literal start_ge_lo = mk_literal(mk_ge(ji.m_start, slb)); + if (ctx.get_assignment(start_ge_lo) != l_true) { + return; + } + enode_pair eq(ji.m_resource, ctx.get_enode(u.mk_resource(r))); + if (eq.first->get_root() != eq.second->get_root()) { + return; + } + + literal end_ge_lo = mk_literal(mk_ge(ji.m_end, clb)); + // Initialization ensures that satisfiable states have completion time below end. + VERIFY(clb <= get_job_resource(j, r).m_end); + region& r = ctx.get_region(); + ctx.assign(end_ge_lo, + ctx.mk_justification( + ext_theory_propagation_justification(get_id(), r, 1, &start_ge_lo, 1, &eq, end_ge_lo, 0, nullptr))); + } + } + + /** + * For time interval [t0, t1] the end-time can be computed as a function + * of start time based on reource load availability. + * + * r = resource(j) & t1 >= start(j) >= t0 => end(j) = start(j) + ect(j, r, t0) - t0 + */ + void theory_jobscheduler::propagate_end_time_interval(unsigned j, unsigned r) { + // TBD + // establish maximal intervals around start, such that end time is a linear function of start. + } + + void theory_jobscheduler::propagate_resource_energy(unsigned r) { } + + /** + * Ensure that job overlaps don't exceed available energy + */ + bool theory_jobscheduler::constrain_resource_energy(unsigned r) { + bool blocked = false; + vector starts, ends; + res_info const& ri = m_resources[r]; + for (unsigned j : ri.m_jobs) { + if (resource(j) == r) { + starts.push_back(job_time(j, start(j))); + ends.push_back(job_time(j, end(j))); + } + } + job_overlap overlap(starts, ends); + time_t start = 0; + while (overlap.next(start)) { + unsigned cap = 0; + auto const& jobs = overlap.jobs(); + for (auto j : jobs) { + cap += get_job_resource(j, r).m_loadpct; + if (cap > 100) { + block_job_overlap(r, jobs, j); + blocked = true; + goto try_next_overlap; + } + } + try_next_overlap: + ; + } + return blocked; + } + + void theory_jobscheduler::block_job_overlap(unsigned r, uint_set const& jobs, unsigned last_job) { + // + // block the following case: + // each job is assigned to r. + // max { start(j) | j0..last_job } <= min { end(j) | j0..last_job } + // joint capacity of jobs exceeds availability of resource. + // + time_t max_start = 0; + unsigned max_j = last_job; + for (auto j : jobs) { + if (max_start < start(j)) { + max_start = start(j); + max_j = j; + } + if (j == last_job) break; + } + literal_vector lits; + for (auto j : jobs) { + // create literals for: + // resource(j) == r + // m_jobs[j].m_start <= m_jobs[max_j].m_start; + // m_jobs[max_j].m_start <= m_jobs[j].m_end; + lits.push_back(~mk_eq(u.mk_job2resource(j), u.mk_resource(r), false)); + lits.push_back(~mk_le(m_jobs[j].m_start, m_jobs[max_j].m_start)); + lits.push_back(~mk_le(m_jobs[max_j].m_start, m_jobs[max_j].m_end)); + if (j == last_job) break; + } + context& ctx = get_context(); + ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr); + } + + void theory_jobscheduler::propagate() { + for (unsigned j = 0; j < m_jobs.size(); ++j) { + job_info const& ji = m_jobs[j]; + unsigned r = resource(j); + propagate_end_time(j, r); + propagate_end_time_interval(j, r); + } + for (unsigned r = 0; r < m_resources.size(); ++r) { + // TBD: check energy constraints on resources. + } + } theory_jobscheduler::theory_jobscheduler(ast_manager& m): theory(m.get_family_id("jobshop")), m(m), u(m), a(m) { - } std::ostream& theory_jobscheduler::display(std::ostream & out, job_resource const& jr) const { @@ -147,30 +345,37 @@ namespace smt { } time_t theory_jobscheduler::est(unsigned j) { + NOT_IMPLEMENTED_YET(); return 0; } time_t theory_jobscheduler::lst(unsigned j) { + NOT_IMPLEMENTED_YET(); return 0; } time_t theory_jobscheduler::ect(unsigned j) { + NOT_IMPLEMENTED_YET(); return 0; } time_t theory_jobscheduler::lct(unsigned j) { + NOT_IMPLEMENTED_YET(); return 0; } time_t theory_jobscheduler::start(unsigned j) { + NOT_IMPLEMENTED_YET(); return 0; } time_t theory_jobscheduler::end(unsigned j) { + NOT_IMPLEMENTED_YET(); return 0; } unsigned theory_jobscheduler::resource(unsigned j) { + NOT_IMPLEMENTED_YET(); return 0; } @@ -191,7 +396,7 @@ namespace smt { void theory_jobscheduler::add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end) { SASSERT(get_context().at_base_level()); - SASSERT(start < end); + SASSERT(start <= end); m_resources.reserve(r + 1); m_resources[r].m_available.push_back(res_available(max_loadpct, start, end)); } @@ -215,16 +420,27 @@ namespace smt { throw default_exception("every job should be associated with at least one resource"); } // resource(j) = r => end(j) <= end(j, r) + // resource(j) = r => start(j) <= lst(j, r, end(j, r)) for (job_resource const& jr : ji.m_resources) { - app_ref res(u.mk_resource(jr.m_resource_id), m); + unsigned r = jr.m_resource_id; + app_ref res(u.mk_resource(r), m); expr_ref eq(m.mk_eq(job, res), m); - expr_ref imp(m.mk_implies(eq, a.mk_le(ji.m_start->get_owner(), a.mk_int(rational(jr.m_end, rational::ui64())))), m); - ctx.assert_expr(imp); + expr_ref imp(m.mk_implies(eq, mk_le(ji.m_end, jr.m_end)), m); + ctx.assert_expr(imp); + imp = m.mk_implies(eq, mk_le(ji.m_start, lst(j, r))); + ctx.assert_expr(imp); disj.push_back(eq); } // resource(j) = r1 || ... || resource(j) = r_n expr_ref fml = mk_or(disj); ctx.assert_expr(fml); + + // start(j) >= 0 + fml = mk_ge(ji.m_start, 0); + ctx.assert_expr(fml); + + // end(j) <= time_t::max + // is implied by resource(j) = r => end(j) <= end(j, r) } for (unsigned r = 0; r < m_resources.size(); ++r) { vector& available = m_resources[r].m_available; @@ -254,59 +470,24 @@ namespace smt { unsigned r = resource(j); start_times[r].push_back(job_time(j, start(j))); end_times[r].push_back(job_time(j, end(j))); - time_t cap = capacity_used(j, r, start(j), end(j)); - job_resource const& jr = get_job_resource(j, r); - if (jr.m_capacity > cap) { + if (ect(j, r, start(j)) > end(j)) { throw default_exception("job not assigned full capacity"); } } for (unsigned r = 0; r < m_resources.size(); ++r) { - unsigned load_pct = 0; - unsigned idx; - time_t next = 0, start = 0; - // order jobs running on r by start, end-time intervals // then consume ordered list to find jobs in scope. - vector& starts = start_times[r]; - vector& ends = end_times[r]; - job_time::compare cmp; - std::sort(starts.begin(), starts.end(), cmp); - std::sort(ends.begin(), ends.end(), cmp); - unsigned s_idx = 0, e_idx = 0; - - uint_set jobs; // set of jobs currently in scope. - while (resource_available(r, start, load_pct, next, idx)) { - if (load_pct == 0) { - start = next + 1; - continue; - } - // add jobs that begin at or before start. - while (s_idx < starts.size() && starts[s_idx].m_time <= start) { - jobs.insert(starts[s_idx].m_job); - ++s_idx; - } - // remove jobs that end before start. - while (e_idx < ends.size() && ends[s_idx].m_time < start) { - jobs.remove(ends[e_idx].m_job); - ++e_idx; - } - + time_t start = 0; + job_overlap overlap(start_times[r], end_times[r]); + while (overlap.next(start)) { // check that sum of job loads does not exceed 100% unsigned cap = 0; - for (auto j : jobs) { + for (auto j : overlap.jobs()) { cap += get_job_resource(j, r).m_loadpct; } if (cap > 100) { throw default_exception("capacity on resource exceeded"); } - if (s_idx < starts.size()) { - // start time of the next unprocessed job. - start = starts[s_idx].m_time; - } - else { - // done checking. - break; - } } } } @@ -316,14 +497,12 @@ namespace smt { return ji.m_resources[ji.m_resource2index[r]]; } - bool theory_jobscheduler::resource_available(unsigned r, time_t t, unsigned& load_pct, time_t& end, unsigned& idx) { + bool theory_jobscheduler::resource_available(unsigned r, time_t t, unsigned& idx) { vector& available = m_resources[r].m_available; unsigned lo = 0, hi = available.size(), mid = hi / 2; while (lo < hi) { res_available const& ra = available[mid]; if (ra.m_start <= t && t <= ra.m_end) { - end = ra.m_end; - load_pct = ra.m_loadpct; idx = mid; return true; } @@ -342,35 +521,108 @@ namespace smt { return false; } + /** - * compute the capacity used by job j on resource r between start and end. - * The resource r partitions time intervals into segments where a fraction of - * the full capacity of the resource is available. The resource can use up to the - * available fraction. - */ - time_t theory_jobscheduler::capacity_used(unsigned j, unsigned r, time_t start, time_t end) { - time_t cap = 0; - unsigned j_load_pct = get_job_resource(j, r).m_loadpct; + * compute earliest completion time for job j on resource r starting at time start. + */ + time_t theory_jobscheduler::ect(unsigned j, unsigned r, time_t start) { + job_resource const& jr = get_job_resource(j, r); vector& available = m_resources[r].m_available; - unsigned load_pct = 0; - time_t next = 0; + + unsigned j_load_pct = jr.m_loadpct; + time_t cap = jr.m_capacity; unsigned idx = 0; - if (!resource_available(r, start, load_pct, next, idx)) { - return cap; + if (!resource_available(r, start, idx)) { + return std::numeric_limits::max(); } - while (start < end) { - next = std::min(end, next); - SASSERT(start < next); - cap += (std::min(j_load_pct, load_pct) / j_load_pct) * (next - start - 1); - ++idx; - if (idx == available.size()) { - break; + SASSERT(cap > 0); + + for (; idx < available.size(); ++idx) { + start = std::max(start, available[idx].m_start); + time_t end = available[idx].m_end; + unsigned load_pct = available[idx].m_loadpct; + time_t delta = solve_for_capacity(load_pct, j_load_pct, start, end); + if (delta > cap) { + // + // solve for end: + // cap = load * (end - start + 1) + // <=> + // cap / load = (end - start + 1) + // <=> + // end = cap / load + start - 1 + // + end = solve_for_end(load_pct, j_load_pct, start, cap); + cap = 0; + } + else { + cap -= delta; + } + if (cap == 0) { + return end; } - start = available[idx].m_start; - next = available[idx].m_end; - load_pct = available[idx].m_loadpct; } - return cap; + return std::numeric_limits::max(); + } + + time_t theory_jobscheduler::solve_for_end(unsigned load_pct, unsigned job_load_pct, time_t start, time_t cap) { + SASSERT(load_pct > 0); + SASSERT(job_load_pct > 0); + // cap = (load / job_load_pct) * (start - end + 1) + // <=> + // start - end + 1 = (cap * job_load_pct) / load + // <=> + // end = start + 1 - (cap * job_load_pct) / load + // <=> + // end = (load * (start + 1) - cap * job_load_pct) / load + unsigned load = std::min(load_pct, job_load_pct); + return (load * (start + 1) - cap * job_load_pct) / load; + } + + time_t theory_jobscheduler::solve_for_start(unsigned load_pct, unsigned job_load_pct, time_t end, time_t cap) { + SASSERT(load_pct > 0); + SASSERT(job_load_pct > 0); + // cap = (load / job_load_pct) * (start - end + 1) + // <=> + // start - end + 1 = (cap * job_load_pct) / load + // <=> + // start = (cap * job_load_pct) / load + end - 1 + // <=> + // start = (load * (end - 1) + cap * job_load_pct) / load + unsigned load = std::min(load_pct, job_load_pct); + return (load * (end - 1) + cap * job_load_pct) / load; + } + + time_t theory_jobscheduler::solve_for_capacity(unsigned load_pct, unsigned job_load_pct, time_t start, time_t end) { + SASSERT(job_load_pct > 0); + unsigned load = std::min(load_pct, job_load_pct); + return (load * (end - start + 1)) / job_load_pct; + } + + /** + * Compute last start time for job on resource r. + */ + time_t theory_jobscheduler::lst(unsigned j, unsigned r) { + job_resource const& jr = get_job_resource(j, r); + vector& available = m_resources[r].m_available; + unsigned j_load_pct = jr.m_loadpct; + time_t cap = jr.m_capacity; + for (unsigned idx = available.size(); idx-- > 0; ) { + time_t start = available[idx].m_start; + time_t end = available[idx].m_end; + unsigned load_pct = available[idx].m_loadpct; + time_t delta = solve_for_capacity(load_pct, j_load_pct, start, end); + if (delta > cap) { + start = solve_for_start(load_pct, j_load_pct, start, cap); + cap = 0; + } + else { + cap -= delta; + } + if (cap == 0) { + return start; + } + } + throw default_exception("there is insufficient capacity on the resource to run the job"); } }; diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h index f10b72d81..369cc1955 100644 --- a/src/smt/theory_jobscheduler.h +++ b/src/smt/theory_jobscheduler.h @@ -20,9 +20,10 @@ Revision History: --*/ #pragma once; -#include "smt/smt_theory.h" +#include "util/uint_set.h" #include "ast/jobshop_decl_plugin.h" #include "ast/arith_decl_plugin.h" +#include "smt/smt_theory.h" namespace smt { @@ -74,13 +75,12 @@ namespace smt { return ra1.m_start < ra2.m_start; } }; - }; struct res_info { unsigned_vector m_jobs; // jobs allocated to run on resource vector m_available; // time intervals where resource is available - time_t m_end; // can't run after + time_t m_end; // can't run after res_info(): m_end(std::numeric_limits::max()) {} }; @@ -131,10 +131,15 @@ namespace smt { bool get_value(enode * n, expr_ref & r) override; - theory * mk_fresh(context * new_ctx) override; // { return alloc(theory_jobscheduler, new_ctx->get_manager()); } + theory * mk_fresh(context * new_ctx) override; public: - // assignments: + // set up job/resource global constraints + void add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, time_t end); + void add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end); + void add_done(); + + // assignments time_t est(unsigned j); // earliest start time of job j time_t lst(unsigned j); // last start time time_t ect(unsigned j); // earliest completion time @@ -142,19 +147,52 @@ namespace smt { time_t start(unsigned j); // start time of job j time_t end(unsigned j); // end time of job j unsigned resource(unsigned j); // resource of job j + + // derived bounds + time_t ect(unsigned j, unsigned r, time_t start); + time_t lst(unsigned j, unsigned r); - // set up model - void add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, time_t end); - void add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end); - void add_done(); + time_t solve_for_start(unsigned load_pct, unsigned job_load_pct, time_t end, time_t cap); + time_t solve_for_end(unsigned load_pct, unsigned job_load_pct, time_t start, time_t cap); + time_t solve_for_capacity(unsigned load_pct, unsigned job_load_pct, time_t start, time_t end); // validate assignment void validate_assignment(); - bool resource_available(unsigned r, time_t t, unsigned& load_pct, time_t& end, unsigned& idx); // load available on resource r at time t. + bool resource_available(unsigned r, time_t t, unsigned& idx); // load available on resource r at time t. time_t capacity_used(unsigned j, unsigned r, time_t start, time_t end); // capacity used between start and end job_resource const& get_job_resource(unsigned j, unsigned r) const; + // propagation + void propagate_end_time(unsigned j, unsigned r); + void propagate_end_time_interval(unsigned j, unsigned r); + void propagate_resource_energy(unsigned r); + + // final check constraints + bool constrain_resource_energy(unsigned r); + + void block_job_overlap(unsigned r, uint_set const& jobs, unsigned last_job); + + class job_overlap { + vector & m_starts, &m_ends; + unsigned s_idx, e_idx; // index into starts/ends + uint_set m_jobs; + public: + job_overlap(vector& starts, vector& ends); + bool next(time_t& start); + uint_set const& jobs() const { return m_jobs; } + }; + + // term builders + literal mk_ge_lit(expr* e, time_t t); + expr* mk_ge(expr* e, time_t t); + expr* mk_ge(enode* e, time_t t); + literal mk_le_lit(expr* e, time_t t); + expr* mk_le(expr* e, time_t t); + expr* mk_le(enode* e, time_t t); + literal mk_le(enode* l, enode* r); + literal mk_literal(expr* e); + std::ostream& display(std::ostream & out, res_info const& r) const; std::ostream& display(std::ostream & out, res_available const& r) const; std::ostream& display(std::ostream & out, job_info const& r) const;