Implementation of Tetris as a Model Counter
MetadataShow full item record
Solving SharpSAT and MaxSAT problems is an important area of work. Here, we discuss implementing Tetris, an algorithm originally designed for handling natural joins, as an exact model counter for the SharpSAT problem and as a MaxSAT solver. 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. \par We have achieved the following objectives. First, we have found a natural set of 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 small constant factor as compared to other solvers on most benchmarks, while still maintaining an advantage of multiple orders of magnitude on the aforementioned datasets where it excels.