fiveworlds Posted January 8, 2022 Share Posted January 8, 2022 (For anyone interested) I finally got around to finishing the 3-Sat Algorithm (there may be a few typos) package com.company; import java.math.BigInteger; import java.util.Arrays; import java.util.HashMap; public class kSatMap { private static final int k = 3; private static final double permutations = Math.pow(2, k); private static final HashMap<String, String[]> lookupTable; static { lookupTable = new HashMap<>(); //position 0 value assignments (Single Letter Clauses) lookupTable.put("0", new String[]{"00001111"}); // A lookupTable.put("1", new String[]{"11110000"}); // !A //position 0 value assignments (Double Letter Clauses) lookupTable.put("00", new String[]{"00111111"}); // AB lookupTable.put("01", new String[]{"11001111"}); // A!B lookupTable.put("10", new String[]{"11110011"}); // !AB lookupTable.put("11", new String[]{"11111100"}); // !A!B //position 0 value assignments (Treble Letter Clauses) lookupTable.put("000", new String[]{"01111111"}); // ABC lookupTable.put("001", new String[]{"10111111"}); // AB!C lookupTable.put("010", new String[]{"11011111"}); // A!BC lookupTable.put("011", new String[]{"11101111"}); // A!B!B lookupTable.put("100", new String[]{"11110111"}); // !ABC lookupTable.put("101", new String[]{"11111011"}); // !AB!C lookupTable.put("110", new String[]{"11111101"}); // !A!BC lookupTable.put("111", new String[]{"11111110"}); // !A!B!C // Conversions for moving parts. (Single Letter Assignments) lookupTable.put("100000000", new String[]{"00000000", "00000000", "00000000","A","00000000"}); lookupTable.put("100001111", new String[]{"00001111", "00110011", "01010101","A","00001111"}); // A -> C -> E -> assignment lookup lookupTable.put("101010101", new String[]{"00001111", "00110011", "01010101","B","00001111"}); // A -> C -> E -> assignment lookup lookupTable.put("100110011", new String[]{"00001111", "00110011", "01010101","C","00001111"}); // A -> C -> E -> assignment lookup lookupTable.put("111110000", new String[]{"11110000", "11001100", "10101010","A","11110000"}); // B -> D -> F -> assignment lookup lookupTable.put("111001100", new String[]{"11110000", "11001100", "10101010","B","11110000"}); // B -> D -> F -> assignment lookup lookupTable.put("110101010", new String[]{"11110000", "11001100", "10101010","C","11110000"}); // B -> D -> F -> assignment lookup // Conversions for moving parts. (Double Letter Assignments) lookupTable.put("200000000", new String[]{"00000000", "00000000", "00000000","A:B:A,B","00000000","00000000","00000000"}); lookupTable.put("200111111", new String[]{"00111111", "01011111", "01110111", "A,B", "00111111"}); // AC -> AE -> CE -> assignment lookup lookupTable.put("211001111", new String[]{"11001111", "10101111", "10111011", "A,B", "11001111"}); // AD -> AF -> CF -> assignment lookup lookupTable.put("211110011", new String[]{"11110011", "11110101", "11011101", "A,B", "11110011"}); // BC -> BE -> DE -> assignment lookup lookupTable.put("211111100", new String[]{"11111100", "11111010", "11101110", "A,B", "11111100"}); // BD -> BF -> DF -> assignment lookup lookupTable.put("200001111", new String[]{"00001111", "00001111", "00110011","A:A,B","00001111","00001111"}); // AC + AD -> AE + AF -> CE + CF -> assignment lookup lookupTable.put("200000011", new String[]{"00000011", "00000101", "00010001","A:B:A,B","00001111","00001111","00000011"}); // AC + AD + BC -> AE + AF + BE -> CE + CF + DE -> assignment lookup lookupTable.put("200001100", new String[]{"00001100", "00001010", "00100010","A:B:A,B","00001111","11110000","00001100"}); // AC + AD + BD -> AE + AF -> CE + CF -> assignment lookup lookupTable.put("200110000", new String[]{"00110000", "01010000", "01000100","A:B:A,B","11110000", "00001111","00110000"}); // AC + AD -> AE + AF -> CE + CF -> assignment lookup lookupTable.put("200110011", new String[]{"00110011", "10101010", "01100101","B:A,B", "00001111", "00110011"}); // AC + AD -> AE + AF -> CE + CF -> assignment lookup lookupTable.put("200111100", new String[]{"00111100", "00110011", "01100110","A,B","00111100"}); // AC + AD -> AE + AF -> CE + CF -> assignment lookup lookupTable.put("211000011", new String[]{"11000011", "10100101", "01010101","A,B", "11000011"}); // AC + AD -> AE + AF -> CE + CF -> assignment lookup lookupTable.put("211001100", new String[]{"11001100", "10101010", "10101010","B:A,B","00001111", "11001100"}); // AC + AD -> AE + AF -> CE + CF -> assignment lookup lookupTable.put("211110000", new String[]{"11110000", "11110000", "11001100","A:A,B","11110000","11110000"}); // AC + AD -> AE + AF -> CE + CF -> assignment lookup lookupTable.put("211000000", new String[]{"11000000", "10100000", "10001000","A:A,B","11110000","11000000"}); // AC + AD -> AE + AF -> CE + CF -> assignment lookup // Conversions for moving parts. (Triple Letter Assignments) lookupTable.put("301111111", new String[]{"01111111", "01111111", "01111111", "A,B,C", "01111111"}); // ACE lookupTable.put("300111111", new String[]{"00111111", "00111111", "00111111", "A,B,C:A,B", "00111111", "00111111"}); // ACE + ACF lookupTable.put("300011111", new String[]{"00011111", "00011111", "00011111", "A,B,C:A,B:A,C", "00011111", "00111111", "00111111"}); // ACE + ACF + ADE lookupTable.put("300001111", new String[]{"00001111", "00001111", "00001111", "A,B,C:A:A,B:A,C", "00001111", "00001111", "00001111", "00001111"}); // ACE + ACF + ADE + ADF lookupTable.put("300000111", new String[]{"00000111", "00000111", "00000111", "A,B,C:A:A,B:A,C", "00000111", "00001111", "00001111", "00001111"}); // ACE + ACF + ADE + ADF + BCE lookupTable.put("300000011", new String[]{"00000011", "00000011", "00000011", "A,B,C:A:B:A,B:A,C", "00000011","00001111","00001111","00000011", "00001111"}); // ACE + ACF + ADE + ADF + BCE + BCF lookupTable.put("300000001", new String[]{"00000001", "00000001", "00000001", "A,B,C:A:B:A:B:C:A,B:A,C", "00000001","00000011","00001111","00001111","00000011","00001111","00000011", "00001111"}); // ACE + ACF + ADE + ADF + BCE + BCF + BDE lookupTable.put("300000000", new String[]{"00000000", "00000000", "00000000", "A,B,C:A:B:C:A,B:B,C:A,C", "00000000","00000000","00000000","00000000","00000000","00000000","00000000","00000000"}); // ACE + ACF + ADE + ADF + BCE + BCF + BDE + BDF lookupTable.put("301011111", new String[]{"01011111", "01011111", "01011111", "A,B,C:A,C", "01011111","00111111"}); // ACE + ADE lookupTable.put("301010111", new String[]{"01010111", "01010111", "01010111", "A,B,C:A,C", "01010111","00111111"}); // ACE + ADE + BCE lookupTable.put("301010100", new String[]{"01010100", "01010100", "01010100", "A,B,C:A,C:C:A,B", "01010100","00111111","00001111","11111100"}); // ACE + ADE + BCE lookupTable.put("301010101", new String[]{"00001111", "00110011", "01010101","A,B,C:B,C:C:A,C:C", "01010101","00001111","00001111","00111111","00001111"}); // ACE + ADE + BCE lookupTable.put("301010110", new String[]{"01010110", "01010110", "01010110", "A,B,C:A,C", "01000111","00111111"}); // ACE + ADE + BCE lookupTable.put("301010011", new String[]{"01000011", "01000011", "01000011", "A,B,C:A,C:A,B", "01000011","00111111","11110011"}); // ACE + ADE + BCE + BCF lookupTable.put("301010010", new String[]{"01000011", "01000011", "01000011", "A,B,C:A,C:A,B", "01000011","00111100","11110011"}); // ACE + ADE + BCE + BCF lookupTable.put("301010001", new String[]{"01000001", "01000001", "01000001", "A,B,C:A,C:C:A,B", "01000001","00111111","00001111","11110011"}); // ACE + ADE + BCE + BCF + BDE lookupTable.put("301010000", new String[]{"01000000", "01000000", "01000000", "A,B,C:A,C:A:C:A,B:A", "01000000","00111100","11110000","00001111","11110000","11110000"}); // ACE + ADE + BCE + BCF + BDE + BDF lookupTable.put("301001111", new String[]{"01001111", "01001111", "01001111", "A,B,C:A,C:A,B", "01001111","00111111","11001111"}); // ACE + ADE + ADF lookupTable.put("301000111", new String[]{"01000111", "01000111", "01000111", "A,B,C:A,C:A,B", "01000111","00111111","11001111"}); // ACE + ADE + ADF + BCE lookupTable.put("301000011", new String[]{"01000011", "01000011", "01000011", "A,B,C:A,C:A,B", "01000011","00111111","11000011"}); // ACE + ADE + ADF + BCE + BCF lookupTable.put("301000001", new String[]{"01000001", "01000001", "01000001", "A,B,C:A,C:A,B:C", "01000001","00111111","11000011","00001111"}); // ACE + ADE + ADF + BCE + BCF + BDE lookupTable.put("301000000", new String[]{"01000000", "01000000", "01000000", "A,B,C:A,C:A,B:A:B:C", "01000000","00111100","11000000","11110000","11110000","00001111"}); // ACE + ADE + ADF + BCE + BCF + BDE + BDF lookupTable.put("301101111", new String[]{"01101111", "01101111", "01101111", "A,B,C", "01101111"}); // ACE + ADF lookupTable.put("301100111", new String[]{"01100111", "01100111", "01100111", "A,B,C", "01100111"}); // ACE + ADF + BCE lookupTable.put("301100011", new String[]{"01100011", "01100011", "01100011", "A,B,C:A,B", "01100011","11110011"}); // ACE + ADF + BCE + BCF lookupTable.put("301100001", new String[]{"01100001", "01100001", "01100001", "A,B,C:A,B", "01100001","11110011"}); // ACE + ADF + BCE + BCF + BDE lookupTable.put("301100000", new String[]{"01100000", "01100000", "01100000", "A,B,C:A:A,B:A,C:C", "01100000","11110000","11110000","11111100","11110000"}); // ACE + ADF + BCE + BCF + BDE + BDF lookupTable.put("310111111", new String[]{"10111111", "10111111", "10111111", "A,B,C", "10111111"}); // AD -> AF -> CF -> assignment lookup lookupTable.put("311011111", new String[]{"11011111", "11011111", "11011111", "A,B,C", "11011111"}); // BC -> BE -> DE -> assignment lookup lookupTable.put("311101111", new String[]{"11101111", "11101111", "11101111", "A,B,C", "11101111"}); // BD -> BF -> DF -> assignment lookup lookupTable.put("311110111", new String[]{"11110111", "11110111", "11110111", "A,B,C", "11110111"}); // AC -> AE -> CE -> assignment lookup lookupTable.put("311111011", new String[]{"11111011", "11111011", "11111011", "A,B,C", "11111011"}); // AD -> AF -> CF -> assignment lookup lookupTable.put("311111101", new String[]{"11111101", "11111101", "11111101", "A,B,C", "11111101"}); // BC -> BE -> DE -> assignment lookup lookupTable.put("311111110", new String[]{"11111110", "11111110", "11111110", "A,B,C", "11111110"}); // BD -> BF -> DF -> assignment lookup lookupTable.put("311111100", new String[]{"11111100", "11111100", "11111100", "A,B,C:A,B", "11111100","11111100"}); lookupTable.put("311111010", new String[]{"11111010", "11111010", "11111010", "A,B,C:A,C", "11111010", "11111100"}); lookupTable.put("311111001", new String[]{"11111001", "11111001", "11111001", "A,B,C", "11111001"}); lookupTable.put("311111000", new String[]{"11111000", "11111000", "11111000", "A,B,C:A,B:A,C", "11111000","11111100","11111100"}); lookupTable.put("311110110", new String[]{"11110110", "11110110", "11110110", "A,B,C", "11110110"}); lookupTable.put("311110101", new String[]{"11110101", "11110101", "11110101", "A,B,C:A,C", "11110101","11110011"}); lookupTable.put("311110100", new String[]{"11110100", "11110100", "11110100", "A,B,C:A,B", "11110100","11111100"}); lookupTable.put("311110011", new String[]{"11110011", "11110011", "11110011", "A,B,C:A,B", "11110011", "11110011"}); lookupTable.put("311110010", new String[]{"11110010", "11110010", "11110010", "A,B,C:A,B:A,C", "11110010", "11110011","11111100"}); lookupTable.put("311110001", new String[]{"11110001", "11110001", "11110001", "A,B,C:A,B", "11110001", "11110011"}); lookupTable.put("311110000", new String[]{"11110000", "11110000", "11110000", "A,B,C:A:A,B:A,C:C", "11110000","11110000","11110000","11111100","11110000"}); lookupTable.put("311101110", new String[]{"11101110", "11101110", "11101110", "A,B,C:B,C:B", "11101110", "11111100","11110000"}); lookupTable.put("311101101", new String[]{"11101101", "11101101", "11101101", "A,B,C:B", "11101101","11110000"}); lookupTable.put("311101100", new String[]{"11101100", "11101100", "11101100", "A,B,C:B:A,B", "11101100","11110000","11111100"}); lookupTable.put("311101011", new String[]{"11101011", "11101011", "11101011", "A,B,C", "11101011"}); lookupTable.put("311101010", new String[]{"11101010", "11101010", "11101010", "A,B,C:A,C", "11101010","11111100"}); lookupTable.put("311101001", new String[]{"11101001", "11101001", "11101001", "A,B,C", "11101001"}); lookupTable.put("311101000", new String[]{"11101000", "11101000", "11101000", "A,B,C:A,B:A,C", "11101000","11111100","11111100"}); lookupTable.put("311100111", new String[]{"11100111", "11100111", "11100111", "A,B,C", "11100111"}); lookupTable.put("311100110", new String[]{"11100110", "11100110", "11100110", "A,B,C", "11100110"}); lookupTable.put("311100101", new String[]{"11100101", "11100101", "11100101", "A,B,C:A,C", "11100101","11110011"}); lookupTable.put("311100100", new String[]{"11100100", "11100100", "11100100", "A,B,C:A,B:A,C", "11100100","11111100","11110011"}); lookupTable.put("311100011", new String[]{"11100011", "11100011", "11100011", "A,B,C:A,B", "11100011","11110011"}); lookupTable.put("311100010", new String[]{"11100010", "11100010", "11100010", "A,B,C:A,B:A,C", "11100010","11110011","11111100"}); lookupTable.put("311100001", new String[]{"11100001", "11100001", "11100001", "A,B,C:A,B", "11100001","11110011"}); lookupTable.put("311100000", new String[]{"11100000", "11100000", "11100000", "A,B,C:A:A,B:A,C:C", "11100000","11110000","11111100","11111100","11110000"}); lookupTable.put("311011110", new String[]{"11011110", "11011110", "11011110", "A,B,C", "11011110"}); lookupTable.put("311011101", new String[]{"11011101", "11011101", "11011101", "A,B,C:B,C", "11011101", "11110011"}); lookupTable.put("311011100", new String[]{"11011100", "11011100", "11011100", "A,B,C:A,B", "11011100","11111100"}); lookupTable.put("311011011", new String[]{"11011011", "11011011", "11011011", "A,B,C", "11011011"}); lookupTable.put("311011010", new String[]{"11011010", "11011010", "11011010", "A,B,C:A,C", "11011010","11111100"}); lookupTable.put("311011001", new String[]{"11011001", "11011001", "11011001", "A,B,C", "11011001"}); lookupTable.put("311011000", new String[]{"11011000", "11011000", "11011000", "A,B,C:A,B:A,C", "11011000","11111100","11111100"}); lookupTable.put("311010111", new String[]{"11010111", "11010111", "11010111", "A,B,C", "11010111"}); lookupTable.put("311010110", new String[]{"11010110", "11010110", "11010110", "A,B,C", "11010110"}); lookupTable.put("311010101", new String[]{"11010101", "11010101", "11010101", "A,B,C", "11010101"}); lookupTable.put("311010100", new String[]{"11010100", "11010100", "11010100", "A,B,C:A,B", "11010100","11111100"}); lookupTable.put("311010011", new String[]{"11010011", "11010011", "11010011", "A,B,C:A,B", "11010011","11110011"}); lookupTable.put("311010010", new String[]{"11010010", "11010010", "11010010", "A,B,C:A,C:A,B", "11010010","11111100","11110011"}); lookupTable.put("311010001", new String[]{"11010001", "11010001", "11010001", "A,B,C:A,B", "11010001","11110011"}); lookupTable.put("311010000", new String[]{"11010000", "11010000", "11010000", "A,B,C:A:A,B:A,C:C", "11010000","11110000","11110000","11111100","11110000"}); lookupTable.put("311001111", new String[]{"11001111", "11001111", "11001111", "A,B,C:A,B:B", "11001111","11001111"}); lookupTable.put("311001110", new String[]{"11001110", "11001110", "11001110", "A,B,C:A,B:B", "11001110","11001111"}); lookupTable.put("311001101", new String[]{"11001101", "11001101", "11001101", "A,B,C:A,B:B", "11001101","11001111"}); lookupTable.put("311001100", new String[]{"11001100", "11001100", "11001100", "A,B,C:B:A,B:B", "11001100","00001111","11001100","11110000"}); lookupTable.put("311001011", new String[]{"11001011", "11001011", "11001011", "A,B,C:A,B", "11001011","11001111"}); lookupTable.put("311001010", new String[]{"11001010", "11001010", "11001010", "A,B,C:A,B:A,C", "11001010","11001111","11111100"}); lookupTable.put("311001001", new String[]{"11001001", "11001001", "11001001", "A,B,C:A,B", "11001001","11001111"}); lookupTable.put("311001000", new String[]{"11001000", "11001000", "11001000", "A,B,C:A,B:B:A,C", "11001000","11001100","11110000","11111100"}); lookupTable.put("311000111", new String[]{"11000111", "11000111", "11000111", "A,B,C:A,B", "11000111","11001111"}); lookupTable.put("311000110", new String[]{"11000110", "11000110", "11000110", "A,B,C:A,B", "11000110","11001111"}); lookupTable.put("311000101", new String[]{"11000101", "11000101", "11000101", "A,B,C:A,B:A,C", "11000101","11001111","11110011"}); lookupTable.put("311000100", new String[]{"11000100", "11000100", "11000100", "A,B,C:A,B:B:A,C", "11000100","11001100","11110000","11110011"}); lookupTable.put("311000011", new String[]{"11000011", "11000011", "11000011", "A,B,C:A,B", "11000011","11000011"}); lookupTable.put("311000010", new String[]{"11000010", "11000010", "11000010", "A,B,C:A,B:A,C", "11000010","11000011","11111100"}); lookupTable.put("311000001", new String[]{"11000001", "11000001", "11000001", "A,B,C:A,B:A,C", "11000001","11000011","11110011"}); lookupTable.put("311000000", new String[]{"11000000", "11000000", "11000000", "A,B,C:A:A,B:B:A,C:C:B", "11000000","11110000","11000000","11110000","11111100","11110000","11110000"}); lookupTable.put("310111110", new String[]{"10111110", "10111110", "10111110", "A,B,C", "10111110"}); lookupTable.put("310111101", new String[]{"10111101", "10111101", "10111101", "A,B,C", "10111101"}); lookupTable.put("310111100", new String[]{"10111100", "10111100", "10111100", "A,B,C:A,B", "10111100","11111100"}); lookupTable.put("310111011", new String[]{"10111011", "10111011", "10111011", "A,B,C:B,C", "10111011", "11001111"}); lookupTable.put("310111010", new String[]{"10111010", "10111010", "10111010", "A,B,C:A,C", "10111010","11111100"}); lookupTable.put("310111001", new String[]{"10111001", "10111001", "10111001", "A,B,C", "10111001"}); lookupTable.put("310111000", new String[]{"10111000", "10111000", "10111000", "A,B,C:A,B:A,C", "10111000","11111100","11111100"}); lookupTable.put("310110111", new String[]{"10110111", "10110111", "10110111", "A,B,C", "10110111"}); lookupTable.put("310110110", new String[]{"10110110", "10110110", "10110110", "A,B,C", "10110110"}); lookupTable.put("310110101", new String[]{"10110101", "10110101", "10110101", "A,B,C:A,C", "10110101","11110011"}); lookupTable.put("310110100", new String[]{"10110100", "10110100", "10110100", "A,B,C:A,B", "10110100","11111100"}); lookupTable.put("310110011", new String[]{"10110011", "10110011", "10110011", "A,B,C:A,B", "10110011","11110011"}); lookupTable.put("310110010", new String[]{"10110010", "10110010", "10110010", "A,B,C:A,C:A,B", "10110010","11111100","11110011"}); lookupTable.put("310110001", new String[]{"10110001", "10110001", "10110001", "A,B,C:A,B:A,C", "10110001","11110011","11110011"}); lookupTable.put("310110000", new String[]{"10110000", "10110000", "10110000", "A,B,C:A:A,B:A,C:C", "10110000","11110000","11110000","11111100","11110000"}); lookupTable.put("310101111", new String[]{"10101111", "10101111", "10101111", "A,B,C:A,C", "10101111", "11001111"}); lookupTable.put("310101110", new String[]{"10101110", "10101110", "10101110", "A,B,C:A,C", "10101110", "11001111"}); lookupTable.put("310101101", new String[]{"10101101", "10101101", "10101101", "A,B,C:A,C", "10101101", "11001111"}); lookupTable.put("310101100", new String[]{"10101100", "10101100", "10101100", "A,B,C:A,B:A,C", "10101100","11111100", "11001111"}); lookupTable.put("310101011", new String[]{"10101011", "10101011", "10101011", "A,B,C:A.C", "10101011", "11001111"}); lookupTable.put("310101010", new String[]{"10101010", "10101010", "10101010", "A,B,C:C:A,C", "10101010", "11110000", "11000000"}); lookupTable.put("310101001", new String[]{"10101001", "10101001", "10101001", "A,B,C:A,C", "10101001", "11001111"}); lookupTable.put("310101000", new String[]{"10101000", "10101000", "10101000", "A,B,C:C:A,B:A,C", "10101000","11110000","11111100", "11001100"}); lookupTable.put("310100111", new String[]{"10100111", "10100111", "10100111", "A,B,C:A,C", "10100111", "11001111"}); lookupTable.put("310100110", new String[]{"10100110", "10100110", "10100110", "A,B,C:A,C", "10100110", "11001111"}); lookupTable.put("310100101", new String[]{"10100101", "10100101", "10100101", "A,B,C:A,C", "10100101", "11000011"}); lookupTable.put("310100100", new String[]{"10100100", "10100100", "10100100", "A,B,C:A,B:A,C", "10100100","11111100", "11000011"}); lookupTable.put("310100011", new String[]{"10100011", "10100011", "10100011", "A,B,C:A,C:A,B", "10100011", "11000011","11110011"}); lookupTable.put("310100010", new String[]{"10100010", "10100010", "10100010", "A,B,C:C:A,C:A,B", "10100010","11110000", "11001100","11110011"}); lookupTable.put("310100001", new String[]{"10100001", "10100001", "10100001", "A,B,C:A,C:A,B", "10100001", "11000011","11110011"}); lookupTable.put("310100000", new String[]{"10100000", "10100000", "10100000", "A,B,C:A:C:A,B", "10100000","11110000","11110000","11110000"}); lookupTable.put("310011111", new String[]{"10011111", "10011111", "10011111", "A,B,C", "10011111"}); lookupTable.put("310011110", new String[]{"10011110", "10011110", "10011110", "A,B,C", "10011110"}); lookupTable.put("310011101", new String[]{"10011101", "10011101", "10011101", "A,B,C", "10011101"}); lookupTable.put("310011100", new String[]{"10011100", "10011100", "10011100", "A,B,C:A,B", "10011100","11111100"}); lookupTable.put("310011011", new String[]{"10011011", "10011011", "10011011", "A,B,C", "10011011"}); lookupTable.put("310011010", new String[]{"10011010", "10011010", "10011010", "A,B,C:A,C", "10011010","11111100"}); lookupTable.put("310011001", new String[]{"10011001", "10011001", "10011001", "A,B,C", "10011001"}); lookupTable.put("310011000", new String[]{"10011000", "10011000", "10011000", "A,B,C:A,B:A,C", "10011000","11111100","11111100"}); lookupTable.put("310010111", new String[]{"10010111", "10010111", "10010111", "A,B,C", "10010111"}); lookupTable.put("310010110", new String[]{"10010110", "10010110", "10010110", "A,B,C", "10010110"}); lookupTable.put("310010101", new String[]{"10010101", "10010101", "10010101", "A,B,C:A,C", "10010101","11110011"}); lookupTable.put("310010100", new String[]{"10010100", "10010100", "10010100", "A,B,C:A,B:A,C", "10010100","11111100","11110011"}); lookupTable.put("310010011", new String[]{"10010011", "10010011", "10010011", "A,B,C:A,B", "10010011","11110011"}); lookupTable.put("310010010", new String[]{"10010010", "10010010", "10010010", "A,B,C:A,C:A,B", "10010010","11111100","11110011"}); lookupTable.put("310010001", new String[]{"10010001", "10010001", "10010001", "A,B,C:A,B:A,C", "10010001","11110011","11110011"}); lookupTable.put("310010000", new String[]{"10010000", "10010000", "10010000", "A,B,C:A:A,B:A,C:C", "10010000","11110000","11110000","11110000","11110000"}); lookupTable.put("310001111", new String[]{"10001111", "10001111", "10001111", "A,B,C:A,B:A,C", "10001111","11001111", "11001111"}); lookupTable.put("310001110", new String[]{"10001110", "10001110", "10001110", "A,B,C:A,B:A,C", "10001110","11001111", "11001111"}); lookupTable.put("310001101", new String[]{"10001101", "10001101", "10001101", "A,B,C:A,B:A,C", "10001101","11001111", "11001111"}); lookupTable.put("310001100", new String[]{"10001100", "10001100", "10001100", "A,B,C:A,B:B:A,C", "10001100","11001100","11110000", "11001111"}); lookupTable.put("310001011", new String[]{"10001011", "10001011", "10001011", "A,B,C:A,B:A,C", "10001011","11001111", "11001111"}); lookupTable.put("310001010", new String[]{"10001010", "10001010", "10001010", "A,B,C:A,B:C:A,C", "10001010","11001111","11110000", "11001100"}); lookupTable.put("310001001", new String[]{"10001001", "10001001", "10001001", "A,B,C:A,B:A,C", "10001001","11001111", "11001111"}); lookupTable.put("310001000", new String[]{"10001000", "10001000", "10001000", "A,B,C:A,B:B:C:A,C", "10001000","11001100","11110000","11110000", "11001100"}); lookupTable.put("310000111", new String[]{"10000111", "10000111", "10000111", "A,B,C:A,B:A,C", "10000111","11001111", "11001111"}); lookupTable.put("310000110", new String[]{"10000110", "10000110", "10000110", "A,B,C:A,B:A,C", "10000110","11001111", "11001111"}); lookupTable.put("310000101", new String[]{"10000101", "10000101", "10000101", "A,B,C:A,B:A,C", "10000101","11001111", "11000011"}); lookupTable.put("310000100", new String[]{"10000100", "10000100", "10000100", "A,B,C:A,B:B:A,C", "10000100","11001100","11110000", "11000011"}); lookupTable.put("310000011", new String[]{"10000011", "10000011", "10000011", "A,B,C:A,B:A,C", "10000011","11000011", "11001111"}); lookupTable.put("310000010", new String[]{"10000010", "10000010", "10000010", "A,B,C:A,B:C:A,C", "10000010","11000011","11110000", "11001100"}); lookupTable.put("310000001", new String[]{"10000001", "10000001", "10000001", "A,B,C:A,B:A,C", "10000001","11000011", "11000011"}); lookupTable.put("310000000", new String[]{"10000000", "10000000", "10000000", "A,B,C:A,B:A:B:C:A,C", "10000000","11000000","11110000","11110000","11110000", "11000000"}); lookupTable.put("301111110", new String[]{"01111110", "01111110", "01111110", "A,B,C", "01111110"}); lookupTable.put("301111101", new String[]{"01111101", "01111101", "01111101", "A,B,C", "01111101"}); lookupTable.put("301111100", new String[]{"01111100", "01111100", "01111100", "A,B,C:A,B", "01111100","11111100"}); lookupTable.put("301111011", new String[]{"01111011", "01111011", "01111011", "A,B,C", "01111011"}); lookupTable.put("301111010", new String[]{"01111010", "01111010", "01111010", "A,B,C:A,C", "01111010","11111100"}); lookupTable.put("301111001", new String[]{"01111001", "01111001", "01111001", "A,B,C", "01111001"}); lookupTable.put("301111000", new String[]{"01111000", "01111000", "01111000", "A,B,C:A,B:A,C", "01111000","11111100","11111100"}); lookupTable.put("301110111", new String[]{"01110111", "01110111", "01110111", "A,B,C:B,C", "01110111", "00111111"}); lookupTable.put("301110110", new String[]{"01110110", "01110110", "01110110", "A,B,C", "01110110"}); lookupTable.put("301110101", new String[]{"01110101", "01110101", "01110101", "A,B,C:A,C", "01110101","11110011"}); lookupTable.put("301110100", new String[]{"01110100", "01110100", "01110100", "A,B,C:A,B:A,C", "01110100","11111100","11110011"}); lookupTable.put("301110011", new String[]{"01110011", "01110011", "01110011", "A,B,C:A,B", "01110011","11110011"}); lookupTable.put("301110010", new String[]{"01110010", "01110010", "01110010", "A,B,C:A,C:A,B", "01110010","11111100","11110011"}); lookupTable.put("301110001", new String[]{"01110001", "01110001", "01110001", "A,B,C:A,B:A,C", "01110001","11110011","11110011"}); lookupTable.put("301110000", new String[]{"01110000", "01110000", "01110000", "A,B,C:A:A,B:A,C:C", "01110000","11110000","11110000","11110000","11110000"}); lookupTable.put("301101110", new String[]{"01101110", "01101110", "01101110", "A,B,C", "01101110"}); lookupTable.put("301101101", new String[]{"01101101", "01101101", "01101101", "A,B,C", "01101101"}); lookupTable.put("301101100", new String[]{"01101100", "01101100", "01101100", "A,B,C:A,B", "01101100","11111100"}); lookupTable.put("301101011", new String[]{"01101011", "01101011", "01101011", "A,B,C", "01101011"}); lookupTable.put("301101010", new String[]{"01101010", "01101010", "01101010", "A,B,C:A,C", "01101010","11111100"}); lookupTable.put("301101001", new String[]{"01101001", "01101001", "01101001", "A,B,C", "01101001"}); lookupTable.put("301101000", new String[]{"01101000", "01101000", "01101000", "A,B,C:A,B:A,C", "01101000","11111100","11111100"}); lookupTable.put("301100110", new String[]{"01100110", "01100110", "01100110", "A,B,C", "01100110"}); lookupTable.put("301100101", new String[]{"01100101", "01100101", "01100101", "A,B,C:A,C", "01100101","11110011"}); lookupTable.put("301100100", new String[]{"01100100", "01100100", "01100100", "A,B,C:A,B:A,C", "01100100","11111100","11110011"}); lookupTable.put("301100010", new String[]{"01100010", "01100010", "01100010", "A,B,C:A,C:A.B", "01100010","11111100","11110011"}); lookupTable.put("301011110", new String[]{"01011110", "01011110", "01011110", "A,B,C:A,C", "01011110","00111111"}); lookupTable.put("301011101", new String[]{"01011101", "01011101", "01011101", "A,B,C:A,C", "01011101","00111111"}); lookupTable.put("301011100", new String[]{"01011100", "01011100", "01011100", "A,B,C:A,C:A,B", "01011100","00111111","11111100"}); lookupTable.put("301011011", new String[]{"01011011", "01011011", "01011011", "A,B,C:A,C", "01011011","00111111"}); lookupTable.put("301011010", new String[]{"01011010", "01011010", "01011010", "A,B,C:A,C", "01011010","00111100"}); lookupTable.put("301011001", new String[]{"01011001", "01011001", "01011001", "A,B,C:A,C", "01011001","00111111"}); lookupTable.put("301011000", new String[]{"01011000", "01011000", "01011000", "A,B,C:A,C:A,B", "01011000","00111100","11111100"}); lookupTable.put("301001110", new String[]{"01001110", "01001110", "01001110", "A,B,C:A,C:A,B", "01001110","00111111","11001111"}); lookupTable.put("301001101", new String[]{"01001101", "01001101", "01001101", "A,B,C:A,C:A,B", "01001101","00111111","11001111"}); lookupTable.put("301001100", new String[]{"01001100", "01001100", "01001100", "A,B,C:A,C:A,B:B", "01001100","00111111","11001100","11110000"}); lookupTable.put("301001011", new String[]{"01001011", "01001011", "01001011", "A,B,C:A,C:A,B", "01001011","00111111","11001111"}); lookupTable.put("301001010", new String[]{"01001010", "01001010", "01001010", "A,B,C:A,C:A,B", "01001010","00111100","11001111"}); lookupTable.put("301001001", new String[]{"01001001", "01001001", "01001001", "A,B,C:A,C:A,B", "01001001","00111111","11001111"}); lookupTable.put("301001000", new String[]{"01001000", "01001000", "01001000", "A,B,C:A,C:A,B:B", "01001000","00111100","11001100","11110000"}); lookupTable.put("301000110", new String[]{"01000110", "01000110", "01000110", "A,B,C:A,C:A,B:B,C", "01000110","00111111","00111111","00111111"}); lookupTable.put("301000101", new String[]{"01000101", "01000101", "01000101", "A,B,C:A,C:A,B:B,C:C", "01000101","00110011","00111111","00111111","00001111"}); lookupTable.put("301000100", new String[]{"01000100", "01000100", "01000100", "A,B,C:A,C:A,B:B,C:B:C", "01000100","00110011","00111100","00111111","11110000","00001111"}); lookupTable.put("301000010", new String[]{"01000010", "01000010", "01000010", "A,B,C:A,C:A,B:B,C", "0100001","00111100","00111111"}); lookupTable.put("300111110", new String[]{"00111110", "00111110", "00111110", "A,B,C:A,B", "00111110","00111111"}); lookupTable.put("300111101", new String[]{"00111101", "00111101", "00111101", "A,B,C:A,B", "00111101","00111111"}); lookupTable.put("300111100", new String[]{"00111100", "00111100", "00111100", "A,B,C:A,B", "00111100","00111100"}); lookupTable.put("300111011", new String[]{"00111011", "00111011", "00111011", "A,B,C:A,B", "00111011","00111100"}); lookupTable.put("300111010", new String[]{"00111010", "00111010", "00111010", "A,B,C:A,C", "00111010","11111100"}); lookupTable.put("300111001", new String[]{"00111001", "00111001", "00111001", "A,B,C:A,B", "00111001","00111111"}); lookupTable.put("300111000", new String[]{"00111000", "00111000", "00111000", "A,B,C:A,B:A,C", "00111000","00111100","11111100"}); lookupTable.put("300110111", new String[]{"00110111", "00110111", "00110111", "A,B,C:B,C", "00110111","00111111"}); lookupTable.put("300110110", new String[]{"00110110", "00110110", "00110110", "A,B,C:B,C", "00110110","00111111"}); lookupTable.put("300110101", new String[]{"00110101", "00110101", "00110101", "A,B,C:B,C:A,C", "00110101","00111111","11110011"}); lookupTable.put("300110100", new String[]{"00110100", "00110100", "00110100", "A,B,C:B,C:A,B:A,C", "00110100","00111111","00111100","00111100","11110011"}); lookupTable.put("300110011", new String[]{"00110011", "00110011", "00110011", "A,B,C:B:A,B", "00110011", "00001111", "00110011","00110011"}); lookupTable.put("300110010", new String[]{"00110010", "00110010", "00110010", "A,B,C:B:B,C:A,C:A,B", "00110010", "00001111","00111111","11111100","00110011"}); lookupTable.put("300110001", new String[]{"00110001", "00110001", "00110001", "A,B,C:B:B,C:A,B:A,C", "00110001", "00001111","00111111","00110011","11110011"}); lookupTable.put("300110000", new String[]{"00110000", "00110000", "00110000", "A,B,C:A,C:A:B:A,B:B,C:A:A,B:C", "00110000","11110000","11110000", "00001111","00110000","00111111","11110000","00111100","11110000"}); lookupTable.put("300101111", new String[]{"00101111", "00101111", "00101111", "A,B,C:A,C:A,B", "00101111","11001111","00111111"}); lookupTable.put("300101110", new String[]{"00101110", "00101110", "00101110", "A,B,C:A,C:A,B", "00101110","11001111","00111111"}); lookupTable.put("300101101", new String[]{"00101101", "00101101", "00101101", "A,B,C:A,C:A,B", "00101101","11001111","00111111"}); lookupTable.put("300101100", new String[]{"00101100", "00101100", "00101100", "A,B,C:A,B:A,C", "00101100","00111100","11001111"}); lookupTable.put("300101011", new String[]{"00101011", "00101011", "00101011", "A,B,C:A,C:A,B", "00101011","11001111","00111111"}); lookupTable.put("300101010", new String[]{"00101010", "00101010", "00101010", "A,B,C:C:A,C:A,B", "00101010","11110000","11001100","00111111"}); lookupTable.put("300101001", new String[]{"00101001", "00101001", "00101001", "A,B,C:A,C:A,B", "00101001","11001111","00111111"}); lookupTable.put("300101000", new String[]{"00101000", "00101000", "00101000", "A,B,C:C:A,B:A,C", "00101000","11110000","00111100","11001100"}); lookupTable.put("300100111", new String[]{"00100111", "00100111", "00100111", "A,B,C:B,C:A,C:A,B", "00100111","00111111","11001111","00111111"}); lookupTable.put("300100110", new String[]{"00100110", "00100110", "00100110", "A,B,C:B,C:A,C:A,B", "00100110","00111111","11001111","00111111"}); lookupTable.put("300100101", new String[]{"00100101", "00100101", "00100101", "A,B,C:B,C:A,C:A,B", "00100101","00111111","11000011","00111111"}); lookupTable.put("300100100", new String[]{"00100100", "00100100", "00100100", "A,B,C:B,C:A,B:A,C", "00100100","00111111","00111100","11000011"}); lookupTable.put("300100011", new String[]{"00100011", "00100011", "00100011", "A,B,C:B,C:B:A,C:A,B", "00100011","00111111","00001111","11001111","00110011"}); lookupTable.put("300100010", new String[]{"00100010", "00100010", "00100010", "A,B,C:B,C:B:C:A,C:A,B", "00100010","00111111","00001111","11110000","11001100","00110011"}); lookupTable.put("300100001", new String[]{"00100001", "00100001", "00100001", "A,B,C:B,C:B:A,C:A,B", "00100001","00111111","00001111","11000011","00110011"}); lookupTable.put("300100000", new String[]{"00100000", "00100000", "00100000", "A,B,C:B,C:A:B:C:A,B:A,C:C", "00100000","00111111","11110000","00001111","11110000","00111100","11000000","11110000"}); lookupTable.put("300011110", new String[]{"00011110", "00011110", "00011110", "A,B,C:A,C:A,B", "00011110","00111111","00111111"}); lookupTable.put("300011101", new String[]{"00011101", "00011101", "00011101", "A,B,C:A,C:A,B", "00011101","00111111","00111111"}); lookupTable.put("300011100", new String[]{"00011100", "00011100", "00011100", "A,B,C:A,C:A,B", "00011100","00111111","00111100"}); lookupTable.put("300011011", new String[]{"00011011", "00011011", "00011011", "A,B,C:A,C:A,B", "00011011","00111111","00111111"}); lookupTable.put("300011010", new String[]{"00011010", "00011010", "00011010", "A,B,C:A,C:A,B", "00011010","00111100","00111111"}); lookupTable.put("300011001", new String[]{"00011001", "00011001", "00011001", "A,B,C:A,C:A,B", "00011001","00111111","00111111"}); lookupTable.put("300011000", new String[]{"00011000", "00011000", "00011000", "A,B,C:A,C:A,B", "00011000","00111100","00111100"}); lookupTable.put("300010111", new String[]{"00010111", "00010111", "00010111", "A,B,C:A,C:A,B", "00010111","00111111","00111111"}); lookupTable.put("300010110", new String[]{"00010110", "00010110", "00010110", "A,B,C:A,C:A,B", "00010110","00111111","00111111"}); lookupTable.put("300010101", new String[]{"00010101", "00010101", "00010101", "A,B,C:A,C:C:A,B", "00010101","00110011","00111111","00111111"}); lookupTable.put("300010100", new String[]{"00010100", "00010100", "00010100", "A,B,C:A,C:C:A,B", "00010100","00110011","00111111","00111100"}); lookupTable.put("300010011", new String[]{"00010011", "00010011", "00010011", "A,B,C:A,C:B:A,B", "00010011","00111111","00001111","00110011"}); lookupTable.put("300010010", new String[]{"00010010", "00010010", "00010010", "A,B,C:A,C:B:A,B", "00010010","00111100","00001111","00110011"}); lookupTable.put("300010001", new String[]{"00010001", "00010001", "00010001", "A,B,C:A,C:B:C:A,B", "00010001","00110011","00001111","00111111","00110011"}); lookupTable.put("300010000", new String[]{"00010000", "00010000", "00010000", "A,B,C:A,C:A:B:C:A,B", "00010000","00110000","11110000","00001111","11110000","00111100"}); lookupTable.put("300001110", new String[]{"00001110", "00001110", "00001110", "A,B,C:A,C:A,B:A", "00001110","00001111","00001111","00001111"}); lookupTable.put("300001101", new String[]{"00001101", "00001101", "00001101", "A,B,C:A,C:A,B:A", "00001101","00001111","00001111","00001111"}); lookupTable.put("300001100", new String[]{"00001100", "00001100", "00001100", "A,B,C:A:B:A,B:A,C:B:A,B", "00001100", "00001111", "11110000", "00001100","00001111","11110000","00001100"}); lookupTable.put("300001011", new String[]{"00001011", "00001011", "00001011", "A,B,C:A,C:A,B:A", "00001011","00001111","00001111","00001111"}); lookupTable.put("300001010", new String[]{"00001010", "00001010", "00001010", "A,B,C:A,C:A,B:C:A", "00001010","00001100","00001111","11110000","00001111"}); lookupTable.put("300001001", new String[]{"00001001", "00001001", "00001001", "A,B,C:A,C:A,B:A", "00001001","00001111","00001111","00001111"}); lookupTable.put("300001000", new String[]{"00001000", "00001000", "00001000", "A,B,C:A,C:A,B:B:A", "00001000","00001100","00001100","11110000","11110000","00001111"}); lookupTable.put("300000110", new String[]{"00000110", "00000110", "00000110", "A,B,C:A,C:A,B:A", "00000110","00001111","00001111","00001111","00001111"}); lookupTable.put("300000101", new String[]{"00000101", "00000101", "00000101", "A,B,C:B:B,C:A,C:A,B:C:A", "00000101", "00001111", "00001111","00000011","00001111","00001111","00001111"}); lookupTable.put("300000100", new String[]{"00000100", "00000100", "00000100", "A,B,C:A,C:A,B:B,C:B:C:A,B:A", "00000100","00001111","00001100","00111111","11110000","00111111","000001100","00001111"}); lookupTable.put("300000010", new String[]{"00000010", "00000010", "00000010", "A,B,C:A,C:A,B:B,C:B:A:C", "00000010","00001100","00000011","00000011","00001111","11110000","00001111","00001111"}); } //Test Unsatisfiable 3-Sat Clauses //static int[][] testClauses = {{0},{1}}; //static int[][] testClauses = {{1,2},{0,3},{0,2},{1,3}}; //static int[][] testClauses = {{1},{3},{1,2},{0,3},{0,2},{1,3}}; //static int[][] testClauses = {{1},{3},{0,3},{0,2}}; static int[][] testClauses = { {0,2,4},{0,2,5},{0,3,4},{0,3,5},{1,2,4},{1,2,5},{1,3,4}, {8,11,4},{8,2,5},{8,3,4},{8,3,5},{11,2,4},{11,2,5},{11,3,4},{11,3,5}, {30,2,4},{30,11,5},{30,3,4},{30,11,5},{17,2,4},{17,2,5},{17,3,4},{1,3,5}, {0,2,4},{0,2,5},{0,3,4},{0,3,5},{1,6,8},{1,6,9},{1,7,8} }; // static int[][] testClauses = { // {0,2,4},{0,2,5},{0,3,4},{0,3,5},{1,2,4},{1,2,5},{1,3,4}, // {30,12,14},{30,12,15},{30,13,14},{30,13,15}, // {1,12,14},{1,12,15},{1,13,14},{1,13,15}, // {0,2,4},{0,2,5},{0,3,4},{0,3,5},{1,6,8},{1,6,9},{1,7,8},{1,7,9} // }; // static int[][] testClauses = {{0,2,4},{0,2,5},{0,3,4},{0,3,5},{1,6,8},{1,6,9},{1,7,8},{1,7,9}}; // static int[][] testClauses = {{1},{0,2,4},{0,2,5},{0,3,4},{0,3,5}}; // static int[][] testClauses = {{6},{1,6,8},{1,6,9},{1,7,8},{1,7,9}}; // static int[][] testClauses = {{0,2,4},{0,2,5},{0,3,4},{0,3,5},{1,2,4},{1,2,5},{1,3,4},{1,3,5}}; public static void main(String[] args) { int i=0; //We expect a sorted non-messy input with nonsense clauses and duplicate literals removed. So A or !A or A is already gone. while (i < testClauses.length && testClauses[i].length < 2){ System.out.println(Arrays.toString(testClauses[i])); String result; try { result = bitwiseAND(lookupTable.get("["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) +"]")[0], lookupTable.get(testClauses[i][0]%2==0?"0":"1")[0]); } catch (Exception e) { result = bitwiseAND("11111111", //Default to TRUE lookupTable.get(testClauses[i][0]%2==0?"0":"1")[0] ); //Value specified by lookup table } result = padLeftZeros(result,permutations); //Java has a bad habit of dropping the leading zeros... if (result.equals("00000000")){ System.out.println("Unsat!"); System.exit(0);} lookupTable.put("["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) +"]",new String[]{result}); i++; System.out.println(result); } while (i < testClauses.length && testClauses[i].length < 3){ System.out.println(Arrays.toString(testClauses[i])); String result; try { System.out.println(lookupTable.get("["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) +","+(testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1)+"]")[0]); result = bitwiseAND( lookupTable.get("["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) +","+(testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1)+"]")[0], lookupTable.get( (testClauses[i][0]%2==0?"0":"1") + (testClauses[i][1]%2==0?"0":"1") )[0] ); } catch (Exception e) { result = bitwiseAND("11111111", //Default to TRUE lookupTable.get( (testClauses[i][0]%2==0?"0":"1") + (testClauses[i][1]%2==0?"0":"1") )[0] ); //Value specified by lookup table } assign("["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) +","+ (testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1)+"]", result, new String[]{ String.valueOf(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1), String.valueOf(testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1) } ); String A = clauseLookup(0, "["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) + "]"), B = clauseLookup(1, "["+(testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1) + "]"); System.out.println("---TEST----"); System.out.println(result); System.out.println(A); System.out.println(B); System.out.println("---END TEST----"); result = bitwiseAND(A, bitwiseAND(B, result)); result = padLeftZeros(result,permutations); //Java has a bad habit of dropping the leading zeros... if (result.equals("00000000")){ System.out.println("Unsat!"); System.exit(0);} i++; System.out.println(result); } while (i < testClauses.length && testClauses[i].length < 4){ System.out.println(Arrays.toString(testClauses[i])); String result; try { System.out.println( lookupTable.get("["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) +","+ (testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1)+","+ (testClauses[i][2]%2==0?testClauses[i][2]:testClauses[i][2]-1)+"]")[0] ); result = bitwiseAND( lookupTable.get("["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) +","+ (testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1)+","+ (testClauses[i][2]%2==0?testClauses[i][2]:testClauses[i][2]-1)+"]")[0], lookupTable.get( (testClauses[i][0]%2==0?"0":"1") + (testClauses[i][1]%2==0?"0":"1") + (testClauses[i][2]%2==0?"0":"1") )[0] ); } catch (Exception e) { result = bitwiseAND("11111111", //Default to TRUE lookupTable.get( (testClauses[i][0]%2==0?"0":"1") + (testClauses[i][1]%2==0?"0":"1") + (testClauses[i][2]%2==0?"0":"1") )[0] ); //Value specified by lookup table } assign("["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) +","+ (testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1)+","+ (testClauses[i][2]%2==0?testClauses[i][2]:testClauses[i][2]-1)+"]", result, new String[]{ String.valueOf(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1), String.valueOf(testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1), String.valueOf(testClauses[i][2]%2==0?testClauses[i][2]:testClauses[i][2]-1) } ); String A = clauseLookup(0, "["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) + "]"), B = clauseLookup(1, "["+(testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1) + "]"), C = clauseLookup(2, "["+(testClauses[i][2]%2==0?testClauses[i][2]:testClauses[i][2]-1) + "]"), AB = clauseLookup(0, "["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) + ","+ (testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1) +"]"), AC = clauseLookup(1, "["+(testClauses[i][0]%2==0?testClauses[i][0]:testClauses[i][0]-1) + ","+ (testClauses[i][2]%2==0?testClauses[i][2]:testClauses[i][2]-1) + "]"), BC = clauseLookup(2, "["+(testClauses[i][1]%2==0?testClauses[i][1]:testClauses[i][1]-1) + ","+ (testClauses[i][2]%2==0?testClauses[i][2]:testClauses[i][2]-1) + "]"); System.out.println("---TEST----"); System.out.println(" A="+A); System.out.println(" B="+B); System.out.println(" C="+C); System.out.println("AB="+AB); System.out.println("AC="+AC); System.out.println("BC="+BC); System.out.println("----------"); result = padLeftZeros(bitwiseAND(A, bitwiseAND(B, bitwiseAND(C, bitwiseAND(AB, bitwiseAND(AC, bitwiseAND(BC, result)))))),permutations); //Java has a bad habit of dropping the leading zeros... if (result.equals("00000000")){ System.out.println("Unsat!"); System.exit(0);} i++; System.out.println(result); } } static String[] letters = {"A","B","C"}; public static void assign(String assignedIndex, String nextValue, String[] clauseIndexes){ // Recursive Assignment function try { // System.out.println("test"); // System.out.println(clauseIndexes.length+nextValue); String[] positionalResults = lookupTable.get(clauseIndexes.length+nextValue); for (int i = 0; i < clauseIndexes.length; i++) { positionalResults[3] = positionalResults[3].replace(letters[i], clauseIndexes[i]); // System.out.println(Arrays.toString(positionalResults)); } String[] matches = positionalResults[3].split(":"); for(int i = 0; i < matches.length; i++){ // System.out.println("TEST2"); // System.out.println(clauseLookup(0,"[" + matches[i] + "]")); // System.out.println(positionalResults[i+4]); String tempNextValue = padLeftZeros( bitwiseAND( clauseLookup(0,"[" + matches[i] + "]"), positionalResults[i+4] ), permutations ); // System.out.println(tempNextValue); // System.out.println("ENDTEST2"); lookupTable.put("[" + matches[i] + "]",new String[]{tempNextValue}); } } catch (Exception e) { e.printStackTrace(); lookupTable.put(assignedIndex, new String[]{nextValue}); } } public static String bitwiseAND(String value1, String value2){ String result = Integer.toBinaryString( new BigInteger(value1, 2).and(new BigInteger(value2, 2)).intValue()); return padLeftZeros(result, permutations); /// Keep leading zeros. } public static String padLeftZeros(String inputString, double length) { if (inputString.length() >= length) { return inputString; } StringBuilder sb = new StringBuilder(); while (sb.length() < length - inputString.length()) { sb.append('0'); } sb.append(inputString); return sb.toString(); } public static String clauseLookup(int position, String index){ // index should be a clause [24,12,32] try{ return lookup(position, lookupTable.get(index)[0]); } catch (Exception e) { return "11111111"; } } public static String lookup(int position, String index){ //index should be a binary value 00000000 try { return lookupTable.get(index)[position]; } catch (Exception e) { return index; } } } Â Link to comment Share on other sites More sharing options...
Recommended Posts
Create an account or sign in to comment
You need to be a member in order to leave a comment
Create an account
Sign up for a new account in our community. It's easy!
Register a new accountSign in
Already have an account? Sign in here.
Sign In Now