28

Wpis na blogu Scotta Aaronsona przedstawił dziś listę interesujących otwartych problemów / zadań w złożoności. Jeden zwrócił moją uwagę:

Zbuduj bibliotekę publiczną instancji 3SAT z jak najmniejszą liczbą zmiennych i klauzul, które mogłyby mieć godne uwagi konsekwencje, jeśli zostaną rozwiązane. (Na przykład, instancje kodujące wyzwania faktoringu RSA.) Zbadaj wydajność najlepszych obecnych solverów SAT w tej bibliotece.

To wywołało moje pytanie: jaka jest standardowa technika redukcji problemów RSA / faktoringu do SAT i jak szybka jest? Czy istnieje taka standardowa redukcja?

Żeby było jasne, przez „szybki” nie mam na myśli czasu wielomianowego. Zastanawiam się, czy mamy ściślejsze górne granice złożoności redukcji. Na przykład, czy istnieje znana redukcja sześcienna?

— Huck Bennett
źródło

26

Jednym ze sposobów kodowania faktoringu (RSA) do SAT jest użycie obwodów multiplikatora (każdy obwód może być kodowany jako CNF).

Załóżmy, że otrzymaliśmy liczbę całkowitą z bitami, . Nas interesuje znalezienia dwóch -bitowe liczby całkowite i , którego produkt jest . $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$

Najbardziej naiwne kodowanie może być takie: Wiemy o tym

c_{2 n} = a_{n} \land b_{n}

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

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

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

