Descrição
Resolve problemas de satisfatibilidade booleana, em que a pergunta é se um conjunto de condições lógicas pode ser verdadeiro ao mesmo tempo. Pesquisadores e engenheiros usam resolvedores SAT em verificação, planejamento, otimização e raciocínio automatizado.
Esta é uma ferramenta científica de linha de comando. É útil quando outro programa gera arquivos de entrada SAT ou quando o usuário estuda diretamente lógica e resolução de restrições.