0

我将首先通过一个示例来解释什么是密码算术问题：

  T W O
+ T W O
F O U R

我们必须为每个字母分配一个数字 [0-9]，这样没有两个字母共享相同的数字，并且满足上述等式。

解决上述问题的一种方法是：

   7 6 5   
+  7 6 5       
 1 5 3 0

有两种方法可以解决这个问题，一种是蛮力，这会起作用，但这不是最佳方法。另一种方法是使用约束满足。

使用约束满足的解决方案
我们知道 R 将永远是偶数，因为它的 2 * O
这将 O 的域缩小到 {0, 2, 4, 6, 8}
我们也知道 F 只能是 1，因为 F 是'不是两个字母的加法，它必须从T + T = O
生成的进位中获取它的值 这也意味着T + T > 9，只有这样它才能为 F 生成一个进位；
这告诉我们T > 4 {5, 6, 7, 8, 9}
当我们继续这样做时，我们会不断缩小域的范围，这有助于我们将时间复杂度大大降低。

这个概念似乎很简单，但我在用 C++ 实现它时遇到了麻烦。尤其是我们为每个变量生成约束/域的部分。请记住，也有进位。

编辑：我正在寻找一种使用我所说的概念为每个变量生成域的方法。

4

3 回答 3

2

这类问题对于像 Google 的开源 OR-Tools 这样的通用约束编程包来说是一个很好的应用。（参见https://developers.google.com/optimization和https://developers.google.com/optimization/cp/cryptarithmetic）。

该软件包是用 c++ 编写的，因此它应该很适合您。

然后编程问题就这么简单（对不起，因为我在 c# 中使用 OR-Tools，这是 c# 代码，但 c++ 代码看起来几乎相同）

public void initModel(CpModel model)
        {
            // Make variables
            T = model.NewIntVar(0, 9, "T");
            W = model.NewIntVar(0, 9, "W");
            O = model.NewIntVar(0, 9, "O");
            F = model.NewIntVar(0, 9, "F");
            U = model.NewIntVar(0, 9, "U");
            R = model.NewIntVar(0, 9, "R");

            // Constrain the sum
            model.Add((2 * (100 * T + 10 * W + O)) == (1000 * F + 100 * O + 10 * U + R));

            // Make sure the variables are all different
            model.AddAllDifferent(decisionVariables);

            // The leading digit shouldn't be 0
            model.Add(T != 0);
            model.Add(F != 0);
        }

然后调用该Solve方法。

在求和的约束中，操作符* + 和 == 都在包中被覆盖，以创建模型可以用来强制约束的对象。

这是枚举解决方案的输出的开始

Solution #0: time = 0,00 s;
 T = 8
 W = 6
 O = 7
 F = 1
 U = 3
 R = 4

Solution #1: time = 0,01 s;
 T = 8
 W = 4
 O = 6
 F = 1
 U = 9
 R = 2

Solution #2: time = 0,01 s;
 T = 8
 W = 3
 O = 6
 F = 1
 U = 7
 R = 2

Solution #3: time = 0,01 s;
 T = 9
 W = 3
 O = 8
 F = 1
 U = 7
 R = 6

这是完整的代码，包括解决方案打印和执行的 Main 方法：

using Google.OrTools.Sat;
using System;
using System.IO;

namespace SO69626335_CryptarithmicPuzzle
{
    class Program
    {
        static void Main(string[] args)
        {
            try
            {
                Google.OrTools.Sat.CpModel model = new CpModel();
                ORModel myModel = new ORModel();
                myModel.initModel(model);
                IntVar[] decisionVariables = myModel.decisionVariables;

                // Creates a solver and solves the model.
                CpSolver solver = new CpSolver();
                VarArraySolutionPrinter solutionPrinter = new VarArraySolutionPrinter(myModel.variablesToPrintOut);
                solver.SearchAllSolutions(model, solutionPrinter);
                Console.WriteLine(String.Format("Number of solutions found: {0}",
                    solutionPrinter.SolutionCount()));
            }
            catch (Exception e)
            {
                Console.WriteLine(e.Message);
                Console.WriteLine(e.StackTrace);
                throw;
            }

            Console.WriteLine("OK");
            Console.ReadKey();
        }
    }