C a r r y : d_{2 n - 1} = (a_{n} \land b_{n - 1}) \land (a_{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} = (a_{n} \land b_{n - 2}) x o r (a_{n - 1} \land b_{n - 1}) x o r (a_{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}$ ...

Następnie za pomocą transformacji Tseityny powyższe kodowanie można przetłumaczyć na CNF.

Takie podejście powoduje stosunkowo niewielki CNF. Ale to kodowanie nie obsługuje „propagacji jednostek”, a zatem wydajność solverów SAT jest naprawdę zła.

Istnieją inne obwody do mnożenia, które można wykorzystać do tego celu, ale wytwarzają one większy CNF.

— Amir
źródło

10

W sekcji 6.1 „Znajdowanie trudnych przypadków problemu satysfakcji: ankieta” Cooka i Mitchella wykorzystują ten problem jako wyzwanie.

— Amir

Skąd wiesz, że A i B muszą mieć długość n bitów, czy nie może to być n - 1 oraz n bitów? Na pewno może to być 2n bitów i 1 bit.

— Ilya Gazman

1

@Babibu: Jeśli mówimy o ogólnym rozkładaniu na czynniki pierwsze, masz rację. Ale w przypadku RSA wiemy, że każda z dwóch liczb pierwszych ma bitów.

n

$n$

— Amir

Rozumiem, że odpowiadasz, ale nie wiem, jak to kontynuować. Czy możesz pokazać .

c_{2 n - 2}

$c_{2n−2}$

— Ilya Gazman

Co z RSA-129

— Ilya Gazman

18

Rozszerzając to, co napisał @Amir, natknąłem się na następującą ładną stronę internetową, na której znajduje się generator CNF do faktorowania obwodów, które można np. Uruchamiać na niektórych (obecnie nieaktywnych) numerach RSA Factoring Challenge . Wygenerowane instancje są w formacie DIMACS , które można bezpośrednio przekazywać dowolnemu z aktualnych konkurentów w corocznym konkursie na solver SAT . Ogólnie rzecz biorąc, jeśli chodzi o twarde instancje SAT, problemy z testami porównawczymi podane na stronie konkursowej SAT wydają się być całkiem użyteczne, fajna jest również klasyfikacja na losową / wytworzoną / przemysłową.

— Martin Schwarz
źródło

1

Ten link jest bardzo fajny!

— Huck Bennett

Jeśli faktycznie spróbujesz wprowadzić jedną z tych liczb, przekonasz się, że ich kod źródłowy używa typu danych int, a zatem może przechowywać tylko liczby 32-bitowe, podczas gdy niezbadane liczby RSA zaczynają się od setek bitów.

— Elliot Gorokhovsky,

11

Oto artykuł na temat generowania instancji SAT z faktoringu:

Horie, S. & Watanabe, O. [1997] „ Generowanie twardych instancji dla SAT ” Algorytmy i obliczenia 1350: 22-31 ( pdf )

Jest gorszy niż liniowy, ale lepszy niż . 512-bitowy numer typu wyzwania RSA generuje instancję z 63 652 zmiennymi i 406 860 klauzul. $n^2$

— Lou Scheffer
źródło

9

ToughSat Henry Yuen i Joseph Bebel to kolejne narzędzie podobne do tego, które łączy @Martin, które generuje formuły CNF, które kodują przypadki faktoringu i innych trudnych problemów.

— Alessandro Cosentino
źródło

1

Scott również pisał o tym na blogu

— Alessandro Cosentino

0

Zobacz satfactor:

Przekształć faktoryzację całkowitą w boolowski problem ZADOWOLENIA

Shane Neph

Przegląd

Czynniki determinujące dużą liczbę całkowitą były przedmiotem zainteresowania Człowieka przynajmniej od czasów Euclida. Nie ma znanego ogólnego algorytmu dla tego problemu, który skaluje się w czasie krótszym niż wykładniczy w odniesieniu do liczby bitów potrzebnych do przedstawienia liczby całkowitej.

Co robi ten kod

Przekształca problem faktoryzacji liczb całkowitych w boolowski problem ZADOWOLENIA. Jeśli problem rozwiązuje solver SAT, wówczas wyodrębnia czynniki całkowite.

Boolen solvery satysfakcji poprawiają się z każdym rokiem. Co 2 lata odbywa się międzynarodowy konkurs między solverami (patrz http://www.satcompetition.org/ i http://www.satlive.org/ ). Jak dobrze te najnowocześniejsze solwery radzą sobie z jednym z najstarszych istniejących problemów otwartej matematyki?

Ten projekt ma 2 główne cele:
1) Przekształć problem i uwzględnij liczbę całkowitą będącą przedmiotem zainteresowania!
2) Szybko stwórz rozwiązywalny lub nierozwiązywalny problem ZADOWOLENIA, którego trudnością łatwo steruje twórca.
- Aby stworzyć nierozwiązywalny problem SATYSFIABILNOŚCI, po prostu zakoduj liczbę pierwszą.
- Aby stworzyć trudniejsze, ale możliwe do rozwiązania problemy, wybierz większe liczby zespolone z mniejszą liczbą czynników.

Liczba odsetek może być dowolnej wielkości!

Istnieje kilka rozwiązań SATYSFIABILITY typu open source. Niektóre z nich można znaleźć na stronie http://www.satlive.org/ .

Budować

make -C src /

Jak

Wprowadź liczbę zainteresowań w formie binarnej:

bin / iencode 10101> composite.21
// rozwiązuj za pomocą swojego ulubionego solvera i umieść wyniki w solution.txt
bin / extract-sat composite.21 solution.txt

Wynik wyniósłby:
00011
00111

które są reprezentacjami binarnymi dla liczb całkowitych dziesiętnych 3 i 7, współczynniki 21.

Jeśli wejściowa liczba całkowita ma więcej niż 2 czynniki, a problem SAT został rozwiązany, wyjście będzie tylko dwoma z czynników. Mogą to nie być liczby pierwsze (możesz to łatwo sprawdzić w Maxima, Maple lub Mathematica).

Nie wszystkie dane wyjściowe solverów SAT mają ten sam format. Konieczne może być lekceważenie tych wyników. extract-sat wymaga pliku rozwiązania zawierającego listę liczb całkowitych (w dowolnej liczbie wierszy). Na przykład,

1 -2 3 4 -5 ...

— Geremia
źródło

1

Czy potrafisz podsumować techniki stosowane przez to oprogramowanie? W tej witrynie bardziej interesują nas algorytmy i techniki niż reklama oprogramowania. Na przykład pytania dotyczące złożoności redukcji. Nie widzę odpowiedzi na pytanie; na stronach Stack Exchange powinieneś odpowiedzieć tylko wtedy, gdy możesz odpowiedzieć na zadane pytanie. Czy masz też jakieś relacje z narzędziem lub jego autorami?

— DW

Szybka redukcja z RSA do SAT

Przekształć faktoryzację całkowitą w boolowski problem ZADOWOLENIA

Przegląd

Co robi ten kod

Budować

Jak