NVIDIA's AI-Projekt "satlution" macht Furore

By Olaf Jenkner Date 2025-09-13 01:32 Upvotes 2

Das Forum ist ergriffen und hält den Atem an.

Aber im Ernst:
Das ist schwerer Stoff, mit dem wohl nur studierte Informatiker etwas anfangen können.
Könntest du das bitte für den Rest populärwissenschaftlich erklären?

By Ingo Althöfer Date 2025-09-13 05:18

Hallo Olaf, hallo Günter,

auch ich habe nur andeutungsweise verstanden, worum
es geht, um "SAT-Solver":
https://de.wikipedia.org/wiki/Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik

3-SAT ist eines der ursprünglichen NP-vollständigen Probeme.
SAT-Solver gibt es seit den 1990er Jahren.

In Jena gab es in der Informatik einen Lehrstuhl (Martin Mundhenk),
dessen Team manchmal an Wettbewerben für SAT-Probleme teilnahm.
Ulf Lorenz (Computerschach-Programmer vor dem Jahr 2000) hat sich
auch mit Max-SAT-Problemen beschäftigt.

Es würde helfen, wenn Günter einen Link zur Rangliste
der besten SAT-Solver gäbe.

Viele Grüße, Ingo.

By Guenter Stertenbrink Date 2025-09-13 09:49 Edited 2025-09-13 10:09 Upvotes 1

in Raetsel Spalten sieht man manchmal "Logelei"
oder aehnliche Raetsel.
Das ist in etwa vergleichbar mit SAT.
Hier eine kurze Einfuehrung in Deutsch :
http://cl-informatik.uibk.ac.at/teaching/ss14/ewa/reports/ss13-MM.pdf

Natuerlich sind die Computer den Menschen hier haushoch ueberlegen.
Es hat sich in den vergangenen Jahrzehnten gezeigt, dass viele
schwer berechenbare Probleme (auch Schach ?) auf SAT-Probleme
zurueckgefuehrt werden koennen und wegen des Fortschritts bei den SAT-Loesern
wird dieser Weg immer oefter eingeschlagen.
Z.B. bei Eternity in 1999 gab es bereits einige Leute, die das Problem
als SAT-kodierten.
Der derzeit beste SAT-Loeser war bis vor kurzem Kissat 4.0.3,
verfuegbar hier :
https://github.com/arminbiere/kissat/releases
Einmal im Jahr gibt es die SAT-Wettbewerbe , hier der von 2024
auf der Internetseite der Gewinner :
https://cca.informatik.uni-freiburg.de/sat24medals/
Typisch sind diese "Kaktus-Plots" , die zeigen wieviele Probleme
mit welchem Bedenkzeitlimit geloest wurden.
Hier der Fortschritt von 1993-2022 in Kaktus-Plots
https://cca.informatik.uni-freiburg.de/papers/BiereFleuryFroleyksHeule-POS23.pdf
minisat in 2008 war so eine Art "Stockfish" bei den SAT-engines.
Open source, einfach, gut dokumentiert, darauf konnten dann
viele andere engines aufbauen.

"SATLUTION" waehlte die besten 5 Programme aus 2024 und wurde trainiert
an den 400 Problemen ("benchmarks") von 2024.
Also in etwa so ein "6-Hirn", mit dem 6.Hirn ein AI-trainiertes Programm.

By Olaf Jenkner Date 2025-09-13 10:47

Guenter Stertenbrink schrieb:

Hier eine kurze Einfuehrung in Deutsch

Danke, Günter.
Diese Einführung hat mir sehr geholfen, auch wenn ich beim Fachterminus "der LeserIn" an meine Grenzen gekommen bin.

By Ingo Althöfer Date 2025-09-13 20:30

Hallo Günter,

sehr spannend das Ganze.

Guenter Stertenbrink schrieb:

...
"SATLUTION" waehlte die besten 5 Programme aus 2024 und wurde trainiert
an den 400 Problemen ("benchmarks") von 2024.
Also in etwa so ein "6-Hirn", mit dem 6.Hirn ein AI-trainiertes Programm.

Ein kleiner Kreis, zu dem auch GM Karsten Müller und
ich gehören, diskutiert das Thema und Paper auch...
Viele Grüße, Ingo.