Boolean Satisfiability Task

A Boolean Satisfiability Task is a satisfiability task that is restricted to boolean logic sentences (whether they are satisfiable or unsatisfiable)

• AKA: SAT, Propositional Satisfiability, Truth Assignment.
• Context:
  • Input: a Boolean Formula/Logic Clause set. (Convert KB to conjunctive normal form (CNF))
  • output: a Truth Assignment that either satisfies all Clauses, or Failure/Unsatisfiable.
  • It can (typically) be an NP-Complete Task (for task with more than three literals ...)
  • It can be solved by a SAT System (that implements a SAT algorithm).
  • It can be an Automated Reasoning Task.
  • …
• Example(s):
  • Is [math]\displaystyle{ (x_1 \lor ¬x_2 \lor ¬x_3) \land (x_1 \lor x_2 \lor x_4) }[/math] satisfiable? (a 3SAT Task).
  • …
• Counter-Example(s):
  • a Horn Clause Satisfiability Task.
  • a Knapsack Packing Task.
  • an Equation Solving Task.
• See: Constraint Satisfaction Task, MAX-SAT.

---

---

References

2011

• (Wikipedia, 2011) ⇒ http://en.wikipedia.org/wiki/Boolean_satisfiability_problem
  • In computer science, satisfiability (often written in all capitals or abbreviated SAT) is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically FALSE for all possible variable assignments. In this latter case, we would say that the function is unsatisfiable; otherwise it is satisfiable. To emphasize the binary nature of this problem, it is frequently referred to as Boolean or propositional satisfiability. SAT was the first known example of an NP-complete problem. That briefly means that there is no known algorithm that efficiently solves all instances of SAT, and it is generally believed (see P versus NP problem) that no such algorithm can exist. Further, a wide range of other naturally-occurring decision and optimization problems can be transformed into instances of SAT. A class of algorithms called SAT solvers can efficiently solve a large enough subset of SAT instances to be useful in various practical areas such as circuit design and automatic theorem proving, by solving SAT instances made by transforming problems that arise in those areas. Extending the capabilities of SAT solving algorithms is an ongoing area of progress. However, no current such methods can efficiently solve all SAT instances.

---