Kaboom: ein ungewöhnlicher Pionier



Als Kind saß ich dreimal pro Woche anderthalb Stunden bei der Arbeit meines Vaters. Ich durfte an einen Computer gehen, wo es von der Unterhaltung nur einen Pionier und Farbe gab. Ich hatte es satt, schnell zu zeichnen, aber der Wunsch, das gesamte Feld zu öffnen und nicht zu explodieren, motivierte mich, nach neuen und neuen Wegen zu suchen, um dieses Spiel zu spielen. Viele Jahre später stieß ich versehentlich auf einen interessanten Artikel über einen Klon eines Pioniers und konnte nicht vorbeikommen. Ich schlage vor, dass Sie sich damit vertraut machen. Dies ist eine Geschichte über die Entwicklung von Kaboom, einem Klon des legendären Minesweeper-Spiels mit seiner eigenen Begeisterung.

Minesweeper erschien vor ziemlich langer Zeit nach den Maßstäben eines Computerspiels. Aber es scheint mir, dass sich die meisten Leute an die Spiele erinnern, die Teil früherer Windows-Versionen waren. Ich war nie gut in Minesweeper, aber ich habe es von Zeit zu Zeit gespielt. Einige Leute spielen ernster . Und für diejenigen, die sich aufmuntern möchten, empfehle ich Minesweeper - The Movie .

Idee


Vor kurzem hatte ich eine Idee: Was ist, wenn Sie Minesweeper gegen einen klügeren Computer spielen müssen?

Normalerweise wird die Position der Minen zu Beginn des Spiels festgelegt (hier gibt es jedoch einige Tricks - zum Beispiel, damit Sie den ersten Klick nicht verlieren können). Was aber, wenn der Standort der Minen nicht im Voraus festgelegt wurde und das Spiel den Standort der Minen nach Spielbeginn auswählen konnte?

Das wäre ziemlich grausam: Wenn Sie auf ein Quadrat klicken, das eine Mine enthalten kann, wird es immer enthalten sein! Sie müssen also im Voraus nachweisen, dass das Quadrat sicher ist.


In der Abbildung oben sind in den mit einem Punkt gekennzeichneten Zellen garantiert keine Minen vorhanden, und in den mit einem Ausrufezeichen gekennzeichneten Zellen ist garantiert eine enthalten. Fragezeichen bedeuten Unsicherheit: Wenn Sie mehr Zellen öffnen, können Sie möglicherweise berechnen, ob dort eine Mine versteckt ist oder nicht.

Andererseits gibt es Situationen, in denen Sie raten müssen:



In einer der unteren Zellen befindet sich eine Mine. Aber in welchem ​​ist es unmöglich zu verstehen. Sie müssen einen von ihnen auswählen. Aber unter der Bedingung, von der ich gerade gesprochen habe, würde dies einen sicheren Tod bedeuten! Ich wollte, dass das Spiel brutal ist, aber jetzt verliert es offensichtlich.
Daher werde ich die Idee leicht ändern. Sie können es erraten, aber nur, wenn keine sicheren Zellen mehr vorhanden sind. Somit wird das Spiel grausam, aber fair sein.

Mit anderen Worten:

  • , .
  • , , .
  • , :

    1. , , .
    2. , , .


Wie implementiere ich ein solches Spiel? Ich könnte versuchen, alle möglichen Felder zu berechnen, aber das ist unrealistisch: Selbst ein kleines 10x10-Feld bedeutet 2 ^ 100 Möglichkeiten. Es hilft nicht, nur diejenigen auszuwählen, die genau N min enthalten.

Zum Glück muss ich mir keine Sorgen um das gesamte Feld machen. Wir wissen nichts über Landminen, die nicht an Tags angrenzen. Ich interessiere mich nur für diejenigen, die an der Grenze sind, der Rest kann ganz zufällig bestimmt werden.



Dann kann ich alle Optionen für den Standort von Minen an der Grenze gemäß den Etiketten berechnen. Backtracking (Backtracking) - eine gute Technik, mit der Sie alle Kombinationen sortieren, aber auch schnell zurückziehen können, sobald wir feststellen, dass ein Zweig nicht berechnen kann.


Die zwei möglichen Standorte von Minen an der Grenze sind oben gezeigt. Wenn wir sie kombinieren, werden wir verstehen, welche Zellen garantiert leer oder abgebaut sind.

Ich muss auch die Gesamtzahl der Minen verfolgen. Somit sieht der Ort wirklich wie "5 Minuten an der Grenze, 5 Minuten draußen" aus. Dies ist wichtig, da ich sonst zu viele Minen an der Grenze hätte schaffen können (oder zu wenige!)

