import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
import java.util.Scanner;
import java.util.Set;
import java.util.TreeSet;

// William John Holden
// https://wjholden.com
// 2019-07-05
//
// Tested successfully using the PowerShell command
// (gci aim-50*.cnf) + (gci aim-100*.cnf) | % { echo $_.Name; gc $_ | java ..\SAT.java } | sls "aim|Satisfiable" | tee result.txt
// against AIM test cases by Asahiro, Iwama, and Miyano found at
// https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/DIMACS/AIM/aim.tar.gz
//
// If I were to guess I would say this is bounded above by O(2^n * m^2), where
// n is the nubmer of variables and m is the number of clauses.
// In the worst case we branch twice for every variable, and at each branch we
// iterate over every clause. The number of clauses is reduced at each branch, but
// the triangular number is still quadratic.
//
// Benchmark with this command:
// (gci aim-100*.cnf) | % { (Measure-Command { gc $_ | java ..\SAT.java }).TotalMilliseconds } | ft
//
// An earlier version of this program used List<List<Integer>> instead of 
// List<int[]>. This change resulted in a ~10% speedup, which is nice but not
// as exciting as I had hoped for.
public class SAT {
    
    public static List<Integer> isSatisfiable(final List<int[]> f) {
        // Originally there was a base case that searched F for an empty
        // clause. This base case is not necessary now that we use the 
        // fail early method.
        if (f.isEmpty()) {
            // An empty formula is a satisfied formula.
            return new ArrayList<>();
        } else {
            // Recursive case. Select the first variable in the first clause.
            // We initially set it to true. Create a new formula where you
            // remove all clauses that are satisfied by the assignment
            // and remove the variable from all clauses where it does not
            // satisfy the clause.
            final int v = f.get(0)[0];
            final int values[] = new int[] { v, -v };
            
            VariableLoop:
            for (int variable : values) {
                final List<int[]> fprime = new ArrayList<>();
                for (int[] clause : f) {
                    switch (contains(clause, variable)) {
                        case 1:
                            // Clause is satisfied. Do not add clause to F'.
                            break;
                        case -1: 
                            // Fail early. If the clause contained the variable
                            // but the clause has only length 1 then when we falsify
                            // the clause then the entire formula becomes unsatisfiable.
                            // Do not continue iterating through clauses.
                            // See https://twitter.com/wjholdentech/status/1147266662246170624
                            if (clause.length == 1) {
                                continue VariableLoop;
                            } else {
                                int cprime[] = new int[clause.length - 1];
                                for (int i = 0, k = 0 ; i < clause.length ; i++) {
                                    if (clause[i] != -variable) {
                                        cprime[k] = clause[i];
                                        k++;
                                    }
                                }
                                fprime.add(cprime);
                            }
                            break;
                        case 0:
                            fprime.add(clause);
                            break;
                    }
                }

                final List<Integer> sat = isSatisfiable(fprime);
                if (sat != null) {
                    sat.add(variable);
                    return sat;
                }
            }
            return null;
        }
    }
    
    static List<int[]> parseDIMACS(final Scanner sc) {
        List<int[]> input = new ArrayList<>();
        
        // In my application I usually need to skip the first line.
        sc.nextLine();
        
        while (sc.hasNextLine()) {
            String line = sc.nextLine().trim();
            if (line.isEmpty()) {
                // Skip blank lines.
            } else if (line.startsWith("c")) {
                // Ignore comments.
            } else if (line.startsWith("p")) {
                // Assume the formula is given in conjunctive normal form.
            } else {
                // Some ugly logic to handle weird inputs, such as missing
                // a zero or doubled variables in the same clause.
                final String[] split = line.split("\\s+");
                final TreeSet<Integer> c = new TreeSet<>();
                for (String variable : split) {
                    Integer i = Integer.parseInt(variable);
                    if (i != 0) c.add(i);
                }
                final int clause[] = new int[c.size()];
                int i = 0;
                while (!c.isEmpty()) {
                    clause[i++] = c.pollFirst();
                }
                input.add(clause);
            }
        }
        // Shuffling the AIM inputs will completely wreck the performance of this algorithm.
        //Collections.shuffle(input);
        return Collections.unmodifiableList(input);
    }
    
    // Determine if an integer or its negation is in an array.
    private static int contains(int[] a, int v) {
        for (int value : a) {
            if (value == v) {
                return 1;
            } else if (value == -v) {
                return -1;
            }
        }
        return 0;
    }
    
    public static void main (final String args[]) {
        final List<int[]> input;
        if (args.length > 0) {
            input = parseDIMACS(new Scanner(SIMPLE_TEST_CASES[Integer.valueOf(args[0])]));
        } else {
            input = parseDIMACS(new Scanner(System.in));
        }
        
        List<Integer> sat = isSatisfiable(input);
        if (sat != null) {
            System.out.println("SATISFIABLE");
            getVariables(input).forEach(v -> {
                if (!sat.contains(v) && !sat.contains(-v)) {
                    sat.add(v);
                }
            });
            sat.sort((a,b) -> Integer.valueOf(Math.abs(a)).compareTo(Math.abs(b)));
            sat.forEach(l -> System.out.print(l + " "));
            System.out.println();
        } else {
            System.out.println("UNSATISFIABLE");
        }
    }
    
    // Often the set of satisfying assignments returned by isSatisfiable() is
    // not complete. This helper function gets a list of all variables in
    // the input. You can use this information to infer what is missing.
    // This function returns only positive numbers.
    private static Set<Integer> getVariables(List<int[]> input) {
        Set<Integer> s = new TreeSet<>();
        input.forEach(clause -> {
            for (int v : clause) {
                s.add(Math.abs(v));
            }
        });
        return s;
    }
    
    public static final String SIMPLE_TEST_CASES[] = new String[] { 
        "c Satisfiable\n" +
        "p cnf 3 4\n" +
        "1 2 3 0\n" +
        "-1 2 3 0\n" +
        "1 -2 3 0\n" +
        "1 2 -3 0 ",
        
        "c Satisfiable\n" +
        "p cnf 3 3\n" +
        "1 2 3 0\n" +
        "1 -2 0\n" +
        "2 -3 0",

        "c Not satisfiable\n" +
        "p cnf 3 5\n" +
        "1 2 3 0\n" +
        "1 -2 0\n" +
        "2 -3 0\n" +
        "3 -1 0\n" +
        "-1 -2 -3 0",
        
        "c 2SAT Satisfiable\n" +
        "p cnf 3 3\n" +
        "1 -3\n" +
        "-1 2\n" +
        "-2 -3",
        
        "c 2SAT Not Satisfiable\n" +
        "p cnf 1 2\n" +
        "1 1\n" +
        "-1 -1"
    };
}