所以我试图用z3解决调度问题。我有一组需要完成的工作和一组能够完成这些工作的资源。作业是有序的（总顺序），一般来说，问题用线性算术方程（=，<，>）和布尔表达式表示（例如：job1和job2分配给不同的资源=>它们可以并行运行）。
约束本身并不复杂，但我在求解器中抛出的约束数量是数千，可能会增加10倍。
所以我遇到的一个问题是，Z3似乎在确定如何解决同一问题方面不确定（但在不同的运行期间）。有时它会在几秒钟内产生结果但有时需要时间。我经常做的是杀死当前的运行并重新启动然后它再次给我一个几乎瞬间的结果。我想知道，使用某些策略/策略是否有助于更加一致地将Z3引向正确的方向？
我正在使用z3py（带优化），当我打印（len（z3.tactics（）））时，我看到有107种不同的策略。如果我使用print（z3.tactics（））打印这些策略的描述，那就太过分了。
有没有人知道一个纸/网站基本上可以给我一个暗示使用哪种策略取决于我使用哪种约束？ （在我的例子中：线性算术和一些没有量词的布尔约束）
遗憾的是，Z3战术的记录很少。但开发人员并不是真正的责任：基于策略的定理证明与实现的具体内容有关：它是一个好的旧手动证明器（Isabelle，HOL，Coq等）还是更现代/自动化的证明者/求解器等作为Lean / Z3等。最好的策略是继续应用它们，看看你是否能找到合适的组合。不可否认，这不是最有用的建议，但在这一点上，选择正确的策略更多的是艺术而不是科学，需要深入了解求解器本身。
话虽如此，这里有一些基本的文档：http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm
如果您要试验并记录您的发现，我相信其他跟进z3的人会发现它很有用！