Lösung eines Weihnachtsmann-SAT-Problems mit Classiq

Willkommen zu meinem dritten Blog in dieser Serie über die Lösung eines Wichtelproblems mit Quantencomputern. 

Dieses Jahr möchte ich zeigen, wie einfach es ist, mit der Classiq-Plattform Q#-Code zur Lösung des Problems zu erzeugen.

Dieser Blog ist Teil des Q# Ferienkalenders 2022.

Schauen wir uns zunächst an, was das Problem war.

Wir haben 3 oder mehr Leute, die das Wichteln spielen wollen. Alle schreiben ihren Namen auf einen Zettel, und alle Zettel kommen in eine Schüssel. Nach dem Mischen wählt jeder Spieler einen Zettel aus, und da niemand seinen eigenen Namen hat, hat jeder Spieler einen Namen, für den er ein Geschenk kaufen und/oder ein Gedicht schreiben muss.

Dies lässt sich anhand dieser Tabelle leicht veranschaulichen, in diesem Fall haben wir 3 Spieler.

In diesem Fall, wenn X1 = 1 ist, muss Vincent Shai ein Geschenk kaufen.

Um dieses Problem zu lösen, muss man genau einen Wert in jeder Zeile und jeder Spalte haben. Wir können dies als SAT-Problem wie folgt schreiben:

(X1⊕X2)∧(X3⊕X4)∧(X5⊕X6)∧(X3⊕X5)∧(X1⊕X6)∧(X2⊕X4)

Eine ausführlichere Beschreibung finden Sie in meinem ersten Blogbeitrag hier.

Classiq einführen

Classiq ermöglicht es den Endnutzern, effiziente logische Quantenschaltungen in einer Hochsprache zu erzeugen. Wir können die Classiq-Plattform nutzen, um eine Schaltung zu erzeugen, die diese Aufgabe lösen kann, ohne über Qubits oder gatterbasierte Programmierung auf niedriger Ebene nachzudenken. Wir können entweder das Python-SDK, das wir im Folgenden verwenden werden, oder ein textuelles Modell verwenden, um diese logischen Quantenschaltungen zu erstellen.

Schauen wir uns an, wie wir dies tun können.

Erstellen wir zunächst die SAT-Formel als Python-String:

Formel = """(    
    ( ( x1) ^ ( x2) ) und
    ( ( x3) ^ ( x4) ) und
    ( ( x5) ^ ( x6) ) und
    ( ( x3) ^ ( x5) ) und
    ( ( x1) ^ ( x6) ) und
    ( ( x2) ^ ( x4) ))"""

Als Nächstes wollen wir ein Arithmetik-Orakel erstellen, um das SAT-Problem zu lösen:

# Each value can either be 0 or 1 so we use a register size of 1 
qubit.register_size = RegisterUserInput(size=1)

# To solve the SAT problem here we are going to do a search using the Grover method.
# We define the register size per variable, in this case that is always 1.
# Lastly we can either use a “Naive” or “Optimized” approach for uncomputating and freeing intermediate qubits,
# here we use “naive” for clarity of the solution.

grover_params = GroverOperator(
	oracle=ArithmeticOracle(        
  	expression=formula,        
    definitions={
      "x1": register_size,
      "x2": register_size,
      "x3": register_size,
      "x4": register_size,
      "x5": register_size,
      "x6": register_size
    },        
    uncomputation_method="naive"    
  )
)

Was wir hier sehen, ist, dass wir zuerst die Registergröße auf 1 setzen, was bedeutet, dass jede Variable nur den Wert 1 oder 0 annehmen kann. Als nächstes laden wir die Formel in das ArithmeticOracle.

Um daraus tatsächlich eine Schaltung zu erstellen, übergeben wir dieses Orakel wie folgt an Classiqs Synthese-Engine:

# Wir wollen die Anzahl der verwendeten Qubits minimieren, also optimieren wir für die Breite
constraints = Constraints(optimization_parameter="width")
preferences = Preferences(backend_service_provider="Azure Quantum", backend_name="Ionq",output_format=["qs"]
model_designer = ModelDesigner()
model_designer.GroverOperator(grover_params)
circuit = model_designer.synthesize(constraints=constraints,preferences=preferences)

Hier geschehen mehrere Dinge, die wir kurz durchgehen wollen:

• Zunächst definieren wir einen Optimierungsparameter. Dieser weist die Synthese-Engine an, den Schaltkreis zu erstellen, der die geringste Anzahl von Qubits benötigt. 
• Zweitens geben wir die Spezifikation des Backends an die Synthese-Engine weiter. Dadurch wird sichergestellt, dass wir nicht mehr Qubits verwenden, als das Gerät hat. Das Gerät, das wir hier ausgewählt haben, ist das Ionq.qpu-Gerät in Azure Quantum. Außerdem optimieren wir die Schaltung unter Berücksichtigung des nativen unterstützten Gattersets und der QPU-Topologie. Hier geben wir auch das Ausgabeformat an und sagen, dass wir Q#-Code als Ausgabe erhalten möchten.
• Als nächstes fügen wir das Orakel zu unserer ModelDesiger-Instanz hinzu.
• Schließlich erstellen wir die Schaltung anhand der Funktionalität, des Orakels und der Beschränkungen/Präferenzen.

Werfen wir einen Blick auf das Oracle nach der Ausführung der Synthese-Engine, die unten oder hier generiert wird.

Da wir nun das Orakel haben, wollen wir uns auch den Q#-Code für dieses Orakel ansehen. 

Mit 'schaltung.qsharp' können wir den generierten Q#-Code abrufen, der hier verfügbar ist.

Nun, da wir alles vorbereitet haben, ist es an der Zeit, das Programm auszuführen, was folgendermaßen geschehen kann:

cred = AzureCredential(
    tenant_id="",
    client_id="",
    client_secret="",
)

azure_preferences = AzureBackendPreferences(
    backend_name="ionq.simulator",
    credential=cred,
    location="",
    resource_id="",
)


res_azure = Executor(
    backend_preferences=azure_preferences
).execute(Schaltung)

Jetzt sind Sie neugierig, wer wem ein Geschenk machen muss, also hier ist die Ausgabe, die Sie mit 'res.result':

{'X1': 0.0, 'X2': 1.0, 'X3': 1.0, 'X4': 0.0, 'X5': 0.0, 'X6': 1.0}

Das bedeutet, dass Vincent ein Geschenk für Simon, Shai ein Geschenk für Vincent und Simon ein Geschenk für Shai besorgen wird.

Dies zeigt, wie einfach realer, funktionaler Q#-Code mit der Classiq-Plattform generiert und ausgeführt werden kann.