SAT接地工具? [英] Tools for SAT grounding?

问题描述

在ASP(答案集编程)中，程序以更高级别的声明性语言编写，然后以确定性方式进行基础化，以使用lparse或gringo等基础知识来生成ASP实例.

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.

SAT社区是否使用流行的基础生成实例?换句话说，是否有可以表达的东西，例如:

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).

并从中生成DIMACS文件?

and generate a DIMACS file from it?

一般来说，SAT竞赛实例是如何生成的?

In general, how are SAT competition instances generated?

推荐答案

SAT竞争基准实例通常是通过使用专门定制的生成器程序而不是通用的 ASP基础程序创建的.基准要求在此处中进行了描述.

SAT competition benchmark instances are typically created by using specially tailored generator programs rather than general ASP grounders. The benchmark requirements are described here.

其他创建 CNF/DIMACS 文件的选项:

• 通过 Limboole ， bc2cnf
• 将 MiniZinc 约束声明编译为CNF/DIMACS
• 使用 ANF 转换为CNF .org/tag/anf/"rel =" nofollow noreferrer> anf2cnf

• Translate a Boolean expression via Limboole, bool2cnf or bc2cnf
• Compile a MiniZinc constraint declaration into CNF/DIMACS
• Convert ANF to CNF with anf2cnf

您可能有兴趣阅读没有CNF问题.它激发了诸如 MiniZinc 之类的高级语言的使用.

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

这篇关于SAT接地工具?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！