Tools for SAT grounding?

Question

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?

Answer 1

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.