# Implementation of Tetris as a Model Counter

## TL;DR

This paper presents Tetris as a novel exact model counter for SharpSAT problems, demonstrating superior performance on complex benchmarks and standard SAT problems through a geometric framework and optimized data structures.

## Contribution

Introducing Tetris as a new model counter for SharpSAT problems, with practical modifications for improved performance and handling large, complex clause sets.

## Key findings

- Tetris outperforms existing counters on certain benchmarks.
- Efficient data structures enable Tetris to handle large problem instances.
- Tetris achieves comparable or better results than state-of-the-art solvers.

## Abstract

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.