Nochmal: das ist nicht die nächste Generation von Minern!
Ich wuerde das so nicht stehen lassen. Ich habe noch ein bischen ueber das Paper nachgedacht. Und eigentlich ist es relativ simpel. Die vorgeschlagene Methode ist sozusagen "Mining in elegant".
Das worauf heute alle gucken, die GH/s, wuerde der Solver uebernehmen. Wenn ich das BTC-Prinzip richtig verstehe, so bekommen alle die gleiche Aufgaben, jeder versucht per Brute Force die Loesung zu berechnen (eine Schleifendurchlauf = 1 H) und der erste bekommt dann den Zuschlag.
Mit der in der Publikation genannten Methode wuerde die Schleife vom Solver uebernommen, d.h. solange der Solver keine Loesung gefunden hat und Teilbaeume des Suchbaums verwirft, solange beweist der Solver, dass Mengen (!) an Hashs nicht die Loesung sein koennen. Das kann die vorhandene Software nicht, die kann diese Aussage immer nur fuer den gerade gegebenen Hash treffen. Ein Miningalgorithmus wuerde dann wie folgt aussehen:
(i) hole Aufgabe;
(ii) erzeuge und schreibe die Constraints in eine Datei;
(iii) starte den Solver mit Constraints als Input;
(iv) wenn der Solver satisfiable ausgibt:
(a) lese die Loesung ein;
(b) erzeuge daraus das was man benoetigt um den Zuschlag zu bekommen und hole Zuschlag;
(c) gehe zu (i);
(v) wenn der Solver unsatisfiable ausgibt, hmm ... weiss noch nicht recht;
(vi) wenn jmd anderes die Loesung findet:
(a) stoppe Solver;
(b) gehe zu (i);
Was die Publikation unter "non-deterministic" versteht, bedeutet, so glaube ich (bin mir aber nicht 100% sicher), dass die Loesung fuer die Nonce nicht eindeutig ist, es kann sehr viele Loesungen geben, die Nonce haengt dann einfach von der Implementierung des Solvers ab bzw. wenn man einen Zufallsgenerator benutzt um das Branching des Solvers zu bestimmen, eben von der Sequenz der Zufallszahlen.
Ich kann mich mit meiner Interpretation der Methoden aber auch irren ...
Es kann auch gut sein, dass, je groesser die Difficulty ist, desto besser ist die vorgeschlagene Methode. Ich habe die Erfahrung gemacht, dass, je constrainter ein Problem ist, desto schneller findet der Solver eine Loesung. Aber mit solchen Aussagen muss man vorsichtig sein, SAT ist nun mal sehr schwer zu loesen.
Wer Lust hat das mal zu implementieren, ich koennte den SAT-Teil uebernehmen.
Gruss,
cu