Sharp-SAT (original) (raw)
Na teoria da complexidade computacional, #SAT, ou Sharp-SAT é um problema de função relacionado com o problema da satisfabilidade booleana.
| Property | Value |
|---|---|
| dbo:abstract | In computer science, the Sharp Satisfiability Problem (sometimes called Sharp-SAT or #SAT) is the problem of counting the number of interpretations that satisfies a given Boolean formula, introduced by Valiant in 1979. In other words, it asks in how many ways 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. For example, the formula is satisfiable by three distinct boolean value assignments of the variables, namely, for any of the assignments ( = TRUE, = FALSE), ( = FALSE, = FALSE), ( = TRUE, = TRUE), we have = TRUE. #SAT is different from Boolean satisfiability problem (SAT), which asks if there exists a solution of Boolean formula. Instead, #SAT asks to enumerate all the solutions to a Boolean Formula. #SAT is harder than SAT in the sense that, once the total number of solutions to a Boolean formula is known, SAT can be decided in constant time. However, the converse is not true, because knowing a Boolean formula has a solution does not help us to count all the solutions, as there are an exponential number of possibilities. #SAT is a well-known example of the class of counting problems, known as #P-complete (read as sharp P complete). In other words, every instance of a problem in the complexity class #P can be reduced to an instance of the #SAT problem. This is an important result because many difficult counting problems arise in Enumerative Combinatorics, Statistical physics, Network Reliability, and Artificial intelligence without any known formula. If a problem is shown to be hard, then it provides a complexity theoretic explanation for the lack of nice looking formulas. (en) Na teoria da complexidade computacional, #SAT, ou Sharp-SAT é um problema de função relacionado com o problema da satisfabilidade booleana. (pt) |
| dbo:wikiPageID | 25590565 (xsd:integer) |
| dbo:wikiPageLength | 6546 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1032111377 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Enumerative_combinatorics dbr:Validity_(logic) dbr:Interpretation_(logic) dbr:♯P dbr:♯P-complete dbr:Conjunctive_normal_form dbr:Computational_complexity_theory dbr:Computer_science dbr:Horn-satisfiability dbc:Combinatorics dbr:Non-deterministic_Turing_machine dbr:Binary_Decision_Diagram dbc:Satisfiability_problems dbr:Counting_problem_(complexity) dbr:Artificial_intelligence dbc:Computational_problems dbr:2SAT dbr:3SAT dbr:Boolean_satisfiability_problem dbr:Cook-Levin_theorem dbr:Satisfiability dbr:Sharp-P-complete dbr:Statistical_physics dbr:Boolean_logic dbr:Formula_(mathematical_logic) dbr:Planar_3SAT |
| dbp:reason | hash (en) |
| dbp:title | #SAT (en) |
| dbp:wikiPageUsesTemplate | dbt:Correct_title dbt:Refimprove dbt:Reflist |
| dct:subject | dbc:Combinatorics dbc:Satisfiability_problems dbc:Computational_problems |
| gold:hypernym | dbr:Problem |
| rdf:type | yago:WikicatComputationalProblems yago:WikicatSatisfiabilityProblems yago:Abstraction100002137 yago:Attribute100024264 yago:Condition113920835 yago:Difficulty114408086 yago:Problem114410605 dbo:Disease yago:State100024720 |
| rdfs:comment | Na teoria da complexidade computacional, #SAT, ou Sharp-SAT é um problema de função relacionado com o problema da satisfabilidade booleana. (pt) In computer science, the Sharp Satisfiability Problem (sometimes called Sharp-SAT or #SAT) is the problem of counting the number of interpretations that satisfies a given Boolean formula, introduced by Valiant in 1979. In other words, it asks in how many ways 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. For example, the formula is satisfiable by three distinct boolean value assignments of the variables, namely, for any of the assignments ( = TRUE, = FALSE), ( = FALSE, = FALSE), ( = TRUE, = TRUE), we have = TRUE. (en) |
| rdfs:label | Sharp-SAT (en) Sharp-SAT (pt) |
| owl:sameAs | freebase:Sharp-SAT yago-res:Sharp-SAT wikidata:Sharp-SAT dbpedia-pt:Sharp-SAT https://global.dbpedia.org/id/4uLYt |
| prov:wasDerivedFrom | wikipedia-en:Sharp-SAT?oldid=1032111377&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Sharp-SAT |
| is dbo:wikiPageRedirects of | dbr:Sharpsat |
| is dbo:wikiPageWikiLink of | dbr:♯P-complete dbr:♯P-completeness_of_01-permanent dbr:Boolean_satisfiability_problem dbr:IP_(complexity) dbr:Riemann_mapping_theorem dbr:Sharpsat |
| is foaf:primaryTopic of | wikipedia-en:Sharp-SAT |