import java.io.*; import java.util.*; public class Optimization { private static final Scanner cin = new Scanner(System.in); public static void main(String[] args) { for(int iCase = 1; ; iCase++) { TestCase testCase = TestCase.scan(cin); if(testCase == null) { break; } if(iCase > 1) { System.out.println(); } System.out.println("Case " + iCase + ":"); testCase.solve(); testCase.print(System.out); } } private static class TestCase { private final char[] func; private final int n; private Set remain; private Set output; private static final char NOVAL = '-'; private static final char DONE = '+'; private static final char FALSE = '0'; private static final char TRUE = '1'; private static final char UNDEF = 'x'; // pattern == rule | (mask << N) private static final int N = 16; private static final int M = (1 << N) - 1; private TestCase(int n) { this.func = new char[1 << n]; this.n = n; this.remain = new HashSet(); this.output = new HashSet(); } public static TestCase scan(Scanner in) { int n = in.nextInt(); int m = in.nextInt(); if(n == 0 && m == 0) return null; int [] rule = new int [m]; int [] mask = new int [m]; char[] fval = new char[m]; for(int i = 0; i < m; i++) { String s = in.next(); rule[i] = 0; mask[i] = 0; for(int j = 0; j < n; j++) { rule[i] <<= 1; mask[i] <<= 1; if(s.charAt(j) == '1') { rule[i] |= 1; } if(s.charAt(j) != '-') { mask[i] |= 1; } } fval[i] = in.next().charAt(0); } TestCase testCase = new TestCase(n); for(int i = 0; i < (1 << n); i++) { char v = NOVAL; for(int j = 0; j < m; j++) { if((i & mask[j]) == rule[j]) { if(v == NOVAL || fval[j] != UNDEF) { v = fval[j]; } } } if(v == NOVAL) { v = FALSE; } testCase.func[i] = v; } return testCase; } public void print(PrintStream out) { for(int ptn : output) { int rule = (ptn >> 0) & M; int mask = (ptn >> N) & M; for(int i = n - 1; i >= 0; i--) { int mi = (mask >> i) & 1; int ri = (rule >> i) & 1; out.print(mi == 0 ? "-" : ri); } out.println(); } } // finds all implicants private void step1() { Set[] oldptns = new Set[n + 1]; Set[] newptns = new Set[n + 1]; Set[] tmpptns; for(int i = 0; i <= n; i++) { oldptns[i] = new HashSet(); newptns[i] = new HashSet(); } int mask = (1 << n) - 1; for(int i = 0; i < (1 << n); i++) { if(func[i] != FALSE) { int ptn = i | (mask << N); oldptns[Integer.bitCount(i)].add(ptn); remain.add(ptn); } } for(int i = 0; i < n; i++) { for(int j = 0; j < n - i; j++) { for(int p1 : oldptns[j]) for(int p2 : oldptns[j + 1]) { // masks have exactly i set-bits each, thus xors of // masks always have even number of set-bits if(Integer.bitCount(p1 ^ p2) == 1) { remain.remove(p1); remain.remove(p2); int newptn = (p1 & p2) ^ ((p1 ^ p2) << N); newptns[j].add(newptn); remain.add(newptn); } } } tmpptns = oldptns; oldptns = newptns; newptns = tmpptns; for(int j = 0; j < n - 1; j++) newptns[j].clear(); } } private void step2() { for(int i = 0; i < (1 << n); i++) { if(func[i] != TRUE) continue; for(int ptn : output) { int rule = (ptn >> 0) & M; int mask = (ptn >> N) & M; if((i & mask) == rule) { func[i] = DONE; break; } } if(func[i] != TRUE) continue; int tmp = -1; for(int ptn : remain) { int rule = (ptn >> 0) & M; int mask = (ptn >> N) & M; if((i & mask) == rule) { if(tmp != -1) { tmp = -1; break; } tmp = ptn; } } if(tmp != -1) { remain.remove(tmp); output.add(tmp); func[i] = DONE; } } for(int i = 0; i < (1 << n); i++) { if(func[i] != TRUE) continue; for(int ptn : output) { int rule = (ptn >> 0) & M; int mask = (ptn >> N) & M; if((i & mask) == rule) { func[i] = DONE; break; } } } } private void step2a() { Set remainNew; remainNew = new HashSet(); for(int ptn1 : remain) { boolean needed = true; for(int ptn2 : remain) { if(ptn1 == ptn2) { continue; } int rule1 = (ptn1 >> 0) & M; int mask1 = (ptn1 >> N) & M; int cost1 = Integer.bitCount(mask1); int rule2 = (ptn2 >> 0) & M; int mask2 = (ptn2 >> N) & M; int cost2 = Integer.bitCount(mask2); if(cost1 < cost2) { continue; } if(cost1 == cost2 && ptn1 < ptn2) { continue; } boolean unneeded = true; for(int i = 0; i < (1 << n); i++) { if(func[i] == TRUE && (i & mask1) == rule1 && (i & mask2) != rule2) { unneeded = false; break; } } if(unneeded) { needed = false; break; } } if(needed) remainNew.add(ptn1); } remain = remainNew; } private int[] _ptns; private int[] _rule; private int[] _mask; private int[] _cost; private int[] _vals; private int[] _done; private int[] _temp; private int[] _rslt; private static final int NOT_FOUND = Integer.MAX_VALUE; private int maxCost; private int qmax; private void step3() { List values; values = new ArrayList(); for(int i = 0; i < (1 << n); i++) { if(func[i] == TRUE) { values.add(i); } } if(values.isEmpty()) { return; } _ptns = new int[remain.size()]; _rule = new int[remain.size()]; _mask = new int[remain.size()]; _cost = new int[remain.size()]; _vals = new int[values.size()]; _done = new int[values.size()]; _temp = new int[remain.size()]; _rslt = new int[remain.size()]; { int j; j = 0; for(int x : remain) { _ptns[j] = x; _rule[j] = (x >> 0) & M; _mask[j] = (x >> N) & M; _cost[j] = Integer.bitCount(_mask[j]); j++; } j = 0; for(int x : values) { _vals[j] = x; _done[j] = -1; j++; } } for(int i = 0; i < _ptns.length; i++) { for(int j = i + 1; j < _ptns.length; j++) { if(_cost[i] > _cost[j]) { int w; w = _ptns[i]; _ptns[i] = _ptns[j]; _ptns[j] = w; w = _rule[i]; _rule[i] = _rule[j]; _rule[j] = w; w = _mask[i]; _mask[i] = _mask[j]; _mask[j] = w; w = _cost[i]; _cost[i] = _cost[j]; _cost[j] = w; } } } maxCost = NOT_FOUND; qmax = 0; while(maxCost == NOT_FOUND) { qmax++; step3(0, 0, 0, _vals.length); } for(int i = 0; i < qmax; i++) output.add(_rslt[i]); } private void step3(int p, int q, int cost, int rest) { if(cost >= maxCost) return; if(q == qmax) { if(rest == 0) { System.arraycopy(_temp, 0, _rslt, 0, qmax); maxCost = cost; } return; } for(int i = p; i <= _ptns.length - (qmax - q); i++) { int newCost = cost + _cost[i]; int newRest = rest; for(int j = 0; j < _vals.length; j++) { if(_done[j] >= 0) { continue; } if((_vals[j] & _mask[i]) != _rule[i]) { continue; } _done[j] = i; newRest--; } if(newRest == rest) { continue; } _temp[q] = _ptns[i]; step3(i + 1, q + 1, newCost, newRest); for(int j = 0; j < _vals.length; j++) { if(_done[j] == i) { _done[j] = -1; } } } } public void solve() { step1(); step2(); step2a(); step3(); } } }