将电路基准转换为CNF公式用于与SAT求解器求解
是否有任何可以将电路基准（ISCA）转换为CNF的工具，以便在SAT求解器中使用它？主要目标是为电路找到一些输入模式，这些输入模式将在某些门中提供一些预定义的输出。
Is there any tool that can convert circuit benchmarks (ISCAS) to CNF so that it can be used in SAT solver? The main goal is to find some input patterns for the circuit which will give some predefined output in some gates.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
工具问题不超出此网站的范围。
我不知道直接的“ ISCAS到DIMACS”转换器。
您可能会查看 bc2cnf 。 This is a versatile converter which reads a circuit description and writes the corresponding
CNFinTool questions are out of scope for this site.
I am not aware of a direct "ISCAS to DIMACS" converter.
You may have a look at bc2cnf. This is a versatile converter which reads a circuit description and writes the corresponding
CNFin DIMACS format.It also contains a parser/converter for the ISCAS-relatedEDIMACSformat.ABC 提供
read_bench和 <代码> write_cnf 。但是，
write_cnf仅适用于具有一个主输出的电路。您可能需要编辑基准，以便在满足门条件时主输出为 1。ABC offers both
read_benchandwrite_cnf.However,
write_cnfonly works for circuits with one primary output. You will likely need to edit your benchmarks so that the primary output is 1 when your gate conditions are satisfied.