Solving a satisfiability problem

The basic search strategy in CP Optimizer can be used to solve satisfiability problems.

The process for finding solutions to constraint satisfaction problems is similar to the process for finding solutions to optimization problems.

Consider this satisfiability problem, written in the C++ API:

    IloIntVar x(env, 0, 7, "x");
    IloIntVar y(env, 0, 7, "y");
    IloIntVar z(env, 0, 7, "z");
    IloIntVarArray all(env, 3, x, y, z);
    model.add(IloAllDiff(env, all));
    model.add(y == IloElement(IloIntArray(env, 7, 3, 7, 8, 8, 0, 1, 4), x));

A typical code for finding a solution to this model would look like:

    IloCP cp(model);
    cp.setParameter(IloCP::LogVerbosity, IloCP::Quiet);
    if (cp.solve()){
      cp.out() << " A solution has been found" 
               << ", x = " << cp.getValue(x)
               << ", y = " << cp.getValue(y)
               << ", z = " << cp.getValue(z) << std::endl;
    } else {
      cp.out() << " The problem has no solution " << std::endl;
    }

Running this code produces the output:

A solution has been found, x = 4, y = 0, z = 1

For constraint satisfaction problems, the search stops at the first solution encountered, thus there are no intermediate solutions found. However, it is possible to produce all solutions to a constraint satisfaction problem. For the model at the start of this section, running the code:

    IloCP cp(model);
    cp.setParameter(IloCP::LogVerbosity, IloCP::Quiet);
    cp.startNewSearch();
    while(cp.next()){
      cp.out() << "x = " << cp.getValue(x)
               << ", y = " << cp.getValue(y)
               << ", z = " << cp.getValue(z) << std::endl;
    }
    cp.end();

produces the 30 distinct solutions of the model:

x = 4, y = 0, z = 1
x = 4, y = 0, z = 2
x = 4, y = 0, z = 3
x = 4, y = 0, z = 5
x = 4, y = 0, z = 6
x = 4, y = 0, z = 7
x = 0, y = 3, z = 1
x = 0, y = 3, z = 2
x = 0, y = 3, z = 4
x = 0, y = 3, z = 5
x = 0, y = 3, z = 6
x = 0, y = 3, z = 7
x = 5, y = 1, z = 0
x = 5, y = 1, z = 2
x = 5, y = 1, z = 3
x = 5, y = 1, z = 4
x = 5, y = 1, z = 6
x = 5, y = 1, z = 7
x = 1, y = 7, z = 0
x = 1, y = 7, z = 2
x = 1, y = 7, z = 3
x = 1, y = 7, z = 4
x = 1, y = 7, z = 5
x = 1, y = 7, z = 6
x = 6, y = 4, z = 0
x = 6, y = 4, z = 1
x = 6, y = 4, z = 2
x = 6, y = 4, z = 3
x = 6, y = 4, z = 5
x = 6, y = 4, z = 7

In the C++ API of CP Optimizer, you use the class IloCP and the methods IloCP::getValue, IloCP::getObjValue, IloCP::startNewSearch, IloCP::next and IloCP::end.

In the Java™ API of CP Optimizer, you use the class IloCP and the methods IloCP.solve, IloCP.getValue, IloCP.getObjValue, IloCP.startNewSearch, IloCP.next and IloCP.end.

In the C# API of CP Optimizer, you use the class CP and the methods CP.Solve, CP.GetValue, CP.GetObjValue, CP.StartNewSearch, CP.Next and CP.End.