Procurando fonte de literatura para seguir a ideia

12

Tenho certeza de que não sou o primeiro a aceitar a idéia que vou apresentar. No entanto, seria útil encontrar alguma literatura relacionada à idéia.

A idéia é construir uma Máquina de Turing M com a propriedade de que, se P = NP, M resolverá o 3-SAT em tempo polinomial. (A escolha do 3-SAT é arbitrária. Poderia ser realmente qualquer problema no NP).

Só para ficar claro, isso não é uma afirmação de que P = NP. Na verdade, acredito no contrário. Apenas afirmo que, se P = NP, M fornecerá uma solução em tempo polinomial. Se você está procurando uma solução eficiente, devo avisar que isso está longe de ser eficiente.

M é construído da seguinte maneira: primeiro, assuma uma codificação canônica para todas as máquinas de Turing e aplique uma numeração a essas máquinas. Portanto, existe uma máquina de Turing número 1, um número 2, etc. A ideia de uma máquina de Turing universal que pode ler o formato de uma máquina fornecida e simular a máquina em funcionamento em uma entrada separada é bem conhecida. M empregará uma Máquina Universal de Turing para construir e simular cada uma delas.

Primeiro, simula o funcionamento da Máquina de Turing 1 para uma única etapa.
Em seguida, ele analisa a saída da Turing Machine 1.
Simula o funcionamento da Turing Machine 1 por duas etapas e analisa a saída e, em seguida, procede à simulação da Turing Machine 2 por 2 etapas. Ele continua e faz um loop dessa maneira, executando a Máquina de Turing 1 para k etapas e depois 2 para k etapas ... e, finalmente, usina k para k etapas.

Após cada execução da simulação, ele examina a saída da execução. Se a saída for uma designação de variáveis ​​que satisfaçam a instância do problema 3-SAT, M parará no estado de aceitação. Se, por outro lado, a saída for uma string de prova em alguma linguagem de prova verificável, com o resultado comprovado de que a instância do problema não é satisfatória, M pára no estado de rejeição. (Para uma linguagem de prova, poderíamos, por exemplo, usar os axiomas de Peano com lógica de segunda ordem e os axiomas lógicos básicos de Hilbert. Deixo como um exercício para o leitor descobrir que, se P = NP, um válido existe uma linguagem de prova e é verificável em tempo polinomial).

Afirmo aqui que M resolverá o 3-SAT em tempo polinomial se e somente se P = NP. Eventualmente, o algoritmo encontrará uma Máquina de Turing mágica com o número K, que, por acaso, é um solucionador eficiente para o problema 3-SAT, e é capaz de fornecer uma prova de seus resultados, tanto para o sucesso quanto para o fracasso. O K será simulado executando etapas de poli (strlen (entrada)) para algum polinômio. O polinômio para M é aproximadamente o quadrado do polinômio para k no fator maior, mas com algumas constantes terríveis no polinômio.

Para reiterar minha pergunta aqui: quero saber se existe uma fonte de literatura que emprega essa ideia. Estou um pouco menos interessado em discutir a ideia em si.

Bill Province
fonte

Respostas:

16

Parece que essa idéia é atribuída a Levin (é chamada de pesquisa ideal). Eu acredito que esse fato é bem conhecido. Um algoritmo semelhante é descrito na Wikipedia, por exemplo, embora esteja usando o problema de soma de subconjuntos. Neste artigo da scholarpedia, você pode encontrar várias referências sobre o assunto, incluindo um ponteiro para o algoritmo original e alguns outros algoritmos de pesquisa ideais.

φP=NPφ

Comentário 2: Como Jaroslaw Blasiok apontou em outra resposta, esse algoritmo não decide Sat apenas assumindo P = NP.

Mateus de Oliveira Oliveira
fonte
Acabei de encontrar a referência da Wikipedia e, de fato, menciona Levin, mas sem citação. Pode ser que isso simplesmente tenha se tornado folclore, mas nunca usado na literatura publicada. Independentemente disso, isso é útil. Obrigado.
Bill Province
Bem-vinda. Encontrei uma página inicial com várias referências sobre o assunto. Eu editei a resposta para incluí-la.
Mateus de Oliveira Oliveira
6

A idéia de executar na diagonal todas as máquinas de Turing possíveis foi usada anteriormente por Leonid Levin no que agora é conhecido como Levins Universal Search. Infelizmente, e ao contrário do equívoco extremamente comum, pelo que sei, variações na pesquisa universal de Levins NÃO são capazes de fornecer algoritmos explícitos para resolver SAT (problema de decisão) em tempo polinomial, considerando apenas a suposição de que P = NP - e nem o seu algoritmo .

