Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- import java.util.Scanner;
- import java.util.ArrayList;
- public class Main {
- public static String clausecheck(int P, int Q, int R, int S, String clause) {
- int notP;
- int notQ;
- int notR;
- int notS;
- if (P == 0) {
- notP = 1;
- } else {
- notP = 0;
- }
- if (Q == 0) {
- notQ = 1;
- } else {
- notQ = 0;
- }
- if (R == 0) {
- notR = 1;
- } else {
- notR = 0;
- }
- if (S == 0) {
- notS = 1;
- } else {
- notS = 0;
- }
- clause = clause.replaceAll(" ", "");
- clause = clause.replaceAll("~P", notP + "");
- clause = clause.replaceAll("P", P + "");
- clause = clause.replaceAll("~Q", notQ + "");
- clause = clause.replaceAll("Q", Q + "");
- clause = clause.replaceAll("~R", notR + "");
- clause = clause.replaceAll("R", R + "");
- clause = clause.replaceAll("~S", notS + "");
- clause = clause.replaceAll("S", S + "");
- int cont = 0;
- while (!clause.equals("1") && !clause.equals("0")) {
- boolean achou1 = false;
- boolean achou2 = false;
- clause = clause.replaceAll("(0v0)", 0 + "");
- clause = clause.replaceAll("(1v0)", 1 + "");
- clause = clause.replaceAll("(0v1)", 1 + "");
- clause = clause.replaceAll("(1v1)", 1 + "");
- clause = clause.replaceAll("(0&0)", 0 + "");
- clause = clause.replaceAll("(1&0)", 0 + "");
- clause = clause.replaceAll("(0&1)", 0 + "");
- clause = clause.replaceAll("(1&1)", 1 + "");
- clause = clause.replaceAll("(0>0)", 1 + "");
- clause = clause.replaceAll("(0>1)", 1 + "");
- clause = clause.replaceAll("(1>0)", 0 + "");
- clause = clause.replaceAll("(1>1)", 1 + "");
- clause = clause.replaceAll("(0<0)", 1 + "");
- clause = clause.replaceAll("(0<1)", 0 + "");
- clause = clause.replaceAll("(1<0)", 0 + "");
- clause = clause.replaceAll("(1<1)", 1 + "");
- cont++;
- if (cont % 5 == 0) {
- for (int alfa = 0; !achou1 && alfa < clause.length(); alfa++) {
- if (clause.charAt(alfa) == ')') {
- achou1 = true;
- for (int i = alfa; !achou2 && alfa < clause.length(); i--) {
- if (clause.charAt(i) == '(') {
- achou2 = true;
- clause = clause.substring(0, alfa) + clause.substring(alfa + 1);
- clause = clause.substring(0, i) + clause.substring(i + 1);
- }
- }
- }
- }
- }
- }
- return clause;
- }
- public static void main(String[] args) {
- Scanner in = new Scanner(System.in);
- int casos = in.nextInt();
- in.nextLine();
- int problema = 1;
- while (casos-- > 0) {
- boolean SAT = false;
- System.out.println("Problema #" + problema);
- problema++;
- if (in.next().equals("TT")) {
- ArrayList<String> claus = new ArrayList<String>();
- String linha = in.nextLine();
- boolean boolP = false;
- boolean boolQ = false;
- boolean boolR = false;
- boolean boolS = false;
- int variaveis = 0;
- for (int i = 0; i < linha.length(); i++) {
- if (linha.charAt(i) == 40) {
- int fim = 0;
- int parentesis = 1;
- for (int a = i + 1; parentesis != 0 && a < linha.length(); a++) {
- if (linha.charAt(a) == 40) {
- parentesis++;
- } else if (linha.charAt(a) == 41) {
- parentesis--;
- }
- fim = a;
- }
- claus.add(linha.substring(i + 1, fim));
- } else if (linha.charAt(i) == 80) {
- boolP = true;
- } else if (linha.charAt(i) == 81) {
- boolQ = true;
- } else if (linha.charAt(i) == 82) {
- boolR = true;
- } else if (linha.charAt(i) == 83) {
- boolS = true;
- }
- }
- if (boolP) {
- variaveis++;
- System.out.print("P ");
- }
- if (boolQ) {
- variaveis++;
- System.out.print("Q ");
- }
- if (boolR) {
- variaveis++;
- System.out.print("R ");
- }
- if (boolS) {
- variaveis++;
- System.out.print("S ");
- }
- System.out.print("| ");
- int tamanho = claus.size();
- while (tamanho-- > 0) {
- System.out.print(claus.get(tamanho) + " . ");
- }
- System.out.println();
- /* comeca a imprimir aqui */
- if (variaveis == 1) {
- if (boolP) {
- for (int P = 0; P < 2; P++) {
- int x = claus.size();
- System.out.print(P + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(P, 0, 0, 0, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(P, 0, 0, 0, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- } else if (boolQ) {
- for (int Q = 0; Q < 2; Q++) {
- int x = claus.size();
- System.out.print(Q + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(0, Q, 0, 0, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(0, Q, 0, 0, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- } else if (boolR) {
- for (int R = 0; R < 2; R++) {
- int x = claus.size();
- System.out.print(R + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(0, 0, R, 0, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(0, 0, R, 0, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- } else {
- for (int S = 0; S < 2; S++) {
- int x = claus.size();
- System.out.print(S + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(0, 0, 0, S, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(0, 0, 0, S, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- } else if (variaveis == 2) {
- if (boolP && boolQ) {
- for (int P = 0; P < 2; P++) {
- for (int Q = 0; Q < 2; Q++) {
- int x = claus.size();
- System.out.print(P + " " + Q + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(P, Q, 0, 0, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(P, Q, 0, 0, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- } else if (boolP && boolR) {
- for (int P = 0; P < 2; P++) {
- for (int R = 0; R < 2; R++) {
- int x = claus.size();
- System.out.print(P + " " + R + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(P, 0, R, 0, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(P, 0, R, 0, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- } else if (boolP && boolS) {
- for (int P = 0; P < 2; P++) {
- for (int S = 0; S < 2; S++) {
- int x = claus.size();
- System.out.print(P + " " + S + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(P, 0, 0, S, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(P, 0, 0, S, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- } else if (boolQ && boolR) {
- for (int Q = 0; Q < 2; Q++) {
- for (int R = 0; R < 2; R++) {
- int x = claus.size();
- System.out.print(Q + " " + R + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(0, Q, R, 0, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(0, Q, R, 0, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- } else if (boolQ && boolS) {
- for (int Q = 0; Q < 2; Q++) {
- for (int S = 0; S < 2; S++) {
- int x = claus.size();
- System.out.print(Q + " " + S + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(0, Q, 0, S, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(0, Q, 0, S, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- } else {
- for (int R = 0; R < 2; R++) {
- for (int S = 0; S < 2; S++) {
- int x = claus.size();
- System.out.print(R + " " + S + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(0, 0, R, S, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(0, 0, R, S, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- }
- } else if (variaveis == 3) {
- if (!boolS) {
- for (int P = 0; P < 2; P++) {
- for (int Q = 0; Q < 2; Q++) {
- for (int R = 0; R < 2; R++) {
- int x = claus.size();
- System.out.print(P + " " + Q + " " + R + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(P, Q, R, 0, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(P, Q, R, 0, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- }
- } else if (!boolR) {
- for (int P = 0; P < 2; P++) {
- for (int Q = 0; Q < 2; Q++) {
- for (int S = 0; S < 2; S++) {
- int x = claus.size();
- System.out.print(P + " " + Q + " " + S + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(P, Q, 0, S, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(P, Q, 0, S, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- }
- } else if (!boolQ) {
- for (int P = 0; P < 2; P++) {
- for (int R = 0; R < 2; R++) {
- for (int S = 0; S < 2; S++) {
- int x = claus.size();
- System.out.print(P + " " + R + " " + S + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(P, 0, R, S, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(P, 0, R, S, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- }
- } else {
- for (int Q = 0; Q < 2; Q++) {
- for (int R = 0; R < 2; R++) {
- for (int S = 0; S < 2; S++) {
- int x = claus.size();
- System.out.print(Q + " " + R + " " + S + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(0, Q, R, S, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(0, Q, R, S, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- }
- }
- } else {
- for (int P = 0; P < 2; P++) {
- for (int Q = 0; Q < 2; Q++) {
- for (int R = 0; R < 2; R++) {
- for (int S = 0; S < 2; S++) {
- int x = claus.size();
- System.out.print(P + " " + Q + " " + R + " " + S + " | ");
- while (x-- > 0) {
- for (int algoqueeunaousei = 0; algoqueeunaousei < claus.get(x)
- .length(); algoqueeunaousei++) {
- System.out.print(" ");
- }
- System.out.print(clausecheck(P, Q, R, S, claus.get(x)));
- }
- System.out.println();
- if (clausecheck(P, Q, R, S, claus.get(0)).equals("1")) {
- SAT = true;
- }
- }
- }
- }
- }
- }
- }
- if (SAT) {
- System.out.println("Sim, é satisfatível.\n\n");
- } else {
- System.out.println("Não, não é satisfatível.\n\n");
- }
- }
- in.close();
- }
- }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement