Knowledge compilation (KC) transforms Boolean formulae into alternative representations that allow for more efficient reasoning. However, KC still fails to scale on some Boolean formulae, including some representing the variability of large configurable systems (e.g., OS kernels, automotive product lines, etc.), for which these analyses are paramount. We hypothesise that a divide-and-conquer strategy to knowledge compilation may push its scalability further. Concretely, our DivKC algorithms decompose a large Boolean formula into two smaller ones, which we can easily compile into the d-DNNF form. When evaluated on a diversified benchmark of 4,656 formulae, DivKC compiles 114 formulae out of the 672 formulae that were previously out of reach for the D4 state-of-the-art d-DNNF compiler. We then show how to leverage DivKC decompositions to build an approximate model counter and a uniform random sampler.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

DivKC: A Divide-and-Conquer Approach to Knowledge Compilation

  • Olivier Zeyen,
  • Karim Tit,
  • Maxime Cordy,
  • Gilles Perrouin

摘要

Knowledge compilation (KC) transforms Boolean formulae into alternative representations that allow for more efficient reasoning. However, KC still fails to scale on some Boolean formulae, including some representing the variability of large configurable systems (e.g., OS kernels, automotive product lines, etc.), for which these analyses are paramount. We hypothesise that a divide-and-conquer strategy to knowledge compilation may push its scalability further. Concretely, our DivKC algorithms decompose a large Boolean formula into two smaller ones, which we can easily compile into the d-DNNF form. When evaluated on a diversified benchmark of 4,656 formulae, DivKC compiles 114 formulae out of the 672 formulae that were previously out of reach for the D4 state-of-the-art d-DNNF compiler. We then show how to leverage DivKC decompositions to build an approximate model counter and a uniform random sampler.