28

Scott Aaronsons heutiger Blogbeitrag enthielt eine Liste von interessanten offenen Problemen / Aufgaben in der Komplexität. Besonders eines hat meine Aufmerksamkeit erregt:

Erstellen Sie eine öffentliche Bibliothek von 3SAT-Instanzen mit möglichst wenigen Variablen und Klauseln, deren Lösung bemerkenswerte Konsequenzen hätte. (Zum Beispiel Instanzen, die die RSA-Faktorisierungsherausforderungen codieren.) Untersuchen Sie die Leistung der besten aktuellen SAT-Löser in dieser Bibliothek.

Dies hat meine Frage aufgeworfen: Was ist die Standardtechnik, um RSA / Factoring-Probleme auf SAT zu reduzieren, und wie schnell ist sie? Gibt es eine solche Standardreduzierung?

Nur um klar zu sein, mit "schnell" meine ich keine Polynomzeit. Ich frage mich, ob wir der Komplexität der Reduktion engere Grenzen gesetzt haben. Gibt es zum Beispiel eine bekannte kubische Reduktion?

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

26

Ein Ansatz zum Codieren von Faktor (RSA) zu SAT besteht in der Verwendung von Multiplikatorschaltungen (jede Schaltung kann als CNF codiert werden).

Nehmen wir an, wir erhalten eine ganze Zahl mit Bits, . Wir sind daran interessiert, zwei Bit-Ganzzahlen und deren Produkt . $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$

Die naivste Kodierung kann ungefähr so aussehen: Wir wissen das

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

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

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

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

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

Dann kann unter Verwendung der Tseitin-Transformation die obige Codierung in CNF übersetzt werden.

Dieser Ansatz erzeugt einen relativ kleinen CNF. Diese Codierung unterstützt jedoch nicht "Unit Propagation" und daher ist die Leistung von SAT-Solvern wirklich schlecht.

Es gibt andere Schaltkreise zur Multiplikation, die für diesen Zweck verwendet werden können, aber sie erzeugen einen größeren CNF.

Amir
quelle

10

In Abschnitt 6.1 von "Finden von harten Instanzen des Erfüllbarkeitsproblems: Eine Umfrage" von Cook und Mitchell verwenden sie dieses Problem als Herausforderung.

Amir

Woher wissen Sie, dass A und B eine Länge von n Bits haben müssen, können es nicht n - 1 und und n Bits sein? Natürlich kann es 2n Bits und 1 Bit sein.

Ilya Gazman

1

@Babibu: Wenn wir über die allgemeine Faktorisierung sprechen, haben Sie recht. Im Fall von RSA wissen wir jedoch, dass jede der beiden Primzahlen Bits hat.

n

$n$

Amir

c_{2 n - 2}

$c_{2n−2}$

Was ist mit RSA-129

Ilya Gazman

18

Als ich das, was @Amir schrieb, erweiterte, stieß ich auf die folgende nette Webseite, auf der sich ein CNF-Generator für Factoring-Schaltungen befindet , die man zB auf einigen der (jetzt inaktiven) RSA Factoring Challenge- Nummern ausführen kann . Die generierten Instanzen sind im DIMACS- Format, das direkt an einen der aktuellen Wettbewerber des jährlichen SAT- Solver- Wettbewerbs gesendet werden kann . In Bezug auf harte SAT-Instanzen im Allgemeinen scheinen die Benchmark-Probleme, die auf der Website des SAT-Wettbewerbs angegeben wurden, sehr nützlich zu sein.

Martin Schwarz
quelle

1

Dieser Link ist sehr cool!

Huck Bennett

Wenn Sie tatsächlich versuchen, eine dieser Zahlen einzugeben, werden Sie feststellen, dass der Quellcode den Datentyp int verwendet und daher nur 32-Bit-Zahlen enthalten kann, während die nicht faktorisierten RSA-Zahlen bei Hunderten von Bits beginnen.

Elliot Gorokhovsky

11

Hier ist ein Artikel zum Generieren von SAT-Instanzen aus Factoring:

Horie, S. & Watanabe, O. [1997] " Hard instance generation for SAT " Algorithmen und Berechnung 1350: 22-31 ( pdf )

$n^2$

Lou Scheffer
quelle

9

