Einzigartige

Diese Frage befindet sich wahrscheinlich an der Grenze zwischen "on-topic" und "off-topic". Allerdings habe ich hier ähnliche Fragen gesehen, daher werde ich sie stellen.

Ich implementiere einen eindeutigen $k$ SAT-Löser, dessen Eingabe eine $k$ CNF-Formel mit höchstens $1$ befriedigender Zuordnung ist. Um sein praktisches Verhalten zu testen, benötige ich eine Reihe solcher Formeln. Ich habe im Internet nach ihnen gesucht und nichts gefunden (während es andererseits sehr einfach ist, Reihen gewöhnlicher $k$ CNF-Formeln zu finden).

Wo finde ich Unique $k$ -SAT-Instanzen?

Alternativ wäre ich auch damit zufrieden, eine Prozedur zu kennen, um eindeutig befriedigende Instanzen zu erzeugen. Der einzige Ansatz, der mir bekannt ist, wird als " Planted-SAT-Instanz-Generierung" bezeichnet : Sie generieren zufällig eine Zuweisung von $n$ Variablen, dann generieren Sie nur die Klauseln, die mit einer solchen Zuweisung übereinstimmen. Dieser Ansatz ist aus folgenden Gründen für meine Zwecke unbefriedigend:

• Die erhaltene Formel kann weitere unerwünschte zufriedenstellende Zuordnungen aufweisen.
• Um sicherzustellen, dass die Formel durch die gewünschte Zuweisung eindeutig erfüllt wird, sollten Sie alle möglichen Klauseln einführen, die damit übereinstimmen. Dies würde zu Formeln mit zu vielen Klauseln führen, die wahrscheinlich leicht zu lösen sind und daher nicht für das Worst-Case-Verhalten des Lösers repräsentativ sind. Mir ist nicht klar, wie wir die Eindeutigkeit wirksam erzwingen und gleichzeitig die Anzahl der Klauseln vernünftig halten können.

Wie können wir eindeutig erfüllbare Formeln mit einer angemessenen Anzahl von Klauseln erzeugen? Mit vernünftig meine ich weit entfernt vom Maximum .$2^k \cdot {n \choose k}$

