Implementation of Tetris as a Model Counter.
arXiv: Data Structures and Algorithms(2017)
摘要
Solving SharpSAT problems is an important area of work. In this paper, we discuss implementing Tetris, an algorithm originally designed for handling natural joins, as an exact model counter for the SharpSAT problem. Tetris uses a simple geometric framework, yet manages to achieve the fractional hypertree-width bound. Its design allows it to handle complex problems involving extremely large numbers of clauses on which other state-of-the-art model counters do not perform well, yet still performs strongly on standard SAT benchmarks. We have achieved the following objectives. First, we have found a natural set of model counting benchmarks on which Tetris outperforms other model counters. Second, we have constructed a data structure capable of efficiently handling and caching all of the data Tetris needs to work on over the course of the algorithm. Third, we have modified Tetris in order to move from a theoretical, asymptotic-time-focused environment to one that performs well in practice. In particular, we have managed to produce results keeping us within a single order of magnitude as compared to other solvers on most benchmarks, and outperform those solvers by multiple orders of magnitude on others.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络