约束线性方程的解

Question

我正在寻找求解线性方程组的方法。具体来说是 8 个方程式，总共有 16 个未知值。

每个未知值 (w[0...15]) 是一个 32 位二进制值，对应于 8 位上写入的 4 个 ascii 字符。

我试过将这个线性方程组写成一个矩阵方程。

现在，使用 Eigen linear algebra library，我得到了 16 个解决方案 (w[0...15])，但它们都是十进制值或空值，这不是我需要的。所有 16 个解决方案都需要在其二进制表示下等效于 4 个十六进制字符。表示 48 到 56（ascii 表示“0”到“9”）、65 和 90（ascii 表示 'A' 到 'Z'）或 97 和 122（ascii 表示 'a' 到'z').

我找到了解决这个问题的方法，使用的是 box-constraints。示例显示 here using python's lsq_linear function which allows the user to specify bounds. It seems Eigen does not let the user specify bounds in its decomposition methods.

因此，我的问题是，如何使用线性代数库在 C++ 中获得类似的结果？或者有没有更好的方法来求解这样的方程组而不用在单个矩阵方程下写？

提前致谢。

Answer 1

如果你的未知数比方程多，你的系统肯定是不确定的，8 x 16 矩阵的秩最多为 8，因此你至少有 16 个自由度。

此外，如果您对变量有限制，即混合等式和不等式，那么您的问题最好作为 linear programming. You can set a dummy objective function c[i] = 0, you could use GLPK 提出，但这是一个非常通用的解决方案。如果你想要一个小代码片段，你可能会找到一个玩具实现的 Simplex 方法来满足你的需要。

Answer 2

由于您在 Z/2³²Z 上使用线性方程，整数线性规划（如您标记的问题）可能是一个解决方案，并且算法本质上是浮点数是不合适的。框约束是不够的，它们不会强制变量采用整数值。此外，问题中显示的模型没有考虑到 Z/2³²Z 中的乘法和加法可以 wrap，这不包括许多潜在的解决方案（或者可能是有意的？）并且可能使实例在本应可解决的情况下意外不可行。

ILP 可以相对直接地对 Z/2³²Z 上的方程建模（使用 0 和 2³² 之间的整数变量和一些不受约束的附加变量按 2³² 缩放以“吸收”环绕），但它往往真的很难与这种公式相提并论——我想说这是没有 ILP 求解器的最坏情况之一进入“故意困难”的案件。具有 32x 布尔变量的更间接的模型也是可能的，但这会导致具有非常大的常量的约束，并且 ILP 求解器也倾向于与它们作斗争。总的来说，我不建议使用 ILP 来解决这个问题。

我推荐的是提供位向量理论的 SMT 求解器，或者伪布尔求解器或普通 SAT 求解器（这将留下实现布尔电路并将其转换为 CNF 的繁重工作给你，而不是让它们内置在求解器中）。

Answer 3

我按照@harold 的建议选择了 SMT 求解器。具体来说 CVC4 SMT Solver。这是我用 C++ 编写的代码，用于回答有关为 8 个方程组（限制为 ascii 字符）查找 16 个解 (w[0...15]) 的问题。不过我还有最后一个问题。 pushing 和 popping 是为了什么？ (slv.push() 和 slv.pop())

#include <iostream>
#include <cvc4/cvc4.h>

using namespace std;
using namespace CVC4;

int main() {
    // 1. initialize a CVC4 BitVector SMT solver
    ExprManager em;
    SmtEngine slv(&em);
    slv.setOption("incremental", true); // enable incremental solving
    slv.setOption("produce-models", true); // enable models
    slv.setLogic("QF_BV"); // set the bitvector theory logic
    Type bitvector8 = em.mkBitVectorType(size_8); // create a 8-bit wide bit-vector type (4 x 8-bit = 32-bit)

    // 2. create the SMT solver variables
    Expr w[16][4]; // w[0...15] where each w corresponds to 4 ascii characters

    for (int i = 0; i < 16; ++i) {
        for (int j = 0; j < 4; ++j) {
            // a. define w[i] (four ascii characters per w[i])
            w[i][j] = em.mkVar("w" + to_string(i) + to_string(j), bitvector8);

            // b. constraint w[i][0...3] to be an ascii character
            // - digit (0-9) constraint
            // ascii lower bound digit constraint (bit-vector unsigned greater than or equal)
            Expr digit_lower = em.mkExpr(kind::BITVECTOR_UGE, w[i][j], em.mkConst(BitVector(size_8, Integer(48))));

            // ascii upper bound digit constraint (bit-vector unsigned less than or equal)
            Expr digit_upper = em.mkExpr(kind::BITVECTOR_ULE, w[i][j], em.mkConst(BitVector(size_8, Integer(56))));
            Expr digit_constraint = em.mkExpr(kind::AND, digit_lower, digit_upper);

            // - lower alphanumeric character (a-z) constraint
            // ascii lower bound alpha constraint (bit-vector unsigned greater than or equal)
            Expr alpha_lower = em.mkExpr(kind::BITVECTOR_UGE, w[i][j], em.mkConst(BitVector(size_8, Integer(97))));

            // ascii upper bound alpha constraint (bit-vector unsigned less than or equal)
            Expr alpha_upper = em.mkExpr(kind::BITVECTOR_ULE, w[i][j], em.mkConst(BitVector(size_8, Integer(122))));
            Expr alpha_constraint = em.mkExpr(kind::AND, alpha_lower, alpha_upper);

            Expr ascii_constraint = em.mkExpr(kind::OR, digit_constraint, alpha_constraint);
            slv.assertFormula(ascii_constraint);
        }
    }

    // 3. encode the 8 equations
    for (int i = 0; i < 8; ++i) {
        // a. build the multiplication part (index * w[i])
        vector<Expr> left_mult_hand;

        for (int j = 0; j < 16; ++j) {
            vector <Expr> inner_wj;
            for (int k = 0; k < 4; ++k) inner_wj.push_back(w[j][k]);
            Expr wj = em.mkExpr(kind::BITVECTOR_CONCAT, inner_wj);

            Expr index = em.mkConst(BitVector(size_32, Integer(m_unknowns[j])));
            left_mult_hand.push_back(em.mkExpr(kind::BITVECTOR_MULT, index, wj));
        }

        // b. sum each index * w[i]
        slv.push();
        Expr left_hand = em.mkExpr(kind::BITVECTOR_PLUS, left_mult_hand);
        Expr result = em.mkConst(BitVector(size_32, Integer(globalSums.to_ulong())));
        Expr assumption = em.mkExpr(kind::EQUAL, left_hand, result);
        slv.assertFormula(assumption);

        // c. check for satisfiability
        cout << "Result from CVC4 is: " << slv.checkSat(em.mkConst(true)) << endl << endl;
        slv.pop();
    }

    return 0;
}

约束线性方程的解

Constraining the solutions for linear equations

linear-algebra

eigen

lapack

integer-programming