28

A postagem no blog de Scott Aaronson hoje deu uma lista de problemas / tarefas abertos interessantes em complexidade. Um em particular chamou minha atenção:

Crie uma biblioteca pública de instâncias 3SAT, com o menor número possível de variáveis e cláusulas, que teria consequências notáveis se resolvidas. (Por exemplo, instâncias que codificam os desafios de fatoração de RSA.) Investigue o desempenho dos melhores solucionadores de SAT atuais nesta biblioteca.

Isso desencadeou minha pergunta: qual é a técnica padrão para reduzir os problemas de RSA / fatoração para SAT e qual a velocidade? Existe uma redução tão padrão?

Só para esclarecer, por "rápido" não quero dizer tempo polinomial. Gostaria de saber se temos limites superiores mais apertados na complexidade da redução. Por exemplo, há uma redução cúbica conhecida?

cc.complexity-theory cr.crypto-security sat reductions factoring Huck Bennett
fonte

26

Uma abordagem para codificar o fatoramento (RSA) no SAT é usar circuitos multiplicadores (todos os circuitos podem ser codificados como CNF).

Vamos supor que recebemos um número inteiro com bits, . Estamos interessados em encontrar dois bits inteiros e , cujo produto é $C$ $2n$ $C=(c_1,c_2,\cdots,c_{2n})_2$ $n$ $A=(a_1,\cdots,a_n)$ $A=(b_1,\cdots,b_n)$ . $C=A*B$

A codificação mais ingênua pode ser algo assim: sabemos que

c_{2 n} = {uma}_{n} \land b_{n}

$c_{2n}= a_n \land b_n$

c_{2 n - 1} = ({uma}_{n} \land b_{n - 1}) x o r ({uma}_{n - 1} \land b_{n})

$c_{2n-1}= (a_n\land b_{n-1}) xor (a_{n-1}\land b_n)$

C uma r r y : d_{2 n - 1} = ({uma}_{n} \land b_{n - 1}) \land ({uma}_{n - 1} \land b_{n})

$Carry:d_{2n-1}= (a_n\land b_{n-1}) \land (a_{n-1}\land b_n)$

...

c_{2 n - 2} = ({uma}_{n} \land b_{n - 2}) x o r ({uma}_{n - 1} \land b_{n - 1}) x o r ({uma}_{n - 2} \land b_{n}) x o r d_{2 n - 1}

$c_{2n-2}= (a_n\land b_{n-2}) xor (a_{n-1}\land b_{n-1}) xor (a_{n-2}\land b_{n}) xor d_{2n-1}$

Em seguida, usando a transformação Tseitin, a codificação acima pode ser convertida em CNF.

Essa abordagem produz um CNF relativamente pequeno. Mas essa codificação não suporta "Propagação de Unidade" e, portanto, o desempenho dos SAT Solvers é muito ruim.

Existem outros circuitos para multiplicação que podem ser utilizados para esse fim, mas eles produzem um CNF maior.

Amir
fonte

10

Na seção 6.1 de "Encontrando instâncias difíceis do problema de satisfação: uma pesquisa", de Cook e Mitchell, eles usam esse problema como um desafio.

Amir

Como você sabe que A e B devem ter n bits de comprimento, não poderiam ser n-1 e n bits. Com certeza pode ser 2n bits e 1 bit.

Ilya Gazman

1

@Babibu: Se estamos falando sobre fatoração geral, você está certo. Mas, no caso do RSA, sabemos que cada um dos dois números primos tem

bits.

n

$n$

Amir

c_{2 n - 2}

$c_{2n−2}$

E quanto a RSA-129

Ilya Gazman 28/11/2013

18

Estendendo o que a @Amir escreveu, me deparei com a boa página da web a seguir, que hospeda um gerador de CNF para circuitos de fatoração que, por exemplo, poderia ser executado em alguns dos números (agora inativos) do Desafio de Factoring RSA (agora inativos) . As instâncias geradas estão em DIMACS formato que pode ser directamente alimentado a qualquer um dos concorrentes atuais na anual SAT solver competição . Em relação às instâncias difíceis do SAT em geral, os problemas de referência apresentados no site da competição do SAT parecem ser bastante úteis, também a classificação em aleatório / trabalhada / industrial é boa.

