我將首先通過一個例子來解釋什么是密碼學問題：
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 中實作它時遇到了麻煩。特別是我們為每個變數生成約束/域的部分。請記住，也涉及到攜帶。
編輯：我正在尋找一種使用我所說的概念為每個變數生成域的方法。
uj5u.com熱心網友回復：
這種問題對于谷歌開源的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方法。
在 sum 的約束中，運算子 * 和 == 在包中都被覆寫以創建模型可以使用的物件來強制執行約束。
這是列舉解決方案的輸出的開始
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_;
}
}
}
uj5u.com熱心網友回復：
一個完整的解決方案的方式超出范圍的簡單，這樣的問題，但我可以畫出你所需要的。
首先，為carry生成新字母：
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 并在那里表達您的問題。
轉載請註明出處，本文鏈接：https://www.uj5u.com/ruanti/325970.html
上一篇：使用push(x)、pop()和pop_max()方法實作佇列
下一篇：如何添加和恢復堆？