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?
źródło
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ą.
źródło
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.n2
źródło
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.
źródło
Zobacz
satfactor
:Przekształć faktoryzację całkowitą w boolowski problem ZADOWOLENIA
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 ...
źródło