【发布时间】：2015-08-25 12:59:36
【问题描述】：
我是 Z3 的初学者。我只是尝试了一些Z3包中发布的例子，其他的经验我已经没有了。我正在处理关于图中最短路径的问题。我可以用 Z3 做吗？谢谢大家。
【问题讨论】：
标签： z3
【发布时间】：2015-08-25 12:59:36
【问题描述】：
您可以用逻辑表达此类查询，但也许您可以只使用专用算法（Dijktra 或变体）来解决此类问题。 有关使用 Z3 的介绍，请查看链接自的教程 http://rise4fun.com/z3
【讨论】：
-
我已经阅读了该材料。我知道Z3非常灵活，能够解决很多复杂的问题。我想了解更多关于Z3的理论，但是似乎没有关于基本机制或介绍的信息。您能告诉我如何了解更多信息吗？