SAT接地工具？

Question

在ASP (应答集编程)中，程序是用更高级别的声明语言编写的，然后以一种确定性的方式来生成ASP实例。

是否有SAT社区用于生成实例的受欢迎的地面站？换句话说，是否有什么东西可以被表达出来，例如：

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

然后从里面生成一个DIMACS文件？

一般而言，SAT竞赛实例是如何产生的？

Answer 1

卫星竞赛基准实例通常是使用专门定制的生成器程序而不是一般的ASP地面创建的。基准测试需求被描述为这里。

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

• 通过林伯勒、bool2cnf或bc2cnf翻译布尔表达式
• 将MiniZinc约束声明编译为CNF/DIMACS
• 用心钠素将anf2cnf转换为CNF

你可能有兴趣阅读报纸不存在CNF问题。它激发了像MiniZinc这样的高级语言的使用。