The 2SAT Problem: Difference between revisions

From NovaOrdis Knowledge Base
Jump to navigation Jump to search
Line 16: Line 16:
* Reduction to computing strongly connected components.
* Reduction to computing strongly connected components.
* "Backtracking"
* "Backtracking"
* Randomized local search
* Randomized local search. Generally, local search heuristics are not guaranteed to run in polynomial time. This 2SAT problem is one of the rare cases when we can prove it is guaranteed to converge with the correct answer quickly.

Revision as of 04:25, 30 November 2021

External

Internal

Overview

The Problem

Given a set of n boolean variables x1, x2, ..., xn, that can be set to true or false and a set of m clauses of 2 literals each (a "literal" is a variable or the negation of the variable: xi or !xi). The output is determining whether there is a variable assignment that simultaneously satisfies every clause.

The 2SAT problem can be solved in polynomial time - it is not an NP-complete problem.

Algorithms

  • Reduction to computing strongly connected components.
  • "Backtracking"
  • Randomized local search. Generally, local search heuristics are not guaranteed to run in polynomial time. This 2SAT problem is one of the rare cases when we can prove it is guaranteed to converge with the correct answer quickly.