Counting the models of a propositional formula is an important problem: for example, it serves as the backbone of probabilistic inference by weighted model counting. A key algorithmic insight is component caching (CC), in which disjoint components of a formula, generated dynamically during a DPLL search, are cached so that they only have to be solved once. In the recent years, driven by SMT technology and probabilistic inference in hybrid domains, there is an increasing interest in counting the models of linear arithmetic sentences. To date, however, solvers for these are block-clause implementations, which are nonviable on large problem instances. In this paper, as a first step in extending CC to hybrid domains, we show how propositional CC systems can be leveraged when limited to piecewise polynomial densities. Our experiments demonstrate a large gap in performance when compared to existing approaches based on a variety of block-clause strategies.
|Title of host publication||Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA.|
|Number of pages||7|
|Publication status||Published - 2016|
|Event||Thirtieth AAAI Conference on Artificial Intelligence - Phoenix, United States|
Duration: 12 Feb 2016 → 17 Feb 2016
|Conference||Thirtieth AAAI Conference on Artificial Intelligence|
|Period||12/02/16 → 17/02/16|