declarative - SAT接地工具？

Question

在 ASP（答案集编程）中，程序是用更高级别的声明性语言编写的，然后以确定性的方式接地，以使用诸如 lparse 或 gringo 之类的接地程序生成 ASP 实例。

SAT 社区是否有流行的grounders 用于生成实例？换句话说，有没有可以采用如下表达式的东西：

vertex(a; b; c).
isRed(V) \/ isBlue (V) \/ isGreen(V) :- vertex(V).

并从中生成一个 DIMACS 文件？

一般来说，SAT竞赛实例是如何产生的？

Answer 1

SAT 竞赛基准实例通常是通过使用专门定制的生成器程序而不是通用的ASP grounders创建的。此处描述了基准要求。

创建CNF/DIMACS文件的其他选项包括：

• 通过Limboole、bool2cnf或 bc2cnf转换布尔表达式
• 将MiniZinc约束声明编译成 CNF/DIMACS
• 使用anf2cnf将ANF转换为 CNF

您可能有兴趣阅读论文没有 CNF 问题。它激发了MiniZinc等高级语言的使用。