potassco
The strength of clasp on normal logic program
I'm trying to use clasp to solve some normal logic programs and it seems like clasp (clingo version 5.7.1) is (much) slower than converting the normal logic program to SAT and solving it with kissat in most UNSAT instances. If I'm not wrong, clasp is using a stable model version of the CDCL algorithm, so my question is which CDCL SAT solver is similar to clasp in terms of solving techniques? In other words, the SAT solver has certain techniques on CNF and clasp has adapted the corresponding technique to normal logic programs. Chaff/Zchaff/Minisat/Cadical?
so my question is which CDCL SAT solver is similar to clasp in terms of solving techniques? In other words, the SAT solver has certain techniques on CNF and clasp has adapted the corresponding technique to normal logic programs. Chaff/Zchaff/Minisat/Cadical?
clasp contains adaptations of various techniques from various SAT solvers, including MiniSat, SatELite, glucose, RSat, PicoSat, Lingeling, Berkmin, Siege and (z)Chaff.
However, it currently lacks certain inprocessing techniques and heuristics that are e.g. implemented in kissat. Furthermore, clasp is not as highly trained/tuned for typical (competition) SAT problems as most SAT solvers. For example, various (SAT) pre-/in-processing techniques are not enabled by default.
Typically, performance on particular problems can be improved by adjusting some of the many provided options (see clasp --help=3) - either manually or automatically with tools like SMAC. Alternatively, clasp offers a set prefabricated configurations that have shown to be effective in different settings. You can select a specific configuration via option --configuration, e.g. clasp --configuration=trendy.
May I also ask if clasp has adapted any QBF-solving techniques for those sigma-2-p complete disjunctive programs? If yes, what are the referenced QBF solvers?
No, clasp does not reference any particular QBF-solving techniques or solvers. Our strategy for solving disjunctive programs is detailed here.