Warum gibt es einen enormen Unterschied zwischen SAT-Lösern?

SAT-Löser sind sehr wichtig bei algebraischen Angriffen , z. B. Walksat und Minisat .

Bei der Lösung der hier zur Verfügung stehenden Benchmark-Probleme besteht jedoch ein enormer Leistungsunterschied zwischen den beiden - Walksat ist für diese Probleme viel schneller als Minisat. Warum ist das?

Diese Implementierung von walkSat scheint einige Leistungsverbesserungen zu haben - gibt es einen Grund, warum sie nicht in den internationalen SAT-Wettbewerben enthalten war ?

Ja, es gibt einen großen Unterschied zwischen MiniSAT und WalkSAT. Lassen Sie uns zunächst klarstellen: MiniSAT ist eine spezifische Implementierung der generischen Klasse von DPLL / CDCL-Algorithmen, die Backtracking und Klausellernen verwenden, während WalkSAT der allgemeine Name für einen Algorithmus ist, der zwischen gierigen Schritten und zufälligen Schritten wechselt.

Im Allgemeinen ist DPLL / CDCL bei strukturierten SAT-Instanzen viel schneller, während WalkSAT bei zufälligem k-SAT viel schneller ist . Industrielle und angewandte SAT-Instanzen sind in der Regel sehr strukturiert, sodass DPLL / CDCL in den meisten modernen SAT-Solvern die dominierende Rolle spielt. Eine Technik kann sich jedoch von Instanz zu Instanz durchsetzen. Dies ist einer der Gründe, warum Portfolio-Löser populär geworden sind.

Ich bezweifle sehr, dass WalkSAT auf den Instanzen auf dieser Seite viel schneller ist als MiniSAT. Zum einen gibt es dort Gigabyte an SAT-Instanzen - wie viele haben Sie versucht, sie miteinander zu vergleichen? WalkSAT ist in den meisten strukturierten Instanzen überhaupt nicht wettbewerbsfähig, weshalb es in Wettbewerben nicht oft vorkommt.

Nebenbei bemerkt: Vijay hat Recht, dass MiniSAT immer noch relevant ist. Da es Open Source und gut geschrieben ist, ist MiniSAT der beste Löser, um zu zeigen, dass eine bestimmte Optimierung vielversprechend ist . Viele Leute optimieren MiniSAT selbst, um ihre Optimierungen zu demonstrieren - werfen Sie einen Blick auf die Kategorie "MiniSAT-Hack" in den letzten SAT-Wettbewerben.

Es gibt einen enormen Unterschied zwischen Satelliteninstanzen . Der SAT-Löser kann für die Klasse von Instanzen eine gute Leistung erbringen, für die Klasse von Instanzen jedoch eine schlechte Leistung , während der Löser für die Klasse und die Klasse schlechte Leistung .X Y B Y $A$$X$$Y$$B$$Y$$X$

Ein gutes Papier zu diesem Thema zu lesen ist dies ein von Nudelman et al . In diesem Artikel geht es darum, einfach zu berechnende Funktionen von SAT-Instanzen zu ermitteln, anhand derer Sie feststellen können, welche Algorithmen wahrscheinlich eine gute Leistung erbringen und welche nicht. Mit dieser Technik ist es möglich, einen Portfolio-basierten Algorithmus zu erstellen, der eine Probleminstanz schnell analysiert und dann die Instanz mit dem am besten geeigneten Algorithmus löst. Es gibt eine Reihe von Veröffentlichungen, die dieser folgen; googeln SATzilla wird viel Lesematerial auftauchen lassen.

Wenn Sie sich fragen, warum SAT-Löser in allen Fällen besser ist als Löser , dann ist das wohl ein Fortschritt :). Wenn Sie wissen möchten, was genau einen guten Löser ausmacht, könnte die Antwort wahrscheinlich in mehrere Doktorarbeiten umgewandelt werden. Ich schlage vor, Sie beginnen mit dem Aufsatz von Nudelman et al .$A$$B$