标签: solver

嗨,我遇到了这个拼图,这是一个名为Cryptarithms的着名的单词和基于数字的谜题的子集.假设你有一个表达式

发送+更多=金钱

现在有趣的部分是,每个字母表代表0-9的唯一数字.我想编写一个广义求解器,但最后我写了一个粗暴的强制解决方案.任何接受者如何解决它？

我认为可以使用谓词逻辑或集合论来解决.我特别感兴趣的是找到基于C#或Python的解决方案.任何人.？

我在C#中有一个应用程序,我需要做一些优化计算,就像Excel Solver Add-in一样,一个选项肯定是编写我自己的求解器实现,但是我有点时间,所以我正在研究已经存在的库可以帮助我解决这个问题.

我一直在尝试微软解决方案基金会,这看起来非常整洁和酷,问题是它似乎不适用于我需要做的那种计算.

在这个问题的最后,我正在添加有关我需要执行和优化的计算的信息.

所以基本上我的问题是,如果你们中的任何人知道我可以用于此目的的任何其他库,或任何可以帮助我自己的解算器的教程,或任何让我领导解决这个问题的想法.

谢谢.

附加信息:

这是我需要计算的数据:

我有7个变量,我们称之为var1,var2,...,var7

这些变量的约束是:

• 所有这些都需要为0 <= varn <= 0.5(其中n是变量的数量)
• 所有变量的总和应该等于1

目标是最大化目标公式,在Excel中如下所示:

 (MMULT(TRANSPOSE(L26:L32),M14:M20)) / (SQRT(MMULT(MMULT(TRANSPOSE(L26:L32),M4:S10),L26:L32))) 

您在此公式中看到的范围L26:L32实际上是包含上述变量的范围,var1,var2,...,varn.

M14:M20和M4:S10是具有从不同来源获得的数据的范围,更可能是十进制值.

正如我之前所说,我使用的是Microsoft Solver Foundation,我用它来模拟几乎所有东西,我创建了处理目标公式操作的函数,但是当我尝试解决模型时它总是失败,我认为这是因为操作的复杂性.

在任何情况下,我只是想显示这些数据,以便您可以了解我需要实现的计算类型.

我正在寻找一个C#dll来解决简单的等式.示例..

10 = 2 + 3 + x

结果应为x = 5;

有免费的DLL吗？

我一直在寻找一个用c ++编写的库来解决这样一个未确定的系统

q是矢量,w,x,y,z变量和a,b,c,d常数.

argmin_q MAX(q) - MIN(q)

ST

q[1] = a - w - y
q[2] = b - w - z
q[3] = c - x - y
q[4] = d - x - z 

找到求解器,算法等非常有用.我发现有几个库能够解决未确定的系统,但另外我需要最小化系数之间的距离.

先感谢您

altober

我最近开始使用MathNet来实现我们的线性代数,但是我在将MATLAB函数转换为MathNet时遇到了一些麻烦.

在MATLAB中,我经常使用反斜杠运算符来简单求解:

C = A\B

MathNet中的等价物是什么？

我使用C = Inv(A)*B在小矩阵中得到相同的结果,但我不知道结果是否精确.

有时<statement> solve_direct（我通常通过调用<statement> try）列出一些库定理并说“当前的目标可以直接解决：……”。

设<theorem>一个搜索结果solve_direct，然后在大多数情况下我可以证明<statement> by (rule theorem)。

然而，有时这样的证明不被接受，导致错误信息“应用初始证明方法失败”。

是否有一种通用的、不同的技术来重用由 找到的定理solve_direct？

还是要看个人情况？我可以尝试找出一个最小的例子并将其附加到这个问题上。

在我的多线程 c# 应用程序中使用 Microsoft Solver Foundation 时遇到问题：

我同时运行两个线程，并在每个线程上调用这样的函数：

private void exampleFunction()
{
    SolverContext context;
    Model model;

    for(int i=0;i<10;i++)
    {
        context = SolverContext.GetContext();
        model = context.CreateModel();

        //adding decisions, constraints and goal to model

        Solution sol = context.Solve();
        string s = sol.Quality.ToString();//and here sometimes I get that sol is null!
        context.ClearModel();
    }
}

看起来我在每个线程中的上下文都是同一个对象，所以当我调用

context.ClearModel();

在线程 1 中，那么在线程 2 中也很清楚（即使线程 2 中的问题尚未解决）。

所以问题是：有没有办法在 MSF 中同时求解两个模型？是否可以声明两个不同的 SolverContext？

在 Isabelle，我经常发现我可以使用不同的求解器成功地证明一个目标。

通常，我更愿意使用可以证明目标的最弱求解器。根据我目前与 Isabelle 的经验，我目前的理解是，按照强度增加和速度降低的顺序，常见的逻辑求解器排名如下（即何时rule和simp两者都起作用，rule应该使用等）：

rule < simp < auto < fastforce < force

这样对吗？这里blast适合放哪里？

我检查编程和伊莎贝尔/ HOL（PDF）证明和与伊莎贝尔/ HOL具体语义，但无法找到答案。

我正在构思一个名为multi-sudoku的数独变种的解算器,其中多个板重叠如下:

如果我正确理解游戏,您必须以这样的方式解决每个网格,即任何两个或更多网格之间的重叠是每个网格解决方案的一部分.

我不确定我应该怎么想这个.任何人都有任何提示/概念线索？此外,如果想到人工智能中的任何主题,我也想听听.

我正在尝试编写一个可以解决数独的算法。现在，我的代码可以工作，直到 supplyGrid 没有数字为止。当它发生时，它应该返回并尝试另一个号码，对吗？老实说，我不知道如何实现这一目标。

var grid = [
    [0, 0, 0, 0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0, 0, 0, 0],
    [0, …