如何在 C++ 中使用约束满足来实现 Cryptarithmetic
How to implement Cryptarithmetic using Constraint Satisfaction in C++
我将首先通过一个例子来解释什么是密码算法问题：
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[ 生成的进位中获取其值=30=]
这也意味着T + T > 9，只有这样才能为F生成进位；
这告诉我们 T > 4 {5, 6, 7, 8, 9}
随着我们继续这样做，我们不断缩小领域，这有助于我们大大降低时间复杂度。
这个概念似乎很简单，但我在用 C++ 实现它时遇到了问题。特别是我们为每个变量生成 constraints/domain 的部分。请记住，也有进位。
编辑：我正在寻找一种使用我陈述的概念为每个变量生成域的方法。
完整的解决方案方式超出了简单 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}}，因为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 也是偶数”。
最后，您的系统需要能够假设并反驳它们，或者证明假设无论如何都是正确的，就像您在 post 中所做的那样。
例如，假设 R 是奇数将意味着 O + O 是奇数，这只有在 O 同时是奇数和偶数时才会发生。因此R必须是偶数。
最终，您将不仅实现了一个用于描述和评估数字域中的布尔子句的正式系统，而且还将拥有一个目标驱动的解决方案引擎。如果这不仅仅是一个无聊的思考，我会强烈考虑采用 SMT 系统来为您解决这个问题，或者至少学习 Prolog 并在那里表达您的问题。
这类问题可以很好地应用通用约束编程包，例如 Google 的开源 OR-Tools。 （参见 https://developers.google.com/optimization and 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
下面是完整的代码，包括解决方案打印和执行的主要方法：
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_;
}
}
}
这是我使用回溯法解决的方法
我这里的方法是巧妙地暴力破解它，我递归地为每个字母分配每个可能的值 [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;
}
我将首先通过一个例子来解释什么是密码算法问题：
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[ 生成的进位中获取其值=30=]
这也意味着T + T > 9，只有这样才能为F生成进位；
这告诉我们 T > 4 {5, 6, 7, 8, 9}
随着我们继续这样做，我们不断缩小领域，这有助于我们大大降低时间复杂度。
这个概念似乎很简单，但我在用 C++ 实现它时遇到了问题。特别是我们为每个变量生成 constraints/domain 的部分。请记住，也有进位。
编辑：我正在寻找一种使用我陈述的概念为每个变量生成域的方法。
完整的解决方案方式超出了简单 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}}，因为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 也是偶数”。
最后，您的系统需要能够假设并反驳它们，或者证明假设无论如何都是正确的，就像您在 post 中所做的那样。 例如，假设 R 是奇数将意味着 O + O 是奇数，这只有在 O 同时是奇数和偶数时才会发生。因此R必须是偶数。
最终，您将不仅实现了一个用于描述和评估数字域中的布尔子句的正式系统，而且还将拥有一个目标驱动的解决方案引擎。如果这不仅仅是一个无聊的思考，我会强烈考虑采用 SMT 系统来为您解决这个问题，或者至少学习 Prolog 并在那里表达您的问题。
这类问题可以很好地应用通用约束编程包，例如 Google 的开源 OR-Tools。 （参见 https://developers.google.com/optimization and 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
下面是完整的代码，包括解决方案打印和执行的主要方法：
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_;
}
}
}
这是我使用回溯法解决的方法
我这里的方法是巧妙地暴力破解它，我递归地为每个字母分配每个可能的值 [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;
}