在ASP（Answer Set Programming）中，程序是用更高级的声明性语言编写的，然后以确定性的方式为基础，使用类似lparse或gringo的grounder生成ASP实例。
SAT社区在生成实例时是否使用了流行的背景？换句话说，有没有什么东西可以用这样的表达式：
vertex(a; b; c).
isRed(V) / isBlue (V) / isGreen(V) :- vertex(V).
并从中生成DIMACS文件？
一般来说，SAT竞赛实例是如何生成的？
SAT竞赛基准实例通常是通过使用专门定制的生成器程序而不是通用的ASP基础程序来创建的。此处描述了基准要求。
创建CNF/DIMACS文件的其他选项包括：
- 通过Limboole、bool2cnf或bc2cnf
- 将MiniZinc约束声明编译到CNF/DIMACS中
- 使用anf2cnf将ANF转换为CNF
你可能有兴趣阅读这篇论文。没有CNF的问题。它激发了像MiniZinc这样的高级语言的使用。