import java.util.Scanner; import java.util.regex.Pattern; /** * BruteForce! */ public class cnf { static final Pattern AND = Pattern.compile(" \\^ "); static final Pattern OR = Pattern.compile(" v "); static boolean[] values; static int[][] clauses; static long counter = 0; public static void main(String[] args) { Scanner scanner = new Scanner(System.in); int n = scanner.nextInt(); scanner.nextLine(); String input = scanner.nextLine(); String[] clausesStr = AND.split(input); values = new boolean[n + 1]; clauses = new int[clausesStr.length][]; int clauseIdx = 0; for (String clauseStr : clausesStr) { String[] literalsStr = OR.split(clauseStr.substring(1, clauseStr.length() - 1)); int literalIdx = 0; int[] literal = new int[literalsStr.length]; for (String literalStr : literalsStr) { literal[literalIdx++] = literalToInt(literalStr); } clauses[clauseIdx++] = literal; } generate(values, 1, n + 1); System.out.println(counter); } static void generate(boolean[] values, int idx, int n) { if (idx == n) { check(values); return; } values[idx] = false; generate(values, idx + 1, n); values[idx] = true; generate(values, idx + 1, n); } static void check(boolean[] values) { for (int[] clause : clauses) { boolean clauseValue = false; for (int literal : clause) { clauseValue = literal < 0 ? (!values[-literal]) : (values[literal]); if (clauseValue) { break; } } if (!clauseValue) { return; } } counter += 1; } static int literalToInt(String str) { int value = 0, len = str.length(); if (str.charAt(0) == '~') { for (int i = 2; i < len; ++i) { value = value * 10 + (str.charAt(i) - '0'); } return - value; } else { for (int i = 1; i < len; ++i) { value = value * 10 + (str.charAt(i) - '0'); } return value; } } }
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 | import java.util.Scanner; import java.util.regex.Pattern; /** * BruteForce! */ public class cnf { static final Pattern AND = Pattern.compile(" \\^ "); static final Pattern OR = Pattern.compile(" v "); static boolean[] values; static int[][] clauses; static long counter = 0; public static void main(String[] args) { Scanner scanner = new Scanner(System.in); int n = scanner.nextInt(); scanner.nextLine(); String input = scanner.nextLine(); String[] clausesStr = AND.split(input); values = new boolean[n + 1]; clauses = new int[clausesStr.length][]; int clauseIdx = 0; for (String clauseStr : clausesStr) { String[] literalsStr = OR.split(clauseStr.substring(1, clauseStr.length() - 1)); int literalIdx = 0; int[] literal = new int[literalsStr.length]; for (String literalStr : literalsStr) { literal[literalIdx++] = literalToInt(literalStr); } clauses[clauseIdx++] = literal; } generate(values, 1, n + 1); System.out.println(counter); } static void generate(boolean[] values, int idx, int n) { if (idx == n) { check(values); return; } values[idx] = false; generate(values, idx + 1, n); values[idx] = true; generate(values, idx + 1, n); } static void check(boolean[] values) { for (int[] clause : clauses) { boolean clauseValue = false; for (int literal : clause) { clauseValue = literal < 0 ? (!values[-literal]) : (values[literal]); if (clauseValue) { break; } } if (!clauseValue) { return; } } counter += 1; } static int literalToInt(String str) { int value = 0, len = str.length(); if (str.charAt(0) == '~') { for (int i = 2; i < len; ++i) { value = value * 10 + (str.charAt(i) - '0'); } return - value; } else { for (int i = 1; i < len; ++i) { value = value * 10 + (str.charAt(i) - '0'); } return value; } } } |