Characterizing Boolean satisfiability variants

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.

Name thesis:degree_name

Master

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2019

Author dc:creator

• Ferreira Antunes Filho, Ivan Tadeu.

Advisor dc:contributor.advisor

• Erik Demaine.

• Electrical Engineering and Computer Science.

Statement 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.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/124241

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/124241