In ASP (Answer Set Programming), programs are written in a higher-level declarative language and then grounded in a deterministic way to generate an ASP instance using a grounder like lparse or gringo.
Are there popular grounders the SAT community uses for generating instances? In other words, is there something that could take an expression such as:
vertex(a; b; c).
isRed(V) \/ isBlue (V) \/ isGreen(V) :- vertex(V).
and generate a DIMACS file from it?
In general, how are SAT competition instances generated?
SAT competition benchmark instances are typically created by using specially tailored generator programs rather than general ASP grounders. The benchmark requirements are described here.
Other options to create a CNF/DIMACS file include:
- Translate a Boolean expression via Limboole, bool2cnf or
bc2cnf
- Compile a MiniZinc constraint declaration into CNF/DIMACS
- Convert ANF to CNF with anf2cnf
You might be interested to read the paper There are no CNF problems. It motivates the usage of high-level languages like MiniZinc.
