Problema da satisfatibilidade de circuito
Na teoria da ciência da computação, o problema da satisfatibilidade de circuito (também conhecido como CIRCUITO-SAT, CircuitoSAT, CSAT, etc.) é o problema de decisão de determinar se um dado circuito Booleano tem uma atribuição das entradas, que torna a saída verdadeira.[1]
Propriedades editar
CircuitoSAT foi provado ser NP-completo.[2] Na verdade, é um protótipo de problema NP-completo; o Teorema de Cook-Levin é, por vezes, provado em CircuitoSAT em vez de ser provado pelas expressões Booleanas para SAT e, em seguida, reduzido para outros problemas de satisfatibilidade para provar a sua NP-completude.[1][3]
A satisfatibilidade de um circuito contendo m portas binárias arbitrárias, pode ser decidido em tempo .[4]
A transformação de Tseitin editar
Existe uma simples redução de CircuitoSAT a SAT, conhecida como a transformação de Tseitin. A transformação é especialmente fácil de descrever, se o circuito é totalmente construído a partir de 2 entradas de portas NAND (um conjunto funcionalmente-completo de operadores Booleanos): atribuir a cada rede no circuito de uma variável e, em seguida, para cada porta NAND, construir as cláusulas na forma normal conjuntiva (v1 ∨ v3) ∧ (v2 ∨ v3) ∧ (v1 ∨ v2 ∨ v3) onde v1 e v2 são as entradas para a porta NAND e v3 é a saída. Estas cláusulas descrevem completamente a relação entre as três variáveis. Unindo as cláusulas de todas as portas com uma cláusula adicional restritiva da variável de saída do circuito para ser verdade completa a redução; uma atribuição de variáveis que satisfaça as restrições existe se, e somente se, o circuito original é satisfatível, e qualquer solução é uma solução para o problema original de encontrar entradas que fazem o circuito de saída 1.[1][5] (O inverso, que SAT é redutível a CircuitoSAT, é ainda mais fácil—simplesmente reescrevemos a fórmula Booleana como um circuito e o resolvemos.)
Referências editar
- ↑ a b c David Mix Barrington and Alexis Maciel (5 de julho de 2000). «Lecture 7: NP-Complete Problems» (PDF)
- ↑ Luca Trevisan (29 de novembro de 2001). «Notes for Lecture 23: NP-completeness of Circuit-SAT» (PDF)
- ↑ See also, for example, the informal proof given in Scott Aaronson's lecture notes from his course Quantum Computing Since Democritus.
- ↑ Sergey Nurk (1 de dezembro de 2009). «An O(2^{0.4058m}) upper bound for Circuit SAT»
- ↑ Marques-Silva, João P. and Luís Guerra e Silva (1999). «Algorithms for Satisfiability in Combinational Circuits Based on Backtrack Search and Recursive Learning» (PDF)[ligação inativa]