Tutto e di + - sat solver VERAMENTE efficienti

salve a tutti,
qualcuno per caso saprebbe consigliarmi un SAT solver davvero ottimo?
Io sto usando Minisat, che è il migliore che ho trovato, ma non basta. se avete suggerimenti sono ben accetti!

il problema SAT è NP-completo. Significa che l'algoritmo deterministico più efficiente che si possa scrivere ha complessità esponenziale. Esistono tuttavia sistemi euristici per trovare soluzioni tramite approssimazioni successive. Nel caso medio hanno tempi polinomiali, ma degradano a più che esponenziali nel caso peggiore.

In caso te lo stessi chiedendo, sono basati sugli algoritmi genetici.

un mio compagno di corso sta lavorando ad una implementazione di minisat in OpenCL, lo speedup è 33x.

è un progetto di tesi quindi non ti so dire se può essere liberamente utilizzabile, inoltre è ancora una versione preliminare che sicuramente lascia spazio ad ulteriori ottimizzazioni

@theKane: conosco il problema della soddisfacibilità logica.
Dato che ogni anno si tengono svariate competizioni tra team che sviluppano sat solver, vorrei solo avere la certezza di stare usando uno dei migliori, visto che ho praticamente già raggiunto il limite della computabilità in tempi non astronomici. Le statistiche riguardanti appunto il degrado verso tempi esponenziali (su cui mi sono basato per scegliere il solver) che ho trovato risalivano al 2008 e davano come migliore Minisat, che sto quindi usando. Intendevo chiedere se qualcuno ha notizie più recenti (che non ho trovato finora).
Inoltre ogni team sceglie l'algoritmo che preferisce, Minisat per esempio "impara" ma non "evolve" propriamente. DPLL è basato su ricorsione, backtrack e unit propagation. WalkSat e GSAT si basano su algoritmi a ricerca locale. Un paio di solvers usano anche algoritmi genetici, ma almeno nel grafico riguardante il 2008 sono finiti decisamente agli ultimi posti.

@hedo: anche il mio è un progetto per la tesi!

ho trovato questo sito che ha risolto il mio quesito:
satcompetition.org/

@hedo: dimenticavo.. se il tuo amico vuole provare un benchmark VERAMENTE difficile per il suo sat solver, mi mandi pure una email.. tra l'altro se ci fosse un modo per risolverlo sarebbe un risultato scientifico piuttosto importante. (ma per ora è decisamente infattibile)