|
In computer science, the Boolean Satisfiability Problem (sometimes called Propositional Satisfiability Problem and abbreviated as SATISFIABILITY or SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called ''satisfiable''. On the other hand, if no such assignment exists, the function expressed by the formula is identically FALSE for all possible variable assignments and the formula is ''unsatisfiable''. For example, the formula "''a'' AND NOT ''b''" is satisfiable because one can find the values ''a'' = TRUE and ''b'' = FALSE, which make (''a'' AND NOT ''b'') = TRUE. In contrast, "''a'' AND NOT ''a''" is unsatisfiable. SAT is one of the first problems that was proven to be NP-complete. This means that all problems in the complexity class NP, which includes a wide range of natural decision and optimization problems, are at most as difficult to solve as SAT. There is no known algorithm that efficiently solves SAT, and it is generally believed that no such algorithm exists; yet this belief has not been proven mathematically, and resolving the question whether SAT has an efficient algorithm is equivalent to the P versus NP problem, which is the most famous open problem in the theory of computing. Despite the fact that no algorithms are known that solve SAT efficiently, correctly, and for all possible input instances, many instances of SAT that occur in practice, such as in artificial intelligence, circuit design and automatic theorem proving, can actually be solved rather efficiently using heuristical SAT-solvers. Such algorithms are not believed to be efficient on all SAT instances, but experimentally these algorithms tend to work well for many practical applications. ==Basic definitions and terminology== A propositional logic formula, also called Boolean expression, is built from variables, operators AND (conjunction, also denoted by ∧), OR (disjunction, ∨), NOT (negation, ¬), and parentheses. A formula is said to be satisfiable if it can be made TRUE by assigning appropriate logical values (i.e. TRUE, FALSE) to its variables. The Boolean satisfiability problem (SAT) is, given a formula, to check whether it is satisfiable. This decision problem is of central importance in various areas of computer science, including theoretical computer science, complexity theory, algorithmics, cryptography and artificial intelligence. There are several special cases of the Boolean satisfiability problem in which the formulas are required to have a particular structure. A literal is either a variable, then called positive literal, or the negation of a variable, then called negative literal. A clause is a disjunction of literals (or a single literal). A clause is called Horn clause if it contains at most one positive literal. A formula is in conjunctive normal form (CNF) if it is a conjunction of clauses (or a single clause). For example, "''x''1" is a positive literal, "¬''x''2" is a negative literal, "''x''1 ∨ ¬''x''2" is a clause, and "(''x''1 ∨ ¬''x''2) ∧ (¬''x''1 ∨ ''x''2 ∨ ''x''3) ∧ ¬''x''1" is a formula in conjunctive normal form, its 1st and 3rd clause are Horn clauses, but its 2nd clause is not. The formula is satisfiable, choosing ''x''1=FALSE, ''x''2=FALSE, and ''x''3 arbitrarily, since (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ ''x''3) ∧ ¬FALSE evaluates to (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ ''x''3) ∧ TRUE, and in turn to TRUE ∧ TRUE ∧ TRUE (i.e. to TRUE). In contrast, the CNF formula ''a'' ∧ ¬''a'', consisting of two clauses of one literal, is unsatisfiable, since for ''a''=TRUE and ''a''=FALSE it evaluates to TRUE ∧ ¬TRUE (i.e. to FALSE) and FALSE ∧ ¬FALSE (i.e. again to FALSE), respectively. For some versions of the SAT problem, it is useful to define the notion of a generalized conjunctive normal form formula, viz. as a conjunction of arbitrarily many generalized clauses, the latter being of the form ''R''(''l''1,...,''l''''n'') for some boolean operator ''R'' and (ordinary) literals ''l''''i''. Different sets of allowed boolean operators lead to different problem versions. As an example, ''R''(¬''x'',''a'',''b'') is a generalized clause, and ''R''(¬''x'',''a'',''b'') ∧ ''R''(''b'',''y'',''c'') ∧ ''R''(''c'',''d'',¬''z'') is a generalized conjunctive normal form. This formula is used below, with ''R'' being the ternary operator that is TRUE just if exactly one of its arguments is. Using the laws of Boolean algebra, every propositional logic formula can be transformed into an equivalent conjunctive normal form, which may, however, be exponentially longer. For example, transforming the formula (''x''1∧''y''1) ∨ (''x''2∧''y''2) ∨ ... ∨ (''x''''n''∧''y''''n'') into conjunctive normal form yields (''x''1∨''x''2∨…∨''x''''n'') ∧ (''y''1∨''x''2∨…∨''x''''n'') ∧ (''x''1∨''y''2∨…∨''x''''n'') ∧ (''y''1∨''y''2∨…∨''x''''n'') ∧ ... ∧ (''x''1∨''x''2∨…∨''y''''n'') ∧ (''y''1∨''x''2∨…∨''y''''n'') ∧ (''x''1∨''y''2∨…∨''y''''n'') ∧ (''y''1∨''y''2∨…∨''y''''n''); while the former is a disjunction of ''n'' conjunctions of 2 variables, the latter consists of 2''n'' clauses of ''n'' variables. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Boolean satisfiability problem」の詳細全文を読む スポンサード リンク
|