Martin Schwarz
fonte

1

Esse link é muito legal!

Huck Bennett 28/05

Se você realmente tentar inserir um desses números, verá que o código-fonte usa o tipo de dados int e, portanto, pode conter apenas números de 32 bits, enquanto os números RSA não executados começam em centenas de bits.

Elliot Gorokhovsky

11

Aqui está um artigo sobre a geração de instâncias SAT a partir de fatoração:

Horie, S. & Watanabe, O. [1997] " Hard instance generation for SAT " Algoritmos e computação 1350: 22-31 ( pdf )

$n^2$

Lou Scheffer
fonte

9

O ToughSat de Henry Yuen e Joseph Bebel é outra ferramenta semelhante à vinculada por @Martin, que gera fórmulas CNF que codificam instâncias de fatoração e outros problemas difíceis.

Alessandro Cosentino
fonte

1

Scott blog sobre isso também: scottaaronson.com/blog/?p=676

Alessandro Cosentino

0

Veja satfactor:

Converter fatoração inteira em um problema booleano de SATISFIABILITY

Shane Neph

visão global

Os fatores determinantes de um número inteiro grande são de interesse do Homem desde pelo menos o tempo de Euclides. Não existe um algoritmo geral conhecido para esse problema que seja escalonado em tempo menor que exponencial em relação ao número de bits necessários para representar o número inteiro.

O que esse código faz

Converte um problema de fatoração inteiro em um problema booleano de SATISFIABILITY. Se o problema for resolvido por um solucionador SAT, ele extrai os fatores inteiros.

Os solucionadores de satisfação da Boolen melhoram a cada ano. A cada 2 anos, ocorre uma competição internacional entre solucionadores (consulte http://www.satcompetition.org/ e http://www.satlive.org/ ). Até que ponto esses solucionadores de última geração podem se sair contra um dos mais antigos problemas de matemática abertos existentes?

Este projeto tem 2 objetivos principais:
1) Converta o problema e fatore um número inteiro de interesse!
2) Crie rapidamente um problema de SATISFIABILIDADE solucionável ou insolúvel, cuja dificuldade é facilmente controlada pelo criador.
- Para criar um problema insatisfatório de SATISFIABILITY, basta codificar um número primo.
- Para criar problemas mais difíceis, mas solucionáveis, escolha números compostos maiores com menos fatores.

O número de interesse pode ser de qualquer tamanho!

Existem alguns solucionadores de SATISFIABILITY de código aberto. Vejo http://www.satlive.org/ para alguns deles.

Construir

make -C src /

Como

Insira um número de interesse em sua forma binária:

bin / iencode 10101> composite.21
// resolva com seu solucionador favorito e coloque resultados em solution.txt
bin / extract-sat composite.21 solution.txt

A saída seria:
00011
00111

que são representações binárias para números inteiros decimais 3 e 7, os fatores de 21.

Se um número inteiro de entrada tiver mais de 2 fatores e o problema SAT for resolvido, a saída será apenas dois dos fatores. Esses podem não ser números primos (você pode testar isso facilmente no Maxima, Maple ou Mathematica).

Nem todos os solucionadores SAT produzem resultados no mesmo formato. Pode ser necessário medicar esses resultados levemente. extract-sat requer um arquivo de solução contendo uma lista de números inteiros (em qualquer número de linhas). Por exemplo,

1 -2 3 4 -5 ...

Geremia
fonte

1

Você pode resumir as técnicas usadas por este software? Neste site, estamos mais interessados em algoritmos e técnicas do que em um anúncio de uma ferramenta de software. Por exemplo, as perguntas para a complexidade da redução. Não vejo como você abordou a questão; nos sites Stack Exchange, você deve responder apenas se puder responder à pergunta específica que foi feita. Além disso, você tem algum relacionamento com a ferramenta ou com seus autores?

DW

Redução rápida de RSA para SAT

Respostas:

Converter fatoração inteira em um problema booleano de SATISFIABILITY

visão global

O que esse código faz

Construir

Como