The Boolean satisfiability problem. It consists of determining a satisfying variable assignment, V, for a Boolean function, f, or determining that no such V exists. SAT is one of the central NP-complete problems.
Published in Chapter:
On the Implementation of a Logic Language for NP Search and Optimization Problems
Sergio Greco (University of Calabria, Italy), Cristian Molinaro (University of Calabria, Italy), Irina Trubitsyna (University of Calabria, Italy), and Ester Zumpano (University of Calabria, Italy)
Copyright: © 2009
|Pages: 7
DOI: 10.4018/978-1-60566-242-8.ch084
Abstract
It is well known that NP search and optimization problems can be formulated as DATALOG¬ (datalog with unstratified negation; Abiteboul, Hull, & Vianu, 1994) queries under nondeterministic stable-model semantics so that each stable model corresponds to a possible solution (Gelfond & Lifschitz, 1988; Greco & Saccà, 1997; Kolaitis & Thakur, 1994). Although the use of (declarative) logic languages facilitates the process of writing complex applications, the use of unstratified negation allows programs to be written that in some cases are neither intuitive nor efficiently valuable. This article presents the logic language NP Datalog, a restricted version of DATALOG¬ that admits only controlled forms of negation, such as stratified negation, exclusive disjunction, and constraints. NP Datalog has the same expressive power as DATALOG¬, enables a simpler and intuitive formulation for search and optimization problems, and can be easily translated into other formalisms. The example below shows how the vertex cover problem can be expressed in NP Datalog.