{"id":{"repo_id":"buffalo","oai_identifier":"oai:ubir.buffalo.edu:10477/78530"},"canonical_url":"https://search.dev.ndltd.org/etd/buffalo/oai:ubir.buffalo.edu:10477/78530","repository":{"repo_id":"buffalo","name":"Buffalo","base_url":"https://ubir.buffalo.edu/oai/request"},"display":{"title":"Implementation of Tetris as a Model Counter","abstract":"Ph.D.","abstract_html":"Ph.D.","abstract_has_math":false,"creators":["Dobler, Jimmy"],"institution":"State University of New York at Buffalo","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Rudra, Atri","Computer Science and Engineering"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2018,"date_issued":"2018-10-26T02:54:55Z","date_published":"2018-10-26T02:54:55Z","updated_at":"2026-07-27T19:05:12Z","subjects":["computer science"],"languages":["eng"],"rights":["Users of works found in University at Buffalo Institutional Repository (UBIR) are responsible for identifying and contacting the copyright owner for permission to reuse. University at Buffalo Libraries do not manage rights for copyright-protected works and cannot assist with permissions.","Copyright retained by author."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/10477/78530","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Rudra, Atri","Computer Science and Engineering"]},{"key":"dc:creator","label":"Author","values":["Dobler, Jimmy"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2018-10-26T02:54:55Z","2018","2018-07-24 14:53:16"]},{"key":"dc:publisher","label":"Institution","values":["State University of New York at Buffalo"]},{"key":"dc:type","label":"Dc Type","values":["Text","Dissertation"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["computer science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Users of works found in University at Buffalo Institutional Repository (UBIR) are responsible for identifying and contacting the copyright owner for permission to reuse. University at Buffalo Libraries do not manage rights for copyright-protected works and cannot assist with permissions.","Copyright retained by author."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/10477/78530"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Ph.D.","Solving #SAT problems is an important area of work. In this thesis, we discuss implementing Tetris, an algorithm originally designed for handling natural database joins, as an exact model counter for the #SAT problem, where we want to count the number of satisfying solutions to a SAT formula. Tetris uses a simple geometric framework, yet manages to achieve the fractional hypertree-width bound. While the original Tetris paper made theoretical connections to #SAT, it left open the questions of implementation and practicality, which we tackle. In this thesis, we achieve the following objectives. First, we have utilized Tetris 's design to allow it to handle complex problems involving extremely large numbers of clauses on which other state-off-the-art model counters do not perform well. The result outperforms other solvers by multiple orders of magnitude, while still remaining competitive on standard #SAT benchmarks. Second, we use SIMD techniques and a novel breadth-first design to construct 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, including adding techniques that allow for intelligent shortcutting where possible. In particular, we have introduced various strategies that allow us to significantly reduce the number of database calls while not adding a significant amount of overhead. Fourth, we have found a natural set of model counting benchmarks on which Tetris outperforms other model counters."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Implementation of Tetris as a Model Counter"]}]}],"canonical_facts":{"dc:contributor":["Rudra, Atri","Computer Science and Engineering"],"dc:creator":["Dobler, Jimmy"],"dc:date":["2018-10-26T02:54:55Z","2018","2018-07-24 14:53:16"],"dc:description":["Ph.D.","Solving #SAT problems is an important area of work. In this thesis, we discuss implementing Tetris, an algorithm originally designed for handling natural database joins, as an exact model counter for the #SAT problem, where we want to count the number of satisfying solutions to a SAT formula. Tetris uses a simple geometric framework, yet manages to achieve the fractional hypertree-width bound. While the original Tetris paper made theoretical connections to #SAT, it left open the questions of implementation and practicality, which we tackle. In this thesis, we achieve the following objectives. First, we have utilized Tetris 's design to allow it to handle complex problems involving extremely large numbers of clauses on which other state-off-the-art model counters do not perform well. The result outperforms other solvers by multiple orders of magnitude, while still remaining competitive on standard #SAT benchmarks. Second, we use SIMD techniques and a novel breadth-first design to construct 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, including adding techniques that allow for intelligent shortcutting where possible. In particular, we have introduced various strategies that allow us to significantly reduce the number of database calls while not adding a significant amount of overhead. Fourth, we have found a natural set of model counting benchmarks on which Tetris outperforms other model counters."],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/10477/78530"],"dc:language":["eng"],"dc:publisher":["State University of New York at Buffalo"],"dc:rights":["Users of works found in University at Buffalo Institutional Repository (UBIR) are responsible for identifying and contacting the copyright owner for permission to reuse. University at Buffalo Libraries do not manage rights for copyright-protected works and cannot assist with permissions.","Copyright retained by author."],"dc:subject":["computer science"],"dc:title":["Implementation of Tetris as a Model Counter"],"dc:type":["Text","Dissertation"]},"updated_at":"2026-07-27T19:05:12Z"}