A ressalva do raciocínio proposto está (com muita freqüência) no "exercício fácil deixado ao leitor" - eu mesmo não pude provar o exercício e não acredito que sua afirmação seja verdadeira, a saber:

Assumindo P = NP, há um tamanho polinomial que o ZFC prova de insatisfação de determinada fórmula booleana.

Além disso: não vejo como provar a existência de um ZFC polinomialmente curto prova a insatisfação sob (mais forte) suposição de que "P = NP é comprovável no ZFC". Torna-se fácil, porém, sob suposição ainda mais forte, a saber:

(*) Existe a máquina M rodando em tempo polinomial que comprovadamente resolve SAT.

E essa é, acredito, a suposição correta sob a qual seu algoritmo resolve SAT em tempo polinomial. Acima, por "provàvelmente resolve SAT", quero dizer: existe uma máquina M e uma prova de ZFC que M resolve SAT.

Observe que essa suposição ainda é um pouco mais fraca que a seguinte: (**) Existe a máquina M, que provavelmente roda em tempo polinomial e que resolve SAT.

Em (**), pode-se ter uma construção explícita alcançando o mesmo objetivo, que é ainda mais simples: enumere todas as provas do ZFC até encontrar a máquina correta M (gastando tempo constante) e, em seguida, execute M em determinada instância.

É verdade, no entanto, que, sob a premissa de P = NP, existe algum sistema de prova polinomialmente verificável, com pequenas provas de insatisfação de determinada fórmula. Infelizmente, não conhecemos nem o sistema de prova nem o verificador de imediato, e não é útil nessa configuração.

f1(x)

Observe que esse esquema se aplica, por exemplo, ao problema FACTORING; aqui f é apenas multiplicação (definida apenas para fatores diferentes de \ pm 1) e B é verificação de primaridade. Portanto, a pesquisa universal de Levins seria (até um fator constante) o algoritmo ideal para FACTORING. Dado que o algoritmo ideal é mais lento que o algoritmo conhecido para verificação de primaridade - no outro caso, a verificação de primaridade se torna dominante.

NPcoNP

Jarosław Błasiok
fonte
1
Se P = NP então co-NP = co-P = P = NP. Portanto, a INCONFIABILIDADE está em NP, assim como testemunhas de tamanho polinomial - você não precisa invocar uma máquina de Turing. Você não pode converter essa testemunha em uma prova ZFC de que a fórmula é insatisfatória? Não entendo a mecânica da prova do ZFC, mas a intuição que recebi de vários lugares é que, a menos que você esteja lidando com "coisas estranhas", o ZFC corresponde a todas as coisas que você pensou que poderia provar de qualquer maneira antes você ouviu falar sobre teoria dos conjuntos. Objetos finitos, como uma fórmula booleana e uma testemunha polinomial de sua insatisfação, provavelmente não são estranhos.
precisa saber é o seguinte
Sim, se P = NP, UNSAT está em NP e possui testemunha de tamanho polinomial. Ou seja: testemunha de tamanho zero, todo o trabalho é feito pelo verificador, certo? Tenho apenas uma ideia em mente como converter essa testemunha de tamanho zero em ZFC e provar que é insatisfatória: forneça uma prova de ZFC de que minha máquina realmente resolve UNSAT e mostre uma corrida dessa máquina na fórmula - isso seria uma prova válida, e isso corresponde ao fato de que o algoritmo proposto pelo OP funciona em (*). Mas e se houvesse alguma máquina complicada que resolvesse o SAT, mas esse fato é improvável? Não que eu acredito é o caso
Jarosław Błasiok
1
O equívoco ao qual estou me referindo é: "se P = NP, a Levins Universal Search fornece um algoritmo de tempo polinomial para resolver um problema NP-completo" ou como às vezes é afirmado: "É impossível ter apenas uma prova não construtiva de P = NP, porque do algoritmo de Levins ". Ambos são falsos - a formulação da Wikipedia apresenta um método que para em polytime em instâncias YES de SUBSET SUM, mas não pára em instâncias NO - não é um algoritmo que decide a soma de subconjuntos em polytime. A formulação do OP é melhor para o objetivo, mas precisa de suposições mais fortes do que P = NP para decidir o SAT no polytime.
Jarosław Błasiok 7/11
1
NPcoNP
1
Agora, a maneira de lidar com isso, como você não conhece explicitamente o verificador para o problema unSAT, seria tentar encontrar uma prova curta em alguma lógica formal que já conhecemos e podemos verificar (sejam axiomas ZFC ou Peano - estamos é mais provável que encontre uma prova curta no primeiro), que esse exemplo é insatisfatório. Mas se alguém quiser provar que existe uma prova tão curta nessa lógica formal, precisará de suposições mais fortes do que P = NP.
Jarosław Błasiok 7/11