risolutore di insiemi di risposte per apprendimento nogood pilotato dai conflitti
clasp è un risolutore di insiemi di risposte per programmi di logica
normale (estesa). Combina le capacità di modellazione di alto livello di
ASP (Answer Set Programming) con tecniche all'avanguardia dall'area della
risoluzione di vincoli booleani. L'algoritmo primario di clasp si basa
sull'apprendimento nogood pilotato da conflitti, una tecnica che ha
dimostrato grande successo per i controlli di soddisfacibilità (SAT). A
differenza di altri risolutori ASP con apprendimento, clasp non si basa su
software datato, come un risolutore SAT o qualsiasi altro risolutore ASP
esistente. Invece clasp è stato sviluppato veramente per la risoluzione di
insiemi di risposte basata su apprendimento nogood pilotato da conflitti.
clasp può essere applicato come risolutore ASP (sul formato di output
LPARSE), come risolutore SAT (su formato DIMACS/CNF semplificato) o come
risolutore PB (su formato OPB).
