De acordo com o XOR Satisfiability Solver Module para integração de DPLL por Tero Laitinen, precisamos de cláusulas n - 1 CNF para converter uma cláusula XOR-SAT n literal se não quisermos aumentar o número de literais. Portanto, entendo que o custo computacional para converter uma expressão XOR-SAT em um estritamente CNF k- SAT é exponencial.
Minha pergunta: qual é o custo computacional se eu quiser reverter o processo? Qual é o custo computacional da conversão de uma expressão CNF -SAT em uma expressão XOR-SAT? Assumo a promessa de que, neste caso, apenas as expressões k -SAT com expressões XOR-SAT equivalentes são consideradas.
sat
boolean-functions
boolean-formulas
Omar Shehab
fonte
fonte
Respostas:
Se todos os relacionamentos XOR entre variáveis nas fórmulas CNF pudessem ser detectados em tempo polinomial, isso permitiria a solução de UNAMBIGUOUS-SAT em tempo polinomial. Pelo teorema de Valiant – Vazirani, esse resultado implicaria que NP = RP.
No caso limitado de recuperar relações XOR codificadas da maneira usual, ou seja,
para
isso pode ser feito em tempo polinomial , classificando as cláusulas seguidas por uma varredura em tempo linear.
fonte