ToughSat von Henry Yuen und Joseph Bebel ist ein weiteres Tool, das dem von @Martin ähnelt und CNF-Formeln generiert, die Instanzen von Factoring und andere schwierige Probleme codieren.

Alessandro Cosentino
quelle

1

Scott hat auch darüber gebloggt

Alessandro Cosentino

0

Siehe satfactor:

Konvertieren Sie die ganzzahlige Faktorisierung in ein boolesches Problem der ZUFRIEDENHEIT

Shane Neph

Überblick

Das Bestimmen von Faktoren mit einer großen ganzen Zahl ist seit mindestens Euklids Zeit für den Menschen von Interesse. Es ist kein allgemeiner Algorithmus für dieses Problem bekannt, der in Bezug auf die Anzahl der zur Darstellung der Ganzzahl benötigten Bits in weniger als exponentieller Zeit skaliert.

Was macht dieser Code?

Konvertiert ein Ganzzahlfaktorisierungsproblem in ein boolesches SATISFIABILITY-Problem. Wenn das Problem von einem SAT-Löser gelöst wird, werden die ganzzahligen Faktoren extrahiert.

Die Zufriedenheitslöser von Boolen verbessern sich jedes Jahr. Alle 2 Jahre findet ein internationaler Wettbewerb zwischen Solvern statt (siehe http://www.satcompetition.org/ und http://www.satlive.org/ ). Wie gut können diese hochmodernen Löser eines der ältesten offenen mathematischen Probleme lösen, die es gibt?

Dieses Projekt hat zwei Hauptziele:
1) Konvertieren Sie das Problem und faktorieren Sie eine ganze Zahl von Interesse!
2) Erstellen Sie schnell entweder ein lösbares oder ein unlösbares ZUFRIEDENHEITS-Problem, dessen Schwierigkeit vom Entwickler leicht kontrolliert werden kann.
- Um ein unlösbares SATISFIABILITY-Problem zu erstellen, codieren Sie einfach eine Primzahl.
- Um schwierigere, aber lösbare Probleme zu erzeugen, wählen Sie größere zusammengesetzte Zahlen mit weniger Faktoren.

Die Anzahl der Interessenten kann beliebig groß sein!

Es gibt einige Open-Source-Löser für ZUFRIEDENHEIT. Einige davon finden Sie unter http://www.satlive.org/ .

Bauen

make -C src /

Wie man

Geben Sie eine Anzahl von Interessen in binärer Form ein:

bin / iencode 10101> composite.21
// Löse mit deinem Lieblingslöser und füge die Ergebnisse in die Datei solution.txt ein
bin / extract-sat composite.21 solution.txt

Der Ausgang wäre:
00011
00111

Dies sind Binärdarstellungen für die Dezimalzahlen 3 und 7, die Faktoren von 21.

Wenn eine Eingabe-Ganzzahl mehr als 2 Faktoren enthält und das SAT-Problem gelöst ist, werden nur zwei der Faktoren ausgegeben. Dies sind möglicherweise keine Primzahlen (Sie können dies problemlos in Maxima, Maple oder Mathematica testen).

Nicht alle SAT-Solver-Ausgaben haben dasselbe Format. Möglicherweise müssen Sie diese Ergebnisse leicht behandeln. Für extract-sat ist eine Lösungsdatei mit einer Liste von Ganzzahlen (in beliebig vielen Zeilen) erforderlich. Beispielsweise,

1 -2 3 4 -5 ...

Geremia
quelle

1

Können Sie die von dieser Software verwendeten Techniken zusammenfassen? Auf dieser Seite interessieren uns mehr Algorithmen und Techniken als Werbung für ein Software-Tool. Zum Beispiel die Fragen nach der Komplexität der Reduktion. Ich verstehe nicht, wie Sie die Frage angesprochen haben. Auf Stack Exchange-Sites sollten Sie nur antworten, wenn Sie die gestellte Frage beantworten können. Haben Sie auch irgendeine Beziehung zu dem Tool oder seinen Autoren?

DW

Schnelle Reduktion von RSA zu SAT

Antworten:

Konvertieren Sie die ganzzahlige Faktorisierung in ein boolesches Problem der ZUFRIEDENHEIT

Überblick

Was macht dieser Code?

Bauen

Wie man