Using Saffron to solve the Set Atomic Basis Problem

Given a set U and a family C of subsets of U of equal size, does there exists a family B of sets (called atoms), not necessarily members of C, such that (1) the members of B are pairwise disjoint, (2) for every member c in C, there exists a subfamily of B whose union is exactly equal to c, and (3) the union of all members of B equals U?

As usual, we model sets as bit strings, where disjoint bit strings are those whose bitwise AND equals the bit string consisting of all zeroes, and unions of bit strings are the result of their bitwise OR.

BitStringBitAtomerDemo.java

package showcase.bitstringbitatom;

import java.util.ArrayList;

import utility.Bitstrings;
import bits.BooleanLiteral;
import bits.Conjunction;
import bits.IBitString;
import bits.IProblem;
import bits.IProblemMessage;
import bits.Problem;
import bitstrings.BitString;
import bitstrings.BitStringBitAtomer;
import bitstrings.BitStringFixer;

public class BitStringBitAtomerDemo extends Problem implements IProblem
{
public static void main(String[] args) throws Exception
{
IBitString[] C = new IBitString[5];
for (int i = 0; i < 5; i++)
{
String str = Bitstrings.randomBitstring(12);
C[i] = new BitString(str);
}

System.out.println("INPUT STRINGS:");
for (int i = 0; i < C.length; i++)
{
System.out.println(C[i].toBits());
}

IBitString atomBitString = new BitString(C[0].size());
ArrayList<String> atoms = new ArrayList<String>();
for (int pos = 0; pos < C[0].size(); pos++)
{
IProblemMessage s = new Conjunction(new BitStringFixer(C),
new BitStringBitAtomer(C, pos, atomBitString))
.findModel(Problem.defaultSolver());
if (s.getStatus() == IProblemMessage.SATISFIABLE
&& s.getLiterals().size() > 0)
{
BooleanLiteral.interpret(s.getLiterals());
String hsb = atomBitString.toBits();
if (!atoms.contains(hsb))
{
atoms.add(hsb);
}
}
else
System.out.println("No solution.");
}

System.out.println("\nOUTPUT ATOMS:");
for (int i = 0; i < atoms.size(); i++)
{
System.out.println(atoms.get(i));
}
}
}

BitStringBitAtomer.java

package bitstrings;

import bits.BitFixer;
import bits.Conjunction;
import bits.Disjunction;
import bits.IBitString;
import bits.IProblem;
import bits.Problem;
import bitstrings.BitString;
import bitstrings.BitStringAnder;
import bitstrings.BitStringEqualizer;
import bitstrings.BitStringNoter;
import exceptions.bitstrings.BitStringBitAtomerException;

public class BitStringBitAtomer extends Problem implements IProblem
{
public BitStringBitAtomer(IBitString[] bitStrings, int pos, IBitString atom)
throws Exception
{
if (bitStrings.length == 0)
throw (new BitStringBitAtomerException(
"IBitString or IBooleanVariable array of zero length was passed to constructor."));
if (atom == null)
throw (new BitStringBitAtomerException(
"A null conditionalResult variable was passed to constructor."));
if (atom.size() == 0)
throw (new BitStringBitAtomerException(
"A conditionalResult of size zero was passed to constructor."));

int stagingIndex = 0;
IProblem[] stagingArray = new IProblem[bitStrings.length + 2];

IBitString[] subTotal = new IBitString[bitStrings.length];
for (int i = 0; i < bitStrings.length; i++)
subTotal[i] = new BitString(bitStrings[0].size());

stagingArray[stagingIndex++] = stagingArray[stagingIndex++] = new Conjunction(
// if bitStrings[0][pos] then subTotal[0]=bitStrings[0]
new Disjunction(new BitFixer(
bitStrings[0].getBooleanVariable(pos), false),
new BitStringEqualizer(subTotal[0], bitStrings[0])),
// if !bitStrings[0][pos] then subTotal[0]=!bitStrings[0]
new Disjunction(new BitFixer(bitStrings[0]
.getBooleanVariable(pos), true), new BitStringNoter(
subTotal[0], bitStrings[0])));

for (int i = 1; i < bitStrings.length; i++)
{
IBitString notbits = new BitString(bitStrings[i].size());
stagingArray[stagingIndex++] = new Conjunction(
new Disjunction(new BitFixer(
bitStrings[i].getBooleanVariable(pos), false),
new BitStringAnder(subTotal[i - 1], bitStrings[i],
subTotal[i])),
new Disjunction(new BitFixer(bitStrings[i]
.getBooleanVariable(pos), true),
new BitStringAnder(subTotal[i - 1], notbits,
subTotal[i])), new BitStringNoter(
bitStrings[i], notbits));
}

stagingArray[stagingIndex++] = new BitStringEqualizer(atom,
subTotal[bitStrings.length - 1]);

this.setClauses(new Conjunction(stagingArray).getClauses());
}
}

OUTPUT:

INPUT STRINGS:
111000011110
101101101011
101010110010
011101011101
111000000111

OUTPUT ATOMS:
100000000010
010000000100
001000000000
000101000000
000010000000
000000100000
000000010000
000000001000
000000000001