{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/124241"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/124241","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Characterizing Boolean satisfiability variants","abstract":"We survey variants of the Boolean Satisfiability problem from over the years and organize them in what we believe to be the most comprehensive list of known results in SAT variants. We propose a new notation to specify them so that the problems can be compared with no ambiguities, and so that new problems can be more easily identified. We also show hardness of many new variants of SAT including a characterization of Sin-k SAT, hardness of variants of MAX Planar SAT, partial characterization of XNF SAT, consequences of the Ordered Planar Dichotomy, and hardness of NAE SAT variants with a bounded number of variable occurrences, in particular NAE EkSAT-k. This is joint work with Aviv Adler, Leo Alcock, Anastasiia Alokhina, Joshua Ani, Jeffrey Bosboom, Erik Demaine, Yevhenii Diomidov, Jonathan Gabor, Yuzhou Gu, Linus Hamilton, Mirai Ikebuchi, Adam Hesterberg, Jayson Lynch, Zhezheng Luo, Xiao Mao, Kevin Sun, John Urschel, Yinzhan Xu, and Lillian Zhang.","abstract_html":"We survey variants of the Boolean Satisfiability problem from over the years and organize them in what we believe to be the most comprehensive list of known results in SAT variants. We propose a new notation to specify them so that the problems can be compared with no ambiguities, and so that new problems can be more easily identified. We also show hardness of many new variants of SAT including a characterization of Sin-k SAT, hardness of variants of MAX Planar SAT, partial characterization of XNF SAT, consequences of the Ordered Planar Dichotomy, and hardness of NAE SAT variants with a bounded number of variable occurrences, in particular NAE EkSAT-k. This is joint work with Aviv Adler, Leo Alcock, Anastasiia Alokhina, Joshua Ani, Jeffrey Bosboom, Erik Demaine, Yevhenii Diomidov, Jonathan Gabor, Yuzhou Gu, Linus Hamilton, Mirai Ikebuchi, Adam Hesterberg, Jayson Lynch, Zhezheng Luo, Xiao Mao, Kevin Sun, John Urschel, Yinzhan Xu, and Lillian Zhang.","abstract_has_math":false,"creators":["Ferreira Antunes Filho, Ivan Tadeu."],"institution":"Massachusetts Institute of Technology","degree_name":"Master","degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","school":null,"contributors":[],"advisors":["Erik Demaine."],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019","date_published":"2019","updated_at":"2026-07-22T22:21:52Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"rights":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1721.1/124241","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Erik Demaine."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","EECS"]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Ferreira Antunes Filho, Ivan Tadeu."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2020-03-24T15:35:55Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2020-03-24T15:35:55Z"]},{"key":"dc:date.issued","label":"Date","values":["2019"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1721.1/124241"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2019","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 65-70) and index."]},{"key":"dc:description.abstract","label":"Abstract","values":["We survey variants of the Boolean Satisfiability problem from over the years and organize them in what we believe to be the most comprehensive list of known results in SAT variants. We propose a new notation to specify them so that the problems can be compared with no ambiguities, and so that new problems can be more easily identified. We also show hardness of many new variants of SAT including a characterization of Sin-k SAT, hardness of variants of MAX Planar SAT, partial characterization of XNF SAT, consequences of the Ordered Planar Dichotomy, and hardness of NAE SAT variants with a bounded number of variable occurrences, in particular NAE EkSAT-k. This is joint work with Aviv Adler, Leo Alcock, Anastasiia Alokhina, Joshua Ani, Jeffrey Bosboom, Erik Demaine, Yevhenii Diomidov, Jonathan Gabor, Yuzhou Gu, Linus Hamilton, Mirai Ikebuchi, Adam Hesterberg, Jayson Lynch, Zhezheng Luo, Xiao Mao, Kevin Sun, John Urschel, Yinzhan Xu, and Lillian Zhang."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M. Eng."]},{"key":"dc:title","label":"Title","values":["Characterizing Boolean satisfiability variants"]}]}],"canonical_facts":{"dc:contributor.advisor":["Erik Demaine."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","EECS"],"dc:contributor.other":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:creator":["Ferreira Antunes Filho, Ivan Tadeu."],"dc:date.accessioned":["2020-03-24T15:35:55Z"],"dc:date.available":["2020-03-24T15:35:55Z"],"dc:date.issued":["2019"],"dc:description":["This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2019","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 65-70) and index."],"dc:description.abstract":["We survey variants of the Boolean Satisfiability problem from over the years and organize them in what we believe to be the most comprehensive list of known results in SAT variants. We propose a new notation to specify them so that the problems can be compared with no ambiguities, and so that new problems can be more easily identified. We also show hardness of many new variants of SAT including a characterization of Sin-k SAT, hardness of variants of MAX Planar SAT, partial characterization of XNF SAT, consequences of the Ordered Planar Dichotomy, and hardness of NAE SAT variants with a bounded number of variable occurrences, in particular NAE EkSAT-k. This is joint work with Aviv Adler, Leo Alcock, Anastasiia Alokhina, Joshua Ani, Jeffrey Bosboom, Erik Demaine, Yevhenii Diomidov, Jonathan Gabor, Yuzhou Gu, Linus Hamilton, Mirai Ikebuchi, Adam Hesterberg, Jayson Lynch, Zhezheng Luo, Xiao Mao, Kevin Sun, John Urschel, Yinzhan Xu, and Lillian Zhang."],"dc:description.degree":["M. Eng."],"dc:identifier.uri":["https://hdl.handle.net/1721.1/124241"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["Characterizing Boolean satisfiability variants"],"dc:type":["Thesis"],"thesis:degree_name":["Master"]},"updated_at":"2026-07-22T22:21:52Z"}