Estudo do problema 2-SAT: algoritmos eficientes e suas aplicações na programação competitiva

Abstract

This work addresses the 2-CNF-SAT problem, a restriction of the Boolean Satisfiability Problem, also known as Satisfiability (SAT), in which formulas are given in Conjunctive Normal Form (CNF) and each clause contains exactly two literals. The main objective is to provide an accessible material in Portuguese for the competitive programming community, especially for those who are preparing themselves for competitions such as the Brazilian Informatics Olympiad (OBI) and the Brazilian Programming Marathon, which serve as qualifying stages for international events like the International Olympiad in Informatics (IOI) and the International Collegiate Programming Contest (ICPC). Furthermore, this work presents the theoretical foundations necessary to understand the 2-CNF-SAT problem and two classic algorithms to solve it, namely the unit propagation-based algorithm proposed in Even et al. (1976) and the graph-based algorithm proposed in Aspvall et al. (1979). Finally, this work also discusses a set of competitive programming problems, showing how they can be modeled into formulas that are instances of the 2-CNF-SAT problem.