I'll start by explaining what a cryptarithmetic problem is, through an example:
T W O
T W O
F O U R
We have to assign a digit [0-9] to each letter such that no two letters share the same digit and it satisfies the above equation.
One solution to the above problem is:
7 6 5
7 6 5
1 5 3 0
There are two ways to solve this problem, one is brute force, this will work but it's not the optimal way. The other way is using constraint satisfaction.
Solution using Constraint Satisfaction
We know that R will always be even because its 2 * O
this narrows down O's domain to {0, 2, 4, 6, 8}
We also know that F can't be anything but 1, since F isn't an addition of two letters, it must be getting its value from carry generated by T T = O
This also implies that T T > 9, only then will it be able to generate a carry for F;
This tells us that T > 4 {5, 6, 7, 8, 9}
And as we go on doing this, we keep on narrowing down the domain and this helps us reduce time complexity by a considerable amount.
The concept seems easy, but I'm having trouble implementing it in C . Especially the part where we generate constraints/domain for each variable. Keep in mind that there are carries involved too.
EDIT: I'm looking for a way to generate a domain for each variable using the concept I stated.
CodePudding user response：
A full solution is way out of scope for a simple SO question, but I can sketch what you would need.
First, generate new letters for the carries:
0 T W O
0 T W O
Z Y X V
F O U R
You can then generate a std::map<char, std::set<int>> containing all the options. The letters have the standard range {0..9}, V is {0}, Z is {1} and Y and X have {0..1}.
Next, you need to encode the additions into a set of clauses.
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'}},
};
Then the fun part begins: you need to create a calculation that will try to simplify the constraints using the knowledge it has.
For example, {SumMod10, {'U', 'O', 'O', 'V'}} can be simplified to {SumMod10, {'U', 'O', 'O', 0}} since V=0.
Sometimes a clause can reduce the range of a variable, for example the {Equal, {'Z', 'F'}} constraint can immediately reduce the range of F to {0,1}.
Next, you need to teach your system about basic algebraic equalities for furhter simplification, such as:
{SumMod10, {A, 0, C}} === {SumMod10, {A, C, 0}} === {Equal, {A,C}}
and even more abstract things like "if A >= 5 and B >= 5 then A B >= 10" or "if A is even and B is even then A B is also even".
Finally, your system needs to be able to assume hypotheses and disprove them, or prove that a hypothesis is true no matter what, like you did in your post. For example, assuming that R is odd would mean that O O is odd, which can only happen if O is odd and even at the same time. Therefore R must be even.
At the end of the day, you will have implemented not only a formal system for describing and evaluating boolean clauses in the numbers domain, you will also have a goal-driven solution engine to go with it. If this is more than just an idle musing, I would strongly look into adoption an SMT system to solve this for you or at least learning Prolog and expressing your problem there.
CodePudding user response：
This kind of problem is a good application for generic constraint programming packages like Google's open source OR-Tools. (See https://developers.google.com/optimization and https://developers.google.com/optimization/cp/cryptarithmetic).
The package is written in c , so it should be a good match for you.
Then programming the problem is as simple as this (sorry, since I work with OR-Tools in c#, this is c# code, but the c code will look pretty much the same)
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);
}
and then calling the Solve method.
In the constraint for the sum, the operators* and == are all overridden in the package to create objects that can be used by the model to enforce the constraint.
This is the start of the output which enumerates the solution
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
And here's the complete code including solution printing and Main method for the execution:
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_;
}
}
}