有人可以帮我指出这将是使用一阶公式，从而给它输入到SMT求解以下等式的最佳编码？
x`=Ax+b
Answer 1:
可以在Z3容易编码的微分方程，因为它仅仅是一组n个线性（仿射）在n ^ 2 + N个实常数（n ^ 2从a_ij，正从b_i）和正实变量（X_I）功能。 您可以在Z3直接编码此。
dotx_1 = a_11 * x_1 + a_12 * x_2 + a_13 * x_3 + ... + a_1n * x_n + b_1
dotx_2 = a_21 * x_1 + a_22 * x_2 + a_13 * x_3 + ... + a_2n * x_n + b_2
...
dotx_n = a_n1 * x_1 + a_n2 * x_2 + a_n3 * x_3 + ... + a_nn * x_n + b_n
这里有一个链接，在Z3Py的这一个2x2版本： http://rise4fun.com/Z3Py/pl6P
然而，编码常微分方程的解将是困难的，因为线性微分方程的解涉及指数（超越函数）。 对于类常微分方程与解决方案，可以表示为多项式（在a_ij常量，X_I变量，和/或一个时间变量t），您将能够编码（精确）解决方案为多项式Z3（参见，例如，[1]）。
然而，对于涉及超越数，一般的解决方案，你有很多可能的选项，这取决于你正在努力完成的任务。 一个选择是造型超越数未解释功能。 有各种SMT-LIB基准，这样做了一些工作，但我不这么熟悉这些，所以希望别人能指出一个链接到他们。 如果你想证明对这种常微分方程的解一些引理这将是最有用的。 像MetiTarski一些工具保持上下超越数（例如使用截断泰勒级数，这是多项式，并在Z3因此表示的）的约束近似的，但我不知道这在Z3的地位，但它看起来像可能有一些支持，莱昂纳多可以在更多的评论[6]。
如果你正在做的可达性计算，那么你可以overapproximate触及集，可与常微分方程解的简单（更抽象）表示来完成。 举例来说，可以应用该杂交技术[2]的变体和具有矩形动力学overapproximate线性动力学，例如，分区的状态空间的一个有趣的子集，则在每个分区中，之下和之上近似每个维度dotx_i = a_i1 X_1 + a_i2 X_2 + ... + b_i与[C，d] dothatx_i \一些常数C和d选择以确保原始（混凝土）的X_I每溶液包含在所述一组overapproximated（摘要）溶液hatx_i的。 从时间0设定的hatx_i的解决方案，t是在区间[C T + X_I（0），d T + X_I（0）]，其中X -1（0）是X_I的在时间零初始条件，并且t是要计算的范围设置上的界定实时。 为此，您可以在所有维度。 为了计算C，d（这很可能会为每个分区的，每个尺寸会发生变化），这取决于你有多在乎稳健，你可以简单地（数字）最大化和最小化在每个分区原ODE dotx_i。
从您的其他职位，它看起来像你试图模拟混合系统。 仿真仍将遭受试图代表超越数的问题，因为即使试图模拟一个轨迹（而不是建模组可能的轨迹）将要求代表的解决方案，这是一般的超越。 据我所知，这仍是在模拟社区进行数值[见，例如，3]，但对“保证”（音）的集成，它提供了有关如何离谱的数字解决方案是从实际（分析界工作）溶液[4，5]。
[1]符号可达性计算为线性矢量场的家庭。 赫拉尔Lafferriere，乔治·帕帕斯J.，和Sergio Yovine。 杂志符号计算，32（3）：231-253，2001年9月http://www.seas.upenn.edu/~pappasg/papers/JSC01.pdf
[2] E. Asarin，T.荡，A.芝，非线性系统的分析，ACTA Informatica的杂交方法，43：7，2007年，451-476， http://www.springerlink.com/content/q6755l613l856737 /
[3]十九可疑的方法来计算一个矩阵的指数，二十五年后，克里夫·莫勒尔和查尔斯·范龙，SIAM回顾，卷。 45，第1号（三月，2003），第3-49， http://www.jstor.org/stable/25054364
[4]自动，保证集成解析函数，马丁C. Eiermann，BIT计算数学，1989， http://www.springerlink.com/content/q2k30rtx2h2n1815/
[5] GRKLib：保证龙格库塔图书馆，Bouissou，澳，马特尔，M.，科学计算，计算机运算和验证的数字，2006年， http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber= 4402398
[6]实代数策略MetiTarski证明，格兰特奥尔尼帕斯莫尔，劳伦斯C.保尔森，和莱昂纳多德莫拉。 智能计算机数学（CICM / AISC）会议，2012年， http://research.microsoft.com/en-us/um/people/leonardo/CICM2012.pdf
文章来源: Encoding of first order differential equation as First order formula