. Ich habe also alle Optionen. Was passiert, wenn ein Spieler beschließt, einen Käfig zu öffnen?

  • Wählen Sie eine zufällige Option (eine, die den „grausamen, aber fairen“ Regeln entspricht). Dadurch wird der Standort der Minen an der Grenze bestimmt.
  • Streuen Sie die außerhalb der Grenze verbleibenden nach dem Zufallsprinzip.
  • Befindet sich in der ausgewählten Zelle eine Mine, ist das Spiel beendet.
  • Sonst:

    1. Definieren Sie eine neue Bezeichnung für die identifizierte Zelle
    2. Zeigen Sie zusätzliche Zellen an, wenn es 0 ist
    3. , ! .


Für kleine Felder ist dies normal. Normalerweise gibt es nur wenige mögliche Kombinationen ... Moment, was ist das?



Oh nein!



Irgendwie gelang es mir, 18 Millionen mögliche Minenstandorte freizuschalten. Mein Firefox verschlingt 12 Gigabyte Speicher und das Öffnen einer Zelle dauert eine halbe Minute. Natürlich brauche ich einen besseren Algorithmus.

Jemand könnte bemerken, dass Minesweeper ein NP-vollständiges Spiel ist und daher eine exponentiell zunehmende Zeit nicht vermieden werden kann. Und im allgemeinen Fall ist dies wahr - es wird Positionen geben, deren Berechnung viel Zeit in Anspruch nimmt. Aber für einen kleinen Bereich funktioniert das.

Ich muss mich nicht an alle Kombinationen erinnern. Ich muss nicht einmal alle Kombinationen berechnen. Alles was benötigt wird ist ein Weg:

  • Überprüfen Sie, ob die Zelle sicher, gefährlich oder vage ist.
  • (, , ).


Anstatt die Optionen selbst auszuprobieren, werde ich den SAT-Solver verwenden . Dies sind Werkzeuge, die eine Formel verwenden, die aus logischen Variablen besteht, und nach einer Reihe von Werten suchen, die die Formel wahr machen würden. Eine solche imaginäre, aber durchaus gültige Methode für unsere Aufgabe.

Eine leistungsfähigere Klasse von Software sind SMT-Löser , die mit einem größeren Bereich von Werten und Formeln arbeiten, z. B. Logik erster Ordnung (Quantifizierer), Arrays, Ganzzahlen usw. Dies hilft zumindest dabei, einige Gleichungen für ganze Zahlen zu definieren. Aber ich brauche etwas, das im Browser funktioniert. Es gelang den Leuten, einige hochentwickelte Tools wie Z3Prover auf den Browser zu portieren , aber die WebAssembly-Version wiegt17 MB , und das ist zu viel.

Ich fand MiniSat , einen kleinen SAT-Löser, der von Joel Galenson für Javascript kompiliert wurde. Die kompilierte Datei benötigt nur 200 Kilobyte, also benutze ich sie.

CNF-Formeln


SAT-Löser arbeiten mit konjunktiven Normalformeln ( CNFs ). Die CNF-Formel lautet beispielsweise „ein UND aus ODERs“:

(a | ~ b | ~ c) & (c | d ~ e) & f

Sie können jede Formel der Satzlogik (Variablen und / oder nicht Implikation) in CNF konvertieren, sodass es sich um eine Art universelles Format handelt.

Wie benutzen wir es? Angenommen, wir haben eine Karte: Wenn ich Variablen für unbekannte Zellen erstelle (im Uhrzeigersinn: x1, x2, x3), müssen diese die folgenden Gleichungen erfüllen: Aber wie kann man in CNF „die Summe der Variablen ist 2“ ausdrücken? Ich habe eine Methode gefunden, die, wie ich später erfuhr, "Binomialcodierung" heißt und die einfachste Codierung ist. Sie sollten alle möglichen Teilmengen von Variablen berücksichtigen. Zum Beispiel benötigen Sie die folgenden Formeln:

? ? 1
2 ? 1




1 + 2 + 3 = 2
2 + 3 = 1
2 + 3 = 1 ( )




x1 + x2 + x3 = 2

  • Für jede Teilmenge von 2 Variablen ist mindestens eine wahr. Dies stellt sicher, dass der Betrag größer als 1 ist.
    (x1 | x2) & (x1 | x3) & (x2 | x3)
  • Mindestens eine Variable ist falsch. Dies stellt sicher, dass der Betrag weniger als 3 beträgt.
    (~ x1 | ~ x2 | ~ x3)


Für x2 + x3 = 1mich brauche ich einen ähnlichen Satz von Formeln:
  • Mindestens eine der Variablen ist korrekt: (x2 | x3)
  • Mindestens eine der Variablen ist falsch (~ x2 | ~ x3).

