More‎ > ‎

How to Solve Verbal Arithmetic with Constraint Programming in Java with CHOCO3?

BY MARKUS SPRUNCK


This article describes basics of Constraint Programming with CHOCO3. Constraint Programming is a very powerful method to solve certain classes of real world problems and/or numerical puzzles.
For some tasks constraint programming is the fastest and shortest solution.  

The sample application demonstrates how to solve Verbal Arithmetic with CHOCO3 - a java library for constraint satisfaction problems and constraint programming. [1]

Definition of Verbal Arithmetic

Wikipedia says about verbal arithmetic: 

"Verbal arithmetic, also known as alphametics, cryptarithmetic, crypt-arithmetic, cryptarithm or word addition, is a type of mathematical game consisting of a mathematical equation among unknown numbers, whose digits are represented by letters. The goal is to identify the value of each letter. The name can be extended to puzzles that use non-alphabetic symbols instead of letters." [2]

A Simple Verbal Arithmetic Task

Maybe you know puzzles like:
  • SEND + MORE = MONEY
    Solution: 9567  + 1085   = 10652

  • CRACK + HACK = ERROR
    Solution: 42641  +  9641 = 52282
To solve these puzzles you have to replace each character in one of the equations with a integer number so that the numeric equation is correct.

Implementation

To compile and run this sample - CHOCO version 3.3.1 has been used. The most important methods are defineIntegerVariablesCharacters() which creates the needed variables for Choco3 and defineConstraints() where the puzzle is defined. In defineConstaints() method the following three constraints are defined:

1) The first digits are not allowed to be zero (this is not mandatory but it looks nicer if the first numbers are not null):

final Constraint a = IntConstraintFactory.arithm(this.intVarMap.get(this.inputFirst.substring(0, 1)), ">", 0);
final Constraint b = IntConstraintFactory.arithm(this.intVarMap.get(this.inputSecond.substring(0, 1)), ">", 0);
final Constraint c = LogicalConstraintFactory.and(a, b);
this.solver.post(c);

2) All characters have to be different from each other:

final IntVar[] allVariables = new IntVar[this.usedCharacters.length()];
for (int i = 0; i < this.usedCharacters.length(); i++) {
    allVariables[i] = this.intVarMap.get(this.usedCharacters.substring(i, i + 1));
}
this.solver.post(IntConstraintFactory.alldifferent(allVariables));

 3) Most important the "First + Second = Result" equation:

final IntVar first = setConstraint("First", this.inputFirst);
final IntVar second = setConstraint("Second", this.inputSecond);
final IntVar result = setConstraint("Result", this.inputResult);
IntVar[] summands = new IntVar[] { first, second };
this.solver.post(IntConstraintFactory.sum(summands, result));

Complete Solution

It is a good idea to take the source code version choco-solver-3.3.1-sources.jar, because it is sometimes very helpful to browse the implementation. 

// Copyright (C) 2012-2015, Markus Sprunck
package com.sw_engineering_candies.example;

import static com.google.common.base.Preconditions.checkArgument;
import static com.google.common.base.Preconditions.checkNotNull;

import java.util.HashMap;
import java.util.Map;

import org.chocosolver.solver.Solver;
import org.chocosolver.solver.constraints.Constraint;
import org.chocosolver.solver.constraints.IntConstraintFactory;
import org.chocosolver.solver.constraints.LogicalConstraintFactory;
import org.chocosolver.solver.search.solution.Solution;
import org.chocosolver.solver.variables.IntVar;
import org.chocosolver.solver.variables.VariableFactory;

/**
 * Sample application for solving Verbal Alphametic Equations with the CHOCO3
 * library. CHOCO is a java library for constraint satisfaction problems and
 * constraint programming.
 *
 * @see <a href="https://github.com/chocoteam/choco3">https://github.com/
 *      chocoteam/choco3</a>
 *
 */
public class VerbalArithmeticWithChoco3 {

	/**
	 * Field inputFirst is the first term.
	 */
	private final String inputFirst;

	/**
	 * Field inputSecond is the second term.
	 */
	private final String inputSecond;

	/**
	 * Field inputResult is the expected result.
	 */
	private final String inputResult;

	/**
	 * Field usedCharacters contains all used characters without duplicates.
	 */
	private final String usedCharacters;

	/**
	 * Field intVarMap holds all needed variables.
	 */
	private final Map<String, IntVar> intVarMap = new HashMap<String, IntVar>();

	/**
	 * Field solver for the model.
	 */
	private final Solver solver = new Solver();

	/**
	 * Constructor for VerbalArithmeticWithChoco3 the strings should not be
	 * empty and if possible upper case.
	 */
	public VerbalArithmeticWithChoco3(final String first, final String second, 
            final String result) {
		// Preconditions
		checkNotNull(first);
		checkArgument(!first.isEmpty());
		checkNotNull(second);
		checkArgument(!second.isEmpty());
		checkNotNull(result);
		checkArgument(!result.isEmpty());

		// Calculations just with upper case
		this.inputFirst = first.toUpperCase();
		this.inputSecond = second.toUpperCase();
		this.inputResult = result.toUpperCase();
		this.usedCharacters = removeDuplicateChar(first.concat(second).concat(result));

		// Solve with Choco3
		defineIntegerVariablesCharacters();
		defineConstraints();
		this.solver.findSolution();

		// Output
		printResults();
	}

	/**
	 * Method removeDuplicateChar creates a string with all containing
	 * characters.
	 */
	private static String removeDuplicateChar(final String input) {
		final StringBuffer result = new StringBuffer(input.length());
		for (int i = 0; i < input.length(); i++) {
			final String next = input.substring(i, i + 1);
			if (-1 == result.indexOf(next)) {
				result.append(next);
			}
		}
		return result.toString();
	}

