satisfiability problem

satisfiability problem

A problem used as an example in complexity theory. It can be stated thus:

Given a Boolean expression E, decide if there is some assignment to the variables in E such that E is true.

A Boolean expression is composed of Boolean variables, (logical) negation (NOT), (logical) conjunction (AND) and parentheses for grouping. The satisfiability problem was the first problem to be proved to be NP-complete (by Cook).

["Introduction to Automata Theory, Languages, and Computation" by Hopcroft and Ullman, pub. Addison-Wesley].
This article is provided by FOLDOC - Free Online Dictionary of Computing (foldoc.org)
Mentioned in ?
References in periodicals archive ?
In this model, each cell can produce and examine a solution of satisfiability problem. As a result, billions of cells can explore billions of possible solutions [29].
Literature [12] proposes a new algorithm based on Boolean satisfiability problem to solve the minimal cut sets in fault tree analysis.
Given a Boolean formula f depending on V , the Boolean Satisfiability problem [11], usually known as SAT, consists in finding, if it exists, an assignment to the variables of f, namely {[v.sub.1], [v.sub.2], ..., [v.sub.n]}, such that f is true, i.e., f([v.sub.1], [v.sub.2], ..., [v.sub.n]) = 1.
For checking rules for inconsistency it is proposed to use AND/OR-graph and solution of satisfiability problem for Boolean formulas (SATisfiability problem--SAT) [11].
A special planar satisfiability problem and a consequence of its NP-completeness.
Jose and Majumdar have presented a new algorithm for error cause localization based on a reduction to the maximal satisfiability problem called MAX-SAT, which asks what is the maximum number of clauses of a Boolean formula that can be simultaneously satisfied by an assignment [16].
Generally, the satisfiability problem (SAT) which is known to be NP-complete [15] is defined as follows.
The proposed solution searching device finds a solution to a nondeterministic polynomial (NP) time complete problem, the satisfiability problem (SAT), much faster than the WalkSAT algorithm, which is one of the fastest stochastic local search algorithms [9, 12].
The problem of computing all signal probabilities in a circuit can be formulated as a random satisfiability problem, which is to determine the probability that a random assignment of variables will satisfy a given Boolean formula [9].
In this paper, we will call as 'WSPS' (Workflow Satisfiability Problem situation) a situation where the WFMS is unable to find (for availability or security reasons) an authorized user to assign to the current task instance in a workflow instance.
Propositional satisfiability problem (SAT) is a well-known decision problem.