Using Saffron to solve the Minimum Test Set problem

Let U be a nonempty set, S a nonempty family of subsets of U. Does there exist a sub family S' of K subsets in S which have the following property: For any distinct elements x and y in U, for every subset T in S', we have either x is in T and y is not, or vice versa.

This problem is clearly equivalent to the following: Given a set S of bit strings of equal length, does there exist a sub family S' of K bit strings in S such that for any distinct bit positions i and j, for every bit string T in S' we have T[i] !=T[j]? The following application solves this equivalent problem.

MinimumTestSetterDemo

package showcase.testset;

import bits.BooleanLiteral;
import bits.Conjunction;
import bits.IBitString;
import bits.IProblem;
import bits.IProblemMessage;
import bits.Problem;
import bitstrings.BitString;
import bitstrings.BitStringFixer;
import bitstrings.MinimumTestSetter;

public class MinimumTestSetterDemo
{
private static String cstring(int i, int j, char c)
{
char[] s = new char[j + 1];
for (int k = 0; k <= j; k++)
if (k == i || k == j)
s[k] = c;
else
s[k] = ' ';
return new String(s);
}

public static void main(String[] args) throws Exception
{
/**
* Set Java variables:
*/

int K = 3;

/**
* Set globals:
*/

/**
* Create Saffron objects and arrays:
*/

IBitString[] S = new IBitString[]
{ new BitString("01000"), new BitString("01011"),
new BitString("10100"), new BitString("01100"),
new BitString("11010"), new BitString("10010"),
new BitString("01010") };

int cLength = S.length;
int cSize = S[0].size();

IBitString includedInTestSet = new BitString(cLength);

/**
* Create problems which constrain the values of these Saffron objects:
*/

IProblem bsf = new BitStringFixer(S);
IProblem mts = new MinimumTestSetter(S, K, includedInTestSet);

/**
* Create the IProblem of satisfying all of these constraining problems:
*/

IProblem problem = new Conjunction(bsf, mts);

/**
* Solve the IProblem:
*/

IProblemMessage s = problem.findModel(Problem.defaultSolver());

if (s.getStatus() == IProblemMessage.SATISFIABLE
&& s.getLiterals().size() > 0)
{
BooleanLiteral.interpret(s.getLiterals());

System.out.println("PROBLEM");
for (int i = 0; i < cLength; i++)
System.out.println("C[" + i + "]=" + S[i].toBits());

System.out.println("\nSOLUTION");
for (int i = 0; i < cLength; i++)
if (includedInTestSet.getBooleanVariable(i).getValue())
System.out.println("C[" + i + "]=" + S[i].toBits());

System.out.println("\nVERIFICATION");
for (int i = 0; i < cSize; i++)
for (int j = i + 1; j < cSize; j++)
{
if (i == j)
continue;
for (int k = 0; k < cLength; k++)
{
boolean ci = S[k].getBooleanVariable(i).getValue();
boolean cj = S[k].getBooleanVariable(j).getValue();

boolean v1 = ci && !cj;
boolean v2 = !ci && cj;
boolean v3 = v1 || v2;
if (v3)
{

System.out.println(S[k].toBits());

System.out.println(cstring(i, j, '^'));
break;
}
}
}
}
else
System.out.println("No solution.");

}
}

MinimumTestSetter.java

package bitstrings;

import naturalnumbers.BitStringTotaler;
import naturalnumbers.NaturalNumber;
import naturalnumbers.NaturalNumberFixer;
import bits.BitFixer;
import bits.Conjunction;
import bits.Disjunction;
import bits.IBitString;
import bits.IBooleanVariable;
import bits.INaturalNumber;
import bits.IProblem;
import bits.Problem;

public class MinimumTestSetter extends Problem implements IProblem
{
public MinimumTestSetter(IBitString[] C, int K, IBitString includedInTestSet)
throws Exception
{
int cLength = C.length;
int cSize = C[0].size();

INaturalNumber NNK = new NaturalNumber(K);

int problemIndex = 0;
IProblem[] problemArray = new IProblem[cSize * cSize - cSize];

for (int i = 0; i < cSize; i++)
for (int j = 0; j < cSize; j++)
{
if (i == j)
continue;
IProblem[] parray = new IProblem[cLength];
for (int k = 0; k < cLength; k++)
{
// (C[k][i] && !C[k][j]) || (!C[k][i] && C[k][j])
IBooleanVariable ci = C[k].getBooleanVariable(i);
IBooleanVariable cj = C[k].getBooleanVariable(j);

parray[k] = new Disjunction(new Conjunction(new BitFixer(
ci, true), new BitFixer(cj, false)),
new Conjunction(new BitFixer(ci, false),
new BitFixer(cj, true)));
}
problemArray[problemIndex++] = new ConditionalDisjunction(
parray, includedInTestSet);
}

this.setClauses(new Conjunction(new BitStringTotaler(includedInTestSet,
NNK), new NaturalNumberFixer(NNK),
new Conjunction(problemArray)).getClauses());
}
}

OUTPUT:

PROBLEM
C[0]=01000
C[1]=01011
C[2]=10100
C[3]=01100
C[4]=11010
C[5]=10010
C[6]=01010

SOLUTION
C[3]=01100
C[5]=10010
C[6]=01010

VERIFICATION
01000
^^
01100
^ ^
01011
^  ^
01011
^   ^
01000
 ^^
01000
 ^ ^
01000
 ^  ^
01011
  ^^
01011
  ^ ^
11010
   ^^