|
37 | 37 | #include <map> |
38 | 38 | #include <memory> |
39 | 39 | #include <set> |
| 40 | +#include <tuple> |
40 | 41 | #include <unordered_map> |
41 | 42 | #include <vector> |
42 | 43 |
|
@@ -393,6 +394,118 @@ State join(const QueryCtx &q, const State &s1, const State &s2) |
393 | 394 | // ToCS 2020), run over the joint graph (element + gate vertices). |
394 | 395 | // --------------------------------------------------------------------- |
395 | 396 |
|
| 397 | +/** |
| 398 | + * @brief Number of *essential* (enumerating) variables of a disjunct. |
| 399 | + * |
| 400 | + * The exponential parameter of the DP is not every join variable but only |
| 401 | + * those that must be enumerated: a variable functionally determined by others |
| 402 | + * does not multiply the partial-homomorphism state. This returns the size of |
| 403 | + * a minimum set @c S of join variables whose FD closure covers all of them |
| 404 | + * (the @c e of the @f$2^{O(k^e)}@f$ bound). |
| 405 | + * |
| 406 | + * The FDs are **mined from the gathered tuples** (@p enc.facts, already |
| 407 | + * post-selection): a column set determines a column when no two tuples of the |
| 408 | + * relation agree on the former and differ on the latter. This captures any |
| 409 | + * declared key (which necessarily holds on the data) along with FDs incidental |
| 410 | + * to this instance, and needs no catalog lookup. The closure is sound for the |
| 411 | + * instance being compiled: if the FD holds on these tuples the variable is |
| 412 | + * genuinely fixed in every world of this computation. |
| 413 | + * |
| 414 | + * The minimum-cover search is @f$2^{|V|}@f$ in the join-variable count @c |V|; |
| 415 | + * above @c MAX_FD_VARS it is skipped and the full count returned (a sound upper |
| 416 | + * bound), the design target being a handful of enumerating variables. |
| 417 | + */ |
| 418 | +unsigned essentialVarCount(const CQ &cq, const std::vector<bool> &appears, |
| 419 | + const JointEncoding &enc) |
| 420 | +{ |
| 421 | + std::vector<unsigned> V; // the join variables |
| 422 | + for (unsigned v = 0; v < cq.n_vars; ++v) |
| 423 | + if (appears[v]) |
| 424 | + V.push_back(v); |
| 425 | + const unsigned nV = static_cast<unsigned>(V.size()); |
| 426 | + static constexpr unsigned MAX_FD_VARS = 12; |
| 427 | + if (nV <= 1 || nV > MAX_FD_VARS) |
| 428 | + return nV; |
| 429 | + |
| 430 | + // Tuples per (relation, arity), as pointers into enc.facts. |
| 431 | + std::map<std::pair<unsigned, std::size_t>, |
| 432 | + std::vector<const std::vector<unsigned long> *> > byrel; |
| 433 | + for (const Fact &f : enc.facts) |
| 434 | + byrel[{f.relation_id, f.elements.size()}].push_back(&f.elements); |
| 435 | + |
| 436 | + // Memoised data FD: do the columns in bitmask @c known determine column @c c |
| 437 | + // in the tuples of (@c rel, @c arity)? |
| 438 | + std::map<std::tuple<unsigned, std::size_t, std::uint64_t, unsigned>, bool> memo; |
| 439 | + auto dataFD = [&](unsigned rel, std::size_t arity, |
| 440 | + std::uint64_t known, unsigned c) -> bool { |
| 441 | + auto key = std::make_tuple(rel, arity, known, c); |
| 442 | + auto it = memo.find(key); |
| 443 | + if (it != memo.end()) |
| 444 | + return it->second; |
| 445 | + bool holds = true; |
| 446 | + auto rit = byrel.find({rel, arity}); |
| 447 | + if (rit != byrel.end()) { |
| 448 | + std::map<std::vector<unsigned long>, unsigned long> grp; |
| 449 | + for (const std::vector<unsigned long> *t : rit->second) { |
| 450 | + std::vector<unsigned long> kv; |
| 451 | + for (std::size_t p = 0; p < arity; ++p) |
| 452 | + if (known & (std::uint64_t{1} << p)) |
| 453 | + kv.push_back((*t)[p]); |
| 454 | + auto git = grp.find(kv); |
| 455 | + if (git == grp.end()) |
| 456 | + grp.emplace(std::move(kv), (*t)[c]); |
| 457 | + else if (git->second != (*t)[c]) { |
| 458 | + holds = false; |
| 459 | + break; |
| 460 | + } |
| 461 | + } |
| 462 | + } |
| 463 | + memo[key] = holds; |
| 464 | + return holds; |
| 465 | + }; |
| 466 | + |
| 467 | + std::unordered_map<unsigned, unsigned> bitOf; |
| 468 | + for (unsigned i = 0; i < nV; ++i) |
| 469 | + bitOf[V[i]] = i; |
| 470 | + const std::uint32_t fullMask = (std::uint32_t{1} << nV) - 1; |
| 471 | + |
| 472 | + // FD closure of a determined set (bitmask over @c V). |
| 473 | + auto closure = [&](std::uint32_t det) -> std::uint32_t { |
| 474 | + bool changed = true; |
| 475 | + while (changed) { |
| 476 | + changed = false; |
| 477 | + for (const Atom &a : cq.atoms) { |
| 478 | + const std::size_t arity = a.vars.size(); |
| 479 | + std::uint64_t knownPos = 0; |
| 480 | + for (std::size_t p = 0; p < arity; ++p) |
| 481 | + if (det & (std::uint32_t{1} << bitOf[a.vars[p]])) |
| 482 | + knownPos |= (std::uint64_t{1} << p); |
| 483 | + for (std::size_t p = 0; p < arity; ++p) { |
| 484 | + if (knownPos & (std::uint64_t{1} << p)) |
| 485 | + continue; // this column already determined |
| 486 | + const unsigned bit = bitOf[a.vars[p]]; |
| 487 | + if (dataFD(a.relation_id, arity, knownPos, static_cast<unsigned>(p))) { |
| 488 | + det |= (std::uint32_t{1} << bit); |
| 489 | + knownPos |= (std::uint64_t{1} << p); |
| 490 | + changed = true; |
| 491 | + } |
| 492 | + } |
| 493 | + } |
| 494 | + } |
| 495 | + return det; |
| 496 | + }; |
| 497 | + |
| 498 | + unsigned best = nV; |
| 499 | + for (std::uint32_t s = 0; s <= fullMask; ++s) { |
| 500 | + const unsigned pc = static_cast<unsigned>(__builtin_popcount(s)); |
| 501 | + if (pc >= best) |
| 502 | + continue; // cannot beat the current minimum |
| 503 | + if (closure(s) == fullMask) |
| 504 | + best = pc; |
| 505 | + } |
| 506 | + return best; |
| 507 | +} |
| 508 | + |
396 | 509 | /** @brief Build the per-disjunct query context and the query stats. */ |
397 | 510 | void buildQueryCtx(const UCQ &ucq, const JointEncoding &enc, |
398 | 511 | QueryCtx &q, UCQJointCompiler::Stats &stats) |
@@ -420,14 +533,10 @@ void buildQueryCtx(const UCQ &ucq, const JointEncoding &enc, |
420 | 533 | di.atoms_of_var[v] |= (std::uint64_t{1} << ai); |
421 | 534 | appears[v] = true; |
422 | 535 | } |
423 | | - // The exponential parameter is the number of variables that occur in |
424 | | - // an atom (the join variables); a variable in no atom never enters a |
425 | | - // code. Key/FD determination (a later milestone) shrinks this. |
426 | | - unsigned ne = 0; |
427 | | - for (unsigned v = 0; v < di.n_vars; ++v) |
428 | | - if (appears[v]) |
429 | | - ++ne; |
430 | | - stats.n_enumerating[d] = ne; |
| 536 | + // The exponential parameter is the number of *essential* join variables: |
| 537 | + // those that must be enumerated once the ones functionally determined by |
| 538 | + // others (via FDs mined from the gathered data) are removed. |
| 539 | + stats.n_enumerating[d] = essentialVarCount(cq, appears, enc); |
431 | 540 | } |
432 | 541 | stats.data_treewidth_lb = enc.data_treewidth_lb; |
433 | 542 | stats.circuit_treewidth_lb = enc.circuit_treewidth_lb; |
|
0 commit comments