Submission #3377294

---

Source Code Expand

import java.util.*;
public class Main{
	static int Search(String[][] literal, int[][] litvar, String var){
		int index = -1;
		for(int i=0; i<literal[0].length; i++){
			String lit1 = literal[0][i];
			String lit2 = literal[1][i];
			char var1 = var.charAt(litvar[0][i]);
			char var2 = var.charAt(litvar[1][i]);
			if((lit1.charAt(0)!='~'&&lit2.charAt(0)!='~'&&var1=='F'&&var2=='F')||(lit1.charAt(0)=='~'&&lit2.charAt(0)!='~'&&var1=='T'&&var2=='F')||(lit1.charAt(0)!='~'&&lit2.charAt(0)=='~'&&var1=='F'&&var2=='T')||(lit1.charAt(0)=='~'&&lit2.charAt(0)=='~'&&var1=='T'&&var2=='T')){
				index = i;
				break;
			}
		}
		return index;
	}
 
	static String Changevar(String var, int litvar){
		StringBuilder sb = new StringBuilder(var);
		if(var.charAt(litvar)=='T'){
			sb.setCharAt(litvar, 'F');
		}
		else{
			sb.setCharAt(litvar, 'T');
		}
		return sb.toString();
	}
 
	public static void main(String[] args){
		Scanner sc = new Scanner(System.in);
		int n = sc.nextInt();
		int m = sc.nextInt();
		String cnf = sc.next();
		String a = sc.next();
		String[] clause = new String[m];
		String[][] literal = new String[2][m];
		int[][] litvar = new int[2][m];
		Arrays.fill(clause, "");
		int j = 1;
		for(int i=0; i<m; i++){
			while(!cnf.substring(j, j+1).equals(")")){
				clause[i] += cnf.substring(j, j+1);
				j++;
			}
			j += 3;
		}
		for(int i=0; i<m; i++){
			String[] spl = clause[i].split("v", 0);
			for(int k=0; k<=1; k++){
				literal[k][i] = spl[k];
				if(literal[k][i].charAt(0)=='~'){
					litvar[k][i] = Integer.parseInt(literal[k][i].substring(1)) - 1;
				}
				else{
					litvar[k][i] = Integer.parseInt(literal[k][i]) - 1;
				}
			}
		}
 
		String ans = "";
		String[] var = new String[2050];
		var[0] = a;
		int now = Search(literal, litvar, var[0]);
		if(now<0){
			ans = "0";
		}
		else{
			int cnt = 0;
			Queue<Integer> queue = new ArrayDeque<Integer>();
			queue.add(now);
			while(queue.size()!=0){
				boolean flag = false;
				now = queue.poll();
				for(int i=0; i<=1; i++){
					cnt++;
					if(cnt>2047){
						break;
					}
					var[cnt] = Changevar(var[(cnt+1)/2-1], litvar[i][now]);
					if(Search(literal, litvar, var[cnt])<0){
						flag = true;
						break;
					}
					else{
						queue.add(Search(literal, litvar, var[cnt]));
					}
				}
				if(cnt>2046){
					ans = "TOO LARGE";
					break;
				}
				if(flag==true){
					int sum = -1;
					for(int i=0; i<=10; i++){
						sum = 2*sum + 2;
						if(cnt<=sum){
							ans = String.valueOf(i);
							break;
						}
					}
				}
			}
		}
		System.out.println(ans);
	}
}

Submission Info

Judge Result