Durch die Kombination erhalte ich eine CNF-Formel mit 6 Punkten. Im Standard-DIMACS-Format: Alle Positionslinien enden mit 0, und die Negation wird mit einem Minus markiert. Wenn ich es mit MiniSat verbinde (probieren Sie es selbst aus), erhalte ich Folgendes : Dies bedeutet, dass MiniSat eine Lösung gefunden hat, bei der x1 und x2 wahr und x3 falsch sind. So wird das Board aussehen: Das gesamte Programm ist etwas komplizierter: Dies ist nur eine Lösung, es gibt eine andere. Um herauszufinden, ob x1, x2, x3 wahr (oder falsch) sein kann, müssen Sie daher weitere Anforderungen stellen. Ich muss fragen: „Ist dies angesichts der obigen Formel und x1 machbar? Wie wäre es mit der obigen Formel sowie ~ x1 "?

p cnf 3 6
1 2 0
1 3 0
2 3 0
-1 -2 -3 0
2 3 0
-2 -3 0




SAT 1 2 -3



! ! 1
2 . 1




Codierung bedeutet, dass ich alle möglichen Kombinationen (zum Beispiel alle Teilmengen von 3) einer Reihe von Variablen finden muss. Für diese Gleichung gibt es jedoch nur bis zu 8 Variablen, sodass die Formel normalerweise klein genug ist, damit MiniSat sie schnell lösen kann.

Min Tracking


Dies ist leider keine vollständige Lösung! Ich muss noch nachverfolgen, wie viele Minen noch übrig sind. Einige Kombinationen sind unmöglich, da Sie sonst mehr Minen als erlaubt erstellen können und es unmöglich ist, zu gewinnen.



In der Tat ist auch der umgekehrte Fall möglich: Wenn zu wenige Minen vorhanden sind, endet das Spiel, da nichts zu platzieren ist.

Daher muss ich in der SAT-Formel angeben, dass „die Anzahl der Minen nicht weniger als X und nicht mehr als Y beträgt“. Zuerst dachte ich, ich könnte den Trick mit allen Kombinationen anwenden. Leider funktioniert es bei großen Zahlen nicht so gut. Wenn es beispielsweise 20 Zellen und 10 Minuten gibt , stellen wir nach dem Verbinden der Zahlen mit dem Binomialkoeffizienten fest, dass die Anzahl der Kombinationen bereits 6 Stellen beträgt!

Also fand ich heraus, dass es viele andere Möglichkeiten gibt, die Summe der Variablen in die SAT-Formel zu kodieren. Sie müssen ein Schema erstellen, das die einzelnen Variablen kombiniert. Siehe zum Beispiel diese Antwort auf StackExchange oder diese .

Am Ende wurde mir die Idee aus einem Artikel mit dem Titel „Effektive CNF-Codierung mit booleschen Kardinalitätsbeschränkungen“ von Olivier Baillot und Yasin Bufhad klar. Wir sehen einen Baum, der rekursiv unäre Zahlen hinzufügt (oder Bits so sortiert, dass jeder am Anfang steht):



Am Ende dieses Diagramms erhalten Sie einen sortierten Satz von Ausgabevariablen. Um zu bestätigen, dass die Summe nicht kleiner als X ist, überprüfen Sie, ob das erste X der resultierenden Variablen 1 ist. Um zu behaupten, dass die Summe nicht mehr als Y ist, überprüfen Sie, ob das letzte N - Y der resultierenden Variablen 0 ist.

Dies ist viel besser als die Verwendung aller möglichen Kombinationen. Dieses Schema ist jedoch immer noch irrational, da es Sätze Ө (N ^ 2) erzeugt. Wenn die Anzahl der offenen Zellen ungefähr 100 beträgt, wird das Spiel träge. Wir können das Spiel weiter optimieren.
Anfragen reduzieren

Beim Studium des Problems habe ich festgestellt, dass ich die Anzahl der Abfragen an den Solver reduzieren kann. Ich wollte den Status aller Zellen bestimmen (dh prüfen, ob sie garantiert gefährlich, sicher oder nicht sind). Ich habe dies mit einer einfachen Schleife gemacht. Angenommen, die Tafel wird durch die Formel F beschrieben:

  • Entscheide dich für F & ~ x1zu prüfen, ob x1 0 sein kann
  • Entscheide dich für F & x1zu prüfen, ob x1 1 sein kann
  • Entscheide dich für F & ~ x2 zu prüfen, ob x2 0 sein kann
  • Entscheide dich für F & x2zu prüfen, ob x2 1 sein kann
  • Usw.

