|
Anzeige
|
SAT-/SMT-Solver ASICsHallo, 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? Hast Du einen konkreten Anwendungsfall, wofür Du das brauchst?
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/
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.
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.
Aber wann ist lang, “zu lang”? In meiner täglichen Arbeit mit Constraint Solvern in Simulationen ist der Flaschenhals meist woanders. Antwort schreibenBitte melde dich an, um einen Beitrag zu schreiben. |
Anzeige
|