	/**
	 * Method defineIntegerVariablesCharacters creates all needed variables.
	 */
	private void defineIntegerVariablesCharacters() {
		for (int i = 0; i < this.usedCharacters.length(); i++) {
			final String character = 
                            this.usedCharacters.substring(i, i + 1);
			this.intVarMap.put(character,    
                            VariableFactory.integer(character, 0, 9, this.solver));
		}
	}

	/**
	 * Method defineConstraints creates all constraints
	 */
	private void defineConstraints() {

		// 1st Constraint - the first digits are not allowed to be zero
		final Constraint a = IntConstraintFactory.arithm(this.intVarMap.get(
                    this.inputFirst.substring(0, 1)), ">", 0);
		final Constraint b = IntConstraintFactory.arithm(
                    this.intVarMap.get(this.inputSecond.substring(0, 1)), ">", 0);
		final Constraint c = LogicalConstraintFactory.and(a, b);
		this.solver.post(c);

		// 2nd Constraint - all characters have to be different
		final IntVar[] allVariables = new IntVar[this.usedCharacters.length()];
		for (int i = 0; i < this.usedCharacters.length(); i++) {
			allVariables[i] = this.intVarMap.get(this.usedCharacters.substring(i, i + 1));
		}
		this.solver.post(IntConstraintFactory.alldifferent(allVariables));

		// 3rd Constraint - the "First + Second = Result" equation
		final IntVar first = setConstraint("First", this.inputFirst);
		final IntVar second = setConstraint("Second", this.inputSecond);
		final IntVar result = setConstraint("Result", this.inputResult);
		IntVar[] summands = new IntVar[] { first, second };
		this.solver.post(IntConstraintFactory.sum(summands, result));
	}

	private IntVar setConstraint(final String name, final String term) {
		final IntVar result = VariableFactory.bounded(name, 0, VariableFactory.MAX_INT_BOUND, this.solver);
		this.solver.post(IntConstraintFactory.scalar(getIntVar(term), getFactors(term), result));
		return result;
	}

	private int[] getFactors(final String valueString) {
		final int[] coefficients = new int[valueString.length()];
		for (int i = 0; i < valueString.length(); i++) {
			coefficients[i] = (int) Math.pow(10, valueString.length() - i - 1);
		}
		return coefficients;
	}

	private IntVar[] getIntVar(final String valueString) {
		final IntVar[] values = new IntVar[valueString.length()];
		for (int i = 0; i < valueString.length(); i++) {
			values[i] = this.intVarMap.get(valueString.substring(i, i + 1));
		}
		return values;
	}

	private void printResults() {
		final StringBuffer buffer = new StringBuffer();
		buffer.append("\tTASK     : ");
		buffer.append(this.inputFirst);
		buffer.append(" + ");
		buffer.append(this.inputSecond);
		buffer.append(" = ");
		buffer.append(this.inputResult);
		buffer.append('\n');

		buffer.append("\tSOLUTION : ");
		final Solution solution = this.solver.getSolutionRecorder().getLastSolution();
		buffer.append((solution != null) ? solution.hasBeenFound() : "false");
		buffer.append('\n');

		buffer.append("\tRESULT   : ");
		buffer.append(getIntegerNumber(this.inputFirst));
		buffer.append(" + ");
		buffer.append(getIntegerNumber(this.inputSecond));
		buffer.append(" = ");
		buffer.append(getIntegerNumber(this.inputResult));

		System.out.println(buffer);
	}

	/**
	 * Method getIntegerNumber is a helper for output method of numbers
	 */
	private String getIntegerNumber(final String text) {
		final StringBuilder result = new StringBuilder();
		for (int i = 0; i < text.length(); i++) {
			final String variable = text.substring(i, i + 1);
			result.append(String.format("%d", this.intVarMap.get(variable).getValue()));
		}
		return result.toString();
	}

	/**
	 * Method main contains some test cases
	 */
	public static void main(final String[] args) {

		System.out.println("positive test case:");
		new VerbalArithmeticWithChoco3("CRACK", "HACK", "ERROR");

		System.out.println("\npositive test case:");
		new VerbalArithmeticWithChoco3("SEND", "MORE", "MONEY");

		System.out.println("\npositive test case:");
		new VerbalArithmeticWithChoco3("AGONY", "JOY", "GUILT");

		System.out.println("\npositive test case:");
		new VerbalArithmeticWithChoco3("APPLE", "LEMON", "BANANA");

		System.out.println("\npositive test case:");
		new VerbalArithmeticWithChoco3("SYSTEMA", "ATIMA", "SECURER");
	}
}

Expected Output of the Application

positive test case:
	TASK     : CRACK + HACK = ERROR
	SOLUTION : true
	RESULT   : 42641 + 9641 = 52282

positive test case:
	TASK     : SEND + MORE = MONEY
	SOLUTION : true
	RESULT   : 9567 + 1085 = 10652

positive test case:
	TASK     : AGONY + JOY = GUILT
	SOLUTION : true
	RESULT   : 89562 + 752 = 90314

positive test case:
	TASK     : APPLE + LEMON = BANANA
	SOLUTION : true
	RESULT   : 67794 + 94832 = 162626

positive test case:
	TASK     : SYSTEMA + ATIMA = SECURER
	SOLUTION : true
	RESULT   : 1413579 + 93279 = 1506858

Find Code on GitHub

References

Sponsored Link