Complexidades temporais dos solucionadores SAT de última geração em relação ao comprimento da fórmula

Question

Estou aprendendo sobre os solucionadores DPLL e CDCL SAT e sei que eles têm complexidade de tempo exponencial ao número de variáveis.

Se não me engano, uma das razões pelas quais a maioria acredita que P não é igual a NP é que não existe algoritmo de tempo polinomial para SAT, apesar do tremendo esforço de matemáticos e cientistas da computação.No entanto, o problema P vs NP se preocupa apenas com a complexidade do tempo em relação ao comprimento da fórmula, não com o número de variáveis.

Se esses solucionadores SAT de última geração fossem executados em fórmulas 3CNF, então uma complexidade de tempo exponencial ao número de variáveis ​​implica uma complexidade de tempo exponencial ao comprimento do 3CNF.

No entanto, se fossem executados em CNFs arbitrárias, cujo comprimento pode ser exponencial ao número de variáveis, então uma complexidade de tempo exponencial ao número de variáveis ​​não implicaria necessariamente uma complexidade de tempo exponencial ao comprimento do CNF.

Assim, uma questão relacionada é: esses solucionadores SAT são executados em 3CNF ou CNF enquanto medem a complexidade do tempo?

Answer 1

Para 3SAT, o número de variáveis ​​está polinomialmente relacionado ao número de cláusulas.(Veja o final para a justificativa.)

Conseqüentemente, qualquer algoritmo para 3SAT cujo tempo de execução seja polinomial no número de cláusulas também seria polinomial no número de variáveis;e qualquer algoritmo para 3SAT cujo tempo de execução seja polinomial no número de variáveis ​​também seria polinomial no número de cláusulas.

Sabe-se que existe um algoritmo de tempo polinomial para 3SAT, se e somente se houver um algoritmo de tempo polinomial para SAT, se e somente se houver um algoritmo de tempo polinomial para CircuitSAT (por exemplo, para fórmulas).Além disso, apesar de décadas de trabalho em solucionadores SAT, ninguém conhece nenhum algoritmo para 3SAT que seja executado em tempo polinomial (ou mesmo em tempo inferior a exponencial, no pior caso).Você poderia considerar isso como evidência de que não existe um algoritmo de tempo polinomial para 3SAT;o que implica que também não existe algoritmo de tempo polinomial para SAT ou CircuitSAT, e também implica que P != NP.

---

Justificação:Deixar $n$ denotar o número de variáveis ​​​​e $m$ o número de cláusulas.Nós temos $n \le 3m$ (uma variável que não aparece em nenhuma cláusula pode ser ignorada) e $m\le 8n^3$ (cada cláusula possui três literais e você pode ignorar cláusulas repetidas).Segue que $n/3 \le m \le 8n^3$ e $\sqrt[3]{m/8} \le n \le 3m$, ou seja, cada um está polinomialmente relacionado ao outro.

---

Vejo que você revisou sua pergunta.Isso esclarece que acho que você tem um equívoco.Você fala sobre "executar [ning] [um solucionador SAT] em fórmulas booleanas arbitrárias".No entanto, você não pode executar um solucionador SAT em uma fórmula booleana arbitrária.Os solucionadores SAT funcionam apenas em fórmulas CNF.

No entanto, sabemos que qualquer fórmula booleana pode ser convertida em uma fórmula CNF equisatisfatível de tamanho no máximo polinomial no tamanho da fórmula e vice-versa.Se você tivesse um algoritmo que pudesse testar a satisfatibilidade de fórmulas booleanas arbitrárias em tempo polinomial no tamanho da fórmula, então seguiria que você teria um algoritmo que pudesse testar a satisfatibilidade de fórmulas 3CNF em tempo polinomial no tamanho da fórmula (cada A fórmula 3CNF é uma fórmula booleana) e, portanto, um algoritmo que poderia testar a satisfatibilidade das fórmulas 3CNF em tempo polinomial no número de variáveis ​​- o que contradiz as evidências disponíveis.Portanto, se você acredita que não existe um algoritmo para resolver 3SAT em tempo polinomial no número de variáveis, então você também deve acreditar que não existe um algoritmo para testar a satisfatibilidade de fórmulas booleanas arbitrárias em tempo polinomial no tamanho da fórmula.