Hier ist eine Möglichkeit, eine eindeutige SAT-Instanz zu generieren, vorausgesetzt, eine SAT-Instanz , von der Sie wissen, dass sie erfüllt werden kann . Betrachten Sie die Formel vonφ ψ ( x $k$$\varphi$$\psi(x)$

Dabei ist eine Hash-Funktion, die eine Zuordnung zu einem Bit-Wert (für einen kleinen Wert von ) abbildet , und ist ein zufälliger Bit-Wert. Wenn ungefähr befriedigende Zuweisungen hat, nehmen wir (heuristisch) an, dass genau eine befriedigende Zuweisung hat (mit konstanter Wahrscheinlichkeit). Wir können testen, ob dies der Fall ist, indem wir einen SAT-Löser verwenden (nämlich testen, ob erfüllbar ist; wenn dies der Fall ist und eine erfüllende Zuweisung ist, testen Sie, ob erfüllbar ist). Wennx k k y k φ 2 k ψ ψ x 0 ψ ( x ) ∧ x ≠ x 0 k k k = 1 , 2 , ... , n n $h$$x$$k$$k$$y$$k$$\varphi$$2^k$$\psi$$\psi$$x_0$$\psi(x) \land x \ne x_0$$k$Ist dies nicht bekannt, können Sie mit der binären Suche oder durch Iteration über jeden Kandidatenwert (wobei die Anzahl der booleschen Variablen in ) finden.$k$$k=1,2,\dots,n$$n$$x$

Sie können die Hash-Funktion frei wählen. Sie werden es wahrscheinlich so einfach wie möglich machen wollen. Eine sehr einfache Konstruktion ist zu haben eine zufällige Teilmenge von auszusuchen Bits von . Eine etwas komplexere Konstruktion besteht darin, dass das te Bit von das oder von zwei zufällig ausgewählten Bits von (wobei für jedes unabhängig ein separates Paar von Bitpositionen gewählt wird ). Wenn Sie einfach halten, bleibt relativ einfach.k x i h ( x ) x i h $h$$k$$x$$i$$h(x)$$x$$i$$h$$\psi$

Diese Art der Transformation wird manchmal als Teil eines Schemas zum Schätzen der Anzahl zufriedenstellender Zuordnungen zu einer Formel verwendet / vorgeschlagen ; Ich habe es für Ihre besonderen Bedürfnisse angepasst.$\varphi$

Sie können im Internet viele Testbeds von SAT-Instanzen finden und diese Transformation auf alle anwenden, um eine Sammlung eindeutiger SAT-Instanzen zu erhalten.$k$

Eine andere Möglichkeit wäre, eindeutige SAT-Instanzen aus der Kryptographie zu generieren . Angenommen, ist eine kryptografische Einwegpermutation. Sei ein zufällig ausgewähltes Element von und sei . Dann ist die durch gegebene Formel eine eindeutige SAT-Instanz. Wählen Sie als weiteres Beispiel zwei große Primzahlen zufällig aus und lassen Sie . Dann ist die Formel gegeben durchf : { 0 , 1 } n → { 0 , 1 } n x { 0 , 1 } n y = f ( x ) φ ( x ) f ( x ) = y k p , q n = p q φ ( x , y ) x ≤ y = n ≤ x $k$$f:\{0,1\}^n \to \{0,1\}^n$$x$$\{0,1\}^n$$y=f(x)$$\varphi(x)$$f(x)=y$$k$$p,q$$n=pq$$\varphi(x,y)$$x \cdot y = n \land x>1 \land y>1 \land x \le y$(mit der offensichtlichen Entsprechung zwischen Bitfolgen und ganzen Zahlen) ist eine eindeutige SAT-Instanz. Diese Konstruktionen scheinen jedoch kein nützlicher Weg zu sein, um Ihren Solver zu bewerten oder zu optimieren. Sie alle haben eine spezielle Struktur, und es gibt keinen Grund zu der Annahme, dass diese Struktur für Probleme der realen Welt repräsentativ ist. Insbesondere SAT-Instanzen, die aus kryptografischen Problemen stammen, sind bekanntermaßen extrem schwer, viel schwerer als SAT-Instanzen, die aus vielen anderen realen Anwendungen von SAT-Lösern stammen. Sie sind daher keine sehr gute Grundlage für das Benchmarking Ihres Lösers.$k$

Im Allgemeinen weisen alle in dieser Antwort erwähnten Techniken den Nachteil auf, dass sie eindeutige SAT-Instanzen mit einer bestimmten Struktur generieren , sodass sie möglicherweise nicht das sind, wonach Sie suchen - oder zumindest nicht vertrauen möchten nur auf Formeln, die auf diese Weise erzeugt werden. Ein besserer Ansatz wäre es, Anwendungen von Unique SAT zu identifizieren (von wem und zu welchem ​​Zweck wird Ihr Solver verwendet?) Und dann zu versuchen, einige realistische Beispiele aus diesen Anwendungsdomänen zu erhalten.$k$$k$

Zu einem verwandten Thema siehe auch Generieren interessanter kombinatorischer Optimierungsprobleme

Sie könnten die Algorithmen in Betracht ziehen, die zum Generieren von Sudoku-Rätseln verwendet werden - vermutlich verallgemeinert auf -, da (normalerweise) Sudoku-Rätsel eine eindeutige Lösung haben sollen. Auf der anderen Seite ist auch Sudoku - Rätsel in der Regel garantiert mindestens eine Lösung haben ... Aber diese Lösung zu finden , immer noch ein guter Maßstab für Ihren Löser sein könnte.$n \times n$

Möglicherweise verwenden Sie einen Sudoku-Generator zusammen mit einer Reduzierung auf SAT, oder Sie überlegen, wie Sie die in der Sudoku-Generierung verwendeten Techniken anwenden können, um eindeutige SAT-Instanzen direkter zu generieren. Bei ersteren haben Ihre SAT-Instanzen offensichtlich eine gewisse Struktur, aber mir ist nicht klar, ob es sich um mehr oder weniger Struktur handelt, als z. B. eine Lösung zu pflanzen oder die Zeugenisolationstechnik zu verwenden. Kommt wahrscheinlich auf deine Bedürfnisse und deinen Löser an.

Die einzige Referenz, die ich hier kenne, ist: Sudoku Puzzles Generieren: von einfach bis böse .

Ich denke, ein guter Testfall wäre, zufällige, eindeutig erfüllbare 3XOR-Instanzen (gepflanzte Instanzen) mit -Einschränkungen zu generieren und diese dann in 3SAT-Instanzen zu konvertieren.$\Theta(n)$

$(1,p),(p,1)$$a<b$$a \neq 1$$b \neq p$

Auch mit diesem Ansatz ist es relativ einfach, Zahlen zu finden, mit ungefähr jedoch vielen Faktoren / Lösungen sind erwünscht. die „weichere“ die Zahl, desto mehr Faktoren.

Verschiedene Forscher haben im Laufe der Jahre diesen Factoring-SAT-Code erstellt (z. B. für DIMACS competition / arcihve, in dem in der Vergangenheit einige Factoring-Instanzen gespeichert waren), aber leider scheint es keine öffentlich zugängliche Version zu geben. Siehe auch den 1. Link unten für einen Verweis, wo der Code anscheinend für einen Abschlusskurs geschrieben / implementiert wurde.

• Reduzieren des Ganzzahlfaktorisierungsproblems auf ein NP-Complete-Problem
• Beispiel für die Generierung einer 3SAT-Schaltung zur Faktorisierung ganzer Zahlen

$e_n$$e_{n+1}$$e_{n+1}$$e_n$

Sie können leicht eindeutige SAT-Formeln mit einer angemessenen Größe direkt generieren.$(|F|<n+2^k)$

$m$$m$
$F$$k$$m$$F$$m$$(2^k-1) \binom{n}{k}$

$\binom{k}{1}$$x_1,x_2 \ldots x_k$
$(\lnot x_1, x_2 \ldots x_k)(x_1, \lnot x_2 \ldots x_k)\ldots (x_1,x_2 \ldots \lnot x_k)$

$\binom{k}{2}$$x_1,x_2 \ldots x_k$
$(\lnot x_1, \lnot x_2, x_3 \ldots x_k)(\lnot x_1,x_2, \lnot x_3 \ldots x_k)\ldots (x_1,x_2 \ldots \lnot x_{k-1} \lnot x_k)$

Fahren Sie fort, bis Sie die einzige -Klausel verwenden, die alle Modelle eliminiert, die jeder Variablen unter eine "1" zuweisen .$\binom{k}{k}$$x_1,x_2 \ldots x_k$

Die einzigen Modelle, die noch nicht eliminiert sind, weisen alle "0" zu. Da ein Modell ist, dann auf eine beliebige Menge von Klauseln , die alle Modelle Zuordnung "1" zu eliminieren und auf alle Variablen unter , zum Beispiel: .$x_1,x_2 \ldots x_k$$m$$n-k$$x_i (k<i\leq n)$$0$$k-1$$x_1,x_2 \ldots x_k$
$(\lnot x_{k+1}, x_1 \ldots, x_{k-1}) \ldots (\lnot x_n, x_1 \ldots x_{k-1})$

Dann ist$|F|=\sum_{i=1}^k \binom{k}{i} +n-k = 2^k-1+n-k$

Um mehr Klauseln zu erhalten, fügen Sie eine beliebige Klausel hinzu, die mindestens eine negierte Variable enthält. Um eine unbefriedigende Formel zu erhalten, fügen Sie einfach eine Klausel mit getrennten Variablen hinzu.$k$