    class ORModel
    {
        IntVar T;
        IntVar W;
        IntVar O;
        IntVar F;
        IntVar U;
        IntVar R;

        public void initModel(CpModel model)
        {
            // Make variables
            T = model.NewIntVar(0, 9, "T");
            W = model.NewIntVar(0, 9, "W");
            O = model.NewIntVar(0, 9, "O");
            F = model.NewIntVar(0, 9, "F");
            U = model.NewIntVar(0, 9, "U");
            R = model.NewIntVar(0, 9, "R");

            // Constrain the sum
            model.Add((2 * (100 * T + 10 * W + O)) == (1000 * F + 100 * O + 10 * U + R));

            // Make sure the variables are all different
            model.AddAllDifferent(decisionVariables);

            // The leading digit shouldn't be 0
            model.Add(T != 0);
            model.Add(F != 0);
        }

        public IntVar[] decisionVariables
        {
            get
            {
                return new IntVar[] { T, W, O, F, U, R };
            }
        }

        public IntVar[] variablesToPrintOut
        {
            get
            {
                return decisionVariables;
            }
        }
    }

    public class VarArraySolutionPrinter : CpSolverSolutionCallback
    {
        private int solution_count_;
        private IntVar[] variables;

        public VarArraySolutionPrinter(IntVar[] variables)
        {
            this.variables = variables;
        }
        public override void OnSolutionCallback()
        {
            // using (StreamWriter sw = new StreamWriter(@"C:\temp\GoogleSATSolverExperiments.txt", true, Encoding.UTF8))
            using (TextWriter sw = Console.Out)
            {
                sw.WriteLine(String.Format("Solution #{0}: time = {1:F2} s;",
                solution_count_, WallTime()));
                foreach (IntVar v in variables)
                {
                    sw.Write(
                    String.Format(" {0} = {1}\r\n", v.ShortString(), Value(v)));
                }
                solution_count_++;
                sw.WriteLine();
            }
            if (solution_count_ >= 10)
            {
                StopSearch();
            }
        }
        public int SolutionCount()
        {
            return solution_count_;
        }
    }
}
于 2021-10-19T15:02:42.843 回答
1

一个完整的解决方案超出了一个简单的 SO 问题的范围，但我可以勾勒出您需要的内容。

首先，为进位生成新字母：

   0 T W O
   0 T W O
+  Z Y X V
   F O U R

然后您可以生成一个std::map<char, std::set<int>>包含所有选项的。字母的标准范围是 {0..9}，V 是 {0}，Z 是 {1}，Y 和 X 是 {0..1}。

接下来，您需要将添加的内容编码为一组子句。

enum class Op { Equal, SumMod10, SumDiv10, Even, Odd };
struct clause { Op op; std::vector<Var> children; };

std::vector<clause> clauses{
{Equal, { 'Z' , 'F'}},
{SumMod10, {'O', 'T', 'T', 'Y'}}, // O = (T+T+Y) mod 10
{SumMod10, {'U', 'W', 'W', 'X'}},
{SumMod10, {'R', 'O', 'O', 'V'}},
{SumDiv10, {'F', 'T', 'T', 'Y'}}, // F is the carry of T+T+Y
{SumDiv10, {'O', 'W', 'W', 'X'}},
{SumDiv10, {'U', 'O', 'O', 'V'}},
};

然后有趣的部分开始了：您需要创建一个计算，该计算将尝试使用它所拥有的知识来简化约束。例如，{SumMod10, {'U', 'O', 'O', 'V'}}可以简化为{SumMod10, {'U', 'O', 'O', 0}}since V=0。有时子句可以缩小变量的范围，例如{Equal, {'Z', 'F'}}约束可以立即将范围缩小F到 {0,1}。

接下来，您需要教您的系统有关基本代数等式以进一步简化，例如： {SumMod10, {A, 0, C}} === {SumMod10, {A, C, 0}} === {Equal, {A,C}} 甚至更抽象的东西，例如“如果 A >= 5 且 B >= 5 则 A+B >= 10”或“如果 A 是偶数B 是偶数，那么 A + B 也是偶数”。

