约束线性方程组的解

编程问答 2022-05-15

问题描述

我正在寻找一种方法来求解线性方程组。具体8个方程，共16个未知值。

Diag1

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

对于

Diag2

：

Diag3

我尝试将这个线性方程组写成一个单一的矩阵方程。这给出了：

Diag4

现在，使用 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”）之间的整数。

目前的 16 个解决方案：

Diag5

我已经使用一种叫做Box-constraints 的东西找到了解决这个问题的方法。示例here 使用python 的lsq_linear 函数显示，该函数允许用户指定边界。似乎 Eigen 不允许用户在其 decomposition methods 中指定边界。

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

提前致谢。

解决方法

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

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

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

,

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

更进一步，如果您对变量有界限，即混合等式和不等式，那么您的问题最好以 linear programming 形式提出。您可以设置虚拟目标函数 c[i] = 0，也可以使用 GLPK，但这是一个非常通用的解决方案。如果您想截取一小段代码，您可能可以找到满足您需求的 Simplex 方法的玩具实现。

,

我按照@harold 的建议选择了 SMT 求解器。特别是 CVC4 SMT Solver。这是我用 C++ 编写的代码，回答了我关于为 8 个方程组找到 16 个解 (w[0...15]) 的问题，这些方程限制为 ascii 字符。不过我还有最后一个问题。什么是推动和弹出？ （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,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,Integer(97))));

            // ascii upper bound alpha constraint (bit-vector unsigned less than or equal)
            Expr alpha_upper = em.mkExpr(kind::BITVECTOR_ULE,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;
}
eigeninteger-programminglapacklinear-algebra