problema de satisfatibilidade booleana

Na teoria da complexidade computacional, o problema de satisfatibilidade booliana (do inglês boolean satisfiability problem, muitas vezes abreviado como SATISFIABILITY ou SAT) foi o primeiro problema identificado como pertencente à classe de complexidade NP-completo.O problema de satisfatibilidade booliana é o problema de determinar se existe uma determinada valoração para as variáveis de uma determinada fórmula booliana tal que esta valoração satisfaça esta fórmula em questão. Por exemplo, tomando como as variáveis boolianas e a expressão caso exista uma atribuição de valores de verdade para as variáveis da fórmula que torne a fórmula avaliada VERDADEIRA, esta fórmula é considera satisfatível, em contrapartida se nenhuma atribuição levou a uma avaliação da fórmula como verdadeira, ela é considerada insatisfatível. Para salientar a natureza binária deste problema, ele é referenciado freqüentemente como o problema de satisfatibilidade booliana ou proposicional. A sigla SAT também é geralmente utilizada para denotá-lo, com o entendimento implícito de que a função e suas variáveis recebem valores binários.