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:

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);

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)); 

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