最后，您的系统需要能够假设假设并反驳它们，或者证明一个假设无论如何都是正确的，就像您在帖子中所做的那样。例如，假设 R 是奇数就意味着 O + O 是奇数，这只有在 O 同时是奇数和偶数时才会发生。因此 R 必须是偶数。

最终，您将不仅实现了一个用于描述和评估数字域中的布尔子句的正式系统，您还将拥有一个目标驱动的解决方案引擎。如果这不仅仅是一种无聊的思考，我会强烈考虑采用 SMT 系统来为你解决这个问题，或者至少学习 Prolog 并在那里表达你的问题。

于 2021-10-19T10:27:11.373 回答
0

这是我使用回溯解决它的方法

我在这里的方法是巧妙地暴力破解它，我递归地将每个可能的值 [0-9] 分配给每个字母并检查是否存在任何矛盾。

矛盾可以是以下之一：

  • 两个或多个字母最终具有相同的值。
  • 字母总和与结果字母的值不匹配。
  • 字母总和已分配给某个字母。

一旦发生矛盾，该特定组合的递归就结束。

#include <bits/stdc++.h>

using namespace std;

vector<string> words, wordOg;
string result, resultOg;
bool solExists = false;

void reverse(string &str){
    reverse(str.begin(), str.end());
}

void printProblem(){
    cout<<"\n";
    for(int i=0;i<words.size();i++){
        for(int j=0;j<words[i].size();j++){
            cout<<words[i][j];
        }
        cout<<"\n";
    }
    cout<<"---------\n";
    for(int i=0;i<result.size();i++){
        cout<<result[i];
    }
    cout<<"\n";
}

void printSolution(unordered_map<char, int> charValue){
    cout<<"\n";
    for(int i=0;i<words.size();i++){
        for(int j=0;j<words[i].size();j++){
            cout<<charValue[wordOg[i][j]];
        }
        cout<<"\n";
    }
    cout<<"---------\n";
    for(int i=0;i<result.size();i++){
        cout<<charValue[resultOg[i]];
    }
    cout<<"\n";
}

void solve(int colIdx, int idx, int carry, int sum,unordered_map<char, int> charValue, vector<int> domain){


    if(colIdx<words.size()){
        if(idx<words[colIdx].size()){
            char ch = words[colIdx][idx];
            if(charValue.find(ch)!=charValue.end()){
                solve(colIdx + 1, idx, carry, sum + charValue[ch], charValue, domain);
            }
            else{
                for(int i=0;i<10;i++){
                    if(i==0 && idx==words[colIdx].size()-1) continue;
                    if(domain[i]==-1){
                        domain[i] = 0;
                        charValue[ch] = i;
                        solve(colIdx + 1, idx, carry, sum + i, charValue, domain);
                        domain[i] = -1;
                    }
                }
            }
        }
        else solve(colIdx + 1, idx, carry, sum, charValue, domain);
    }
    else{
        if(charValue.find(result[idx])!=charValue.end()){
            if(((sum+carry)%10)!=charValue[result[idx]]) return;
        }
        else{
            if(domain[(sum + carry)%10]!=-1) return;
            domain[(sum + carry)%10] = 0;
            charValue[result[idx]] = (sum + carry)%10;
        }
        carry = (sum+carry)/10;
        if(idx==result.size()-1 && (charValue[result[idx]]==0 || carry == 1)) return;
        if(idx+1<result.size()) solve(0, idx+1, carry, 0, charValue, domain);
        else{
            solExists = true;
            printSolution(charValue);
        }
    }
}

int main() {
    unordered_map<char, int> charValue;
    vector<int> domain(10,-1);

    int n;
    cout<<"\nEnter number of input words: ";
    cin>>n;
    cout<<"\nEnter the words: ";
    for(int i=0;i<n;i++){
        string inp;
        cin>>inp;
        words.push_back(inp);
    }
    cout<<"\nEnter the resultant word: ";
    cin>>result;

    printProblem();

    wordOg = words;
    resultOg = result;

    reverse(result);
    for(auto &itr: words) reverse(itr);

    solve(0, 0, 0, 0, charValue, domain);

    if(!solExists) cout<<"\nNo Solution Exists!";
    return 0;
}
于 2021-12-15T06:28:33.133 回答