2-satisfiability

2-Satisfiability, often abbreviated as 2-SAT, is a decision problem in computer science and mathematical logic that involves determining the satisfiability of a boolean formula expressed in conjunctive normal form (CNF) with exactly two literals per clause. In formal terms, a 2-SAT formula consists of a conjunction (AND) of clauses, where each clause is a disjunction (OR) of exactly two literals. A literal is a variable or its negation.