CODEWITHSUNDEEP
declarativesatisfiabilityanswer-set-programming
dspyz
dspyz

Reputation: 5524

Tools for SAT grounding?

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?

Upvotes: 1

Views: 228

Answers (1)

Axel Kemper
Axel Kemper

Reputation: 11332

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:

You might be interested to read the paper There are no CNF problems. It motivates the usage of high-level languages like MiniZinc.

Upvotes: 3

Related Questions