SAT-/SMT-Solver ASICs

[Stefan H. (Firma: dm2sh) (stefan_helmert)]

Hallo,

da nun immer mehr spezialisierte Rechenhardware entsteht, z. B. für 
neuronale Netze, wäre es doch plausibel, dass es so etwas auch für SAT- 
oder SMT-Solver gäbe.

Ich habe nur ein paar wenige, kaum relevante Projekte gefunden, die das 
auf einem FPGA implantieren.

Ist das so wenig relevant? Ist der Geschwindigkeits- bzw. 
Effizienzgewinn zu gering?

[Ben B. (Firma: Funkenflug Industries) (stromkraft)]

Hast Du einen konkreten Anwendungsfall, wofür Du das brauchst?

[Axel S. (a-za-z0-9)]

Stefan H. schrieb:
> da nun immer mehr spezialisierte Rechenhardware entsteht, z. B. für
> neuronale Netze, wäre es doch plausibel, dass es so etwas auch für SAT-
> oder SMT-Solver gäbe.

SAT wie in Schweizer Archiv für Tierheilkunde?
SMT wie in Sowjetisches Militärtribunal?

oder wovon redest du? Ist es zu viel verlangt, seltene oder 
ungebräuchliche TLA [1] aufzulösen?


[1] ja, eben! TLA = three letter acronym

[Stefan H. (Firma: dm2sh) (stefan_helmert)]

Ben B. schrieb:
> Hast Du einen konkreten Anwendungsfall, wofür Du das brauchst?

https://github.com/TheTesla/z3route/blob/master/routelines.ipynb

Ist zwar bei so wenig noch sehr schnell (Sekundenbruchteile), aber je 
komplexer das Problem wird, um so länger dauert es eben.

Axel S. schrieb:
> oder wovon redest du? Ist es zu viel verlangt, seltene oder
> ungebräuchliche TLA [1] aufzulösen?

Wenn Du den jeweiligen Begriff und seine Abkürzung nicht kennst, wirst 
Du auch keine Antwort auf die Frage haben.

Google liefert für beide Begriffe, also SAT-Solver und SMT-Solver 
unmittelbar die richtige Bedeutung.

[Marcus H. (mharnisch)]

Stefan H. schrieb:
> Ist zwar bei so wenig noch sehr schnell (Sekundenbruchteile), aber je
> komplexer das Problem wird, um so länger dauert es eben.

Aber wann ist lang, “zu lang”? In meiner täglichen Arbeit mit Constraint 
Solvern in Simulationen ist der Flaschenhals meist woanders.