|
In computational complexity theory, #SAT, or Sharp-SAT, a function problem related to the Boolean satisfiability problem, is the problem of counting the number of satisfying assignments of a given Boolean formula. It is well-known example for the class of counting problems, which are of special interest in computational complexity theory. It is a #P-complete problem, as any NP machine can be encoded into a Boolean formula by a process similar to that in Cook's theorem, such that the number of satisfying assignments of the Boolean formula is equal to the number of accepting paths of the NP machine. Any formula in SAT can be rewritten as a formula in 3-CNF form preserving the number of satisfying assignments, and so #SAT and #3SAT are equivalent and #3SAT is #P-complete as well. ==Intractable special cases== Model-counting is intractable in many special cases for which satisfiability is tractable. This includes the following. * sets of Horn clauses * sets of 2-literal clauses 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Sharp-SAT」の詳細全文を読む スポンサード リンク
|