2sat (442B)
1 # 2SAT 2 3 [satisfiability_boolean] of [2cnf] 4 5 Can be solved in [linear_time] via [strongly_connected_component], is [nl_complete] 6 7 However: 8 9 - The [max_sat] problem of satisfying the largest number of clauses of a [2cnf] is [nptime]-hard ([garey_johnson] LO5) 10 - The [sharp_satisfiability] problem of counting the satisfying assignments is [nptime]-hard, even for [monotone2cnf] 11 12 Generalization: [max_2sat] 13 14 See also: [3sat] 15 16 Up: [sat_variants]