Was habe ich bemerkt? Wenn ich eine Lösung für F & ~ x1 bekomme, enthält sie auch die Werte aller anderen Variablen. Dies beantwortet bereits viele andere Fragen: Wenn die Lösung x2 = 0 enthält, muss ich nicht fragen, ob x2 0 sein kann, da ich dies bereits weiß. Dadurch kann ich die Anzahl der Anfragen um das 2-5-fache reduzieren.

Caching


Dies löst nicht das Problem der riesigen Formel, die von der "Zähl" -Schaltung erzeugt wird. Wie gesagt, die Anzahl der Sätze liegt in der Größenordnung von N ^ 2. Auf einer großen Tafel kann die Formel bis zu 10.000 Annahmen umfassen.

Glücklicherweise kennen wir die meiste Zeit die genaue Bedeutung vieler Zellen. Wenn die Zelle garantiert leer oder garantiert gefüllt ist, ändert sich der Wert nie! Dies bedeutet, dass wir es zwischenspeichern und nicht in die SAT-Formel aufnehmen können. Sobald wir den Zustand der Zelle bestimmt haben, müssen wir ihn nicht mehr erneut in die Berechnung einbeziehen. Zellen werden verwendet, solange sie nicht definiert sind.

Diese Optimierung ist etwas gefährlich: Wir haben keine Formel mehr, die die Richtigkeit der gesamten Platine bestätigt. Wenn alles andere wie geplant funktioniert, ist dies kein Problem, kann jedoch die Fehlerverfolgung erschweren.

Ein anderer Fall: im Ausland spielen


Dürfen Sie irgendwo auf der Karte außerhalb der Grenze zwischen dem offenen und dem ungeöffneten Bereich des Feldes klicken?

Anfangs dachte ich, es sei dasselbe wie zu raten: Wenn es keine sicheren Zellen gibt, können Sie einfach irgendwo auf das Feld klicken. Einige finden es jedoch seltsam, dass dies die Öffnung eines leeren Käfigs garantiert.

Deshalb habe ich das Spiel so geändert, dass ein Klick außerhalb des Rahmens immer bestraft wird. Mit Ausnahme des Spielbeginns natürlich, denn dann ist das ganze Brett „draußen“.

Es stellt sich jedoch heraus, dass es ein anderes Szenario gibt: Was ist, wenn alle Grenzfelder tödlich sind? Sie haben keine andere Wahl, als etwas anderes zu enthüllen. Diese Situation kann das Spiel von Anfang an unpassierbar machen. Jetzt gibt es noch eine Ausnahme. Sie dürfen außerhalb der Grenzen spielen, wenn:

3 . .
. . .
. . .



  • Das Feld ist nicht offen
  • Die abgebauten Zellen können sich am Rand befinden (ein Klicken auf die Außenseite sollte sicher sein) oder
  • In allen Zellen an der Grenze müssen sich Bomben befinden (Sie müssen nach draußen klicken).

Update : Die Änderung erwies sich als kontrovers, da die Einschränkung etwas künstlich ist. Ich habe einen Schalter hinzugefügt, der das Spielen mit diesen Bedingungen erlaubt / verbietet.

Das ist alles


Sie können hier Kaboom spielen . Versuchen Sie, den Debugging-Modus zu aktivieren: Dies macht das Spiel trivial, zeigt aber gut, wie es funktioniert. Github-

Quellcode . Er ist nicht sehr hübsch. Vielleicht interessiert Sie auch ein ähnliches Spiel von Simon Tatham, dem Erfinder von PuTTY. Seine Version hat eine andere Wendung: Es ist immer ohne Spekulation lösbar. Spielen Sie mit Bedacht! Was kann sonst noch nützlich sein, um im Cloud4Y- Blog zu lesenWie die Bank „kaputt gegangen “ istDatenschutz? Nein, sie haben nicht gehört → Die große Theorie der SchneeflockenDiagnose von Netzwerkverbindungen auf einem virtuellen EDGE-Router











CRISPR-resistente Viren bilden Schutzräume, um Genome vor DNA-durchdringenden Enzymen zu schützen.

Abonnieren Sie unseren Telegrammkanal , damit Sie keinen weiteren Artikel verpassen! Wir schreiben nicht mehr als zweimal pro Woche und nur geschäftlich. Wir erinnern Sie daran, dass Startups 1 Million Rubel bekommen können. von Cloud4Y. Allgemeine Geschäftsbedingungen für diejenigen, die dies wünschen - auf unserer Website: bit.ly/2sj6dPK

Source: https://habr.com/ru/post/undefined/


All Articles