Computational Complexity of SAT, XSAT and NAE-SAT

Focusing on the Mixed Horn formula class (MHF), this thesis explores the SAT problem, which determines the satisfiability of CNF formulas. Highlighting MHF's significance, it connects this subclass to various NP-complete problems, such as Feedback Vertex Set and Vertex Cover. The work demonstrates that SAT remains NP-complete for certain MHF subclasses and introduces algorithms that improve upon existing time bounds. Additionally, it examines the computational complexity of variants like not-all-equal SAT and exact SAT within linear CNF formulas.