CSP2SAT4J: A Simple CSP to SAT Translator. SAT solvers can now handle very large SAT instances. As a consequence, many translations into SAT have been shown successful in recent years: Planning and Bounded Model Checking are two examples of applications in which SAT engines are reported to be as good as or even better than dedicated software. During the first CSP competition, SAT-based approaches were demonstrated competitive with the other CSP solvers on binary constraints. Constraints being provided in extension, it was a big advantage for techniques based on grounding predicates since only benchmarks that could be grounded in a reasonable space were available. As such, the comparison between SAT-based solvers (that need to ground predicates) and the approaches developed by the CSP community (that usually handle directly the constraints as expressed) was not fair. For the second edition of the competition, the constraints can now be given in intension, and global constraints such as allDifferent are available. The idea behind the submission of CSP2SAT4J is to show when SAT-based CSP solvers can still compete in some cases against ”traditional” CSP solvers under those new conditions
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Bischl, Bernd; Kerschke, Pascal; Kotthoff, Lars; Lindauer, Marius; Malitsky, Yuri; Fréchette, Alexandre; Hoos, Holger; Hutter, Frank; Leyton-Brown, Kevin; Tierney, Kevin; Vanschoren, Joaquin: ASlib: a benchmark library for algorithm selection (2016)
- Barahona, Pedro; Hölldobler, Steffen; Nguyen, Van-Hau: Representative encodings to translate finite CSPs into SAT (2014)
- Hurley, Barry; Kotthoff, Lars; Malitsky, Yuri; O’Sullivan, Barry: Proteus: a hierarchical portfolio of solvers and transformations (2014)