Jump to content

Polynomial 3-Sat algorithm


fiveworlds
 Share

Recommended Posts

(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

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 account

Sign in

Already have an account? Sign in here.

Sign In Now
 Share

×
×
  • Create New...

Important Information

We have placed cookies on your device to help make this website better. You can adjust your cookie settings, otherwise we'll assume you're okay to continue.