Submission #3367251


Source Code Expand

import java.util.*;
public class Main{
	static String Getliteral(String clause, int bin){
		String literal = "";
		if(bin==0){
			int i = 0;
			while(!clause.substring(i, i+1).equals("v")){
				literal += clause.substring(i, i+1);
				i++;
			}
		}
		else{
			int i = 0;
			StringBuilder sb = new StringBuilder(clause);
			sb.reverse();
			while(!sb.toString().substring(i, i+1).equals("v")){
				literal = sb.toString().substring(i, i+1) + literal;
				i++;
			}
		}
		return literal;
	}

	static String Changevar(String var, String clause, int bin){
		String literal = Getliteral(clause, bin);
		if(literal.charAt(0)=='~'){
			literal = literal.substring(1);
		}
		int index = Integer.parseInt(literal) - 1;
		StringBuilder sb = new StringBuilder(var);
		if(var.charAt(index)=='T'){
			sb.setCharAt(index, 'F');
		}
		else{
			sb.setCharAt(index, 'T');
		}
		return sb.toString();
	}

	static boolean Checkclause(String clause, String var){
		String lit1 = Getliteral(clause, 0);
		String lit2 = Getliteral(clause, 1);
		int index1 = 0;
		int index2 = 0;
		if(lit1.charAt(0)=='~'){
			index1 = Integer.parseInt(lit1.substring(1)) - 1;
		}
		else{
			index1 = Integer.parseInt(lit1) - 1;
		}
		if(lit2.charAt(0)=='~'){
			index2 = Integer.parseInt(lit2.substring(1)) - 1;
		}
		else{
			index2 = Integer.parseInt(lit2) - 1;
		}
		char var1 = var.charAt(index1);
		char var2 = var.charAt(index2);
		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')){
			return false;
		}
		return true;
	}

	static int Search(String[] clause, String var){
		int index = -1;
		for(int i=0; i<clause.length; i++){
			if(Checkclause(clause[i], var)==false){
				index = i;
				break;
			}
		}
		return index;
	}

	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];
		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;
		}
		String ans = "";
		String[] var = new String[2050];
		var[0] = a;
		int now = Search(clause, var[0]);
		if(now<0){
			ans = "0";
		}
		else if(now>=0){
			int[] bin = {0, 1};
			int cnt = 0;
			Queue<Integer> queue = new ArrayDeque<Integer>();
			queue.add(now);
			while(queue.size()!=0){
				now = queue.poll();
				for(int i=0; i<=1; i++){
					cnt++;
					if(cnt>2046){
						break;
					}
					var[cnt] = Changevar(var[(cnt+1)/2-1], clause[now], i);
					if(Search(clause, var[cnt])<0){
						break;
					}
					else{
						queue.add(Search(clause, var[cnt]));
					}
				}
			}
			if(cnt>2046)ans = "TOO LARGE";
			else{
				int sum = -1;
				for(int i=0; i<=10; i++){
					sum = 2*sum + 2;
					if(cnt<=sum){
						ans = String.valueOf(i);
						break;
					}
				}
			}
		}
		else{
			ans = "TOO LARGE";
		}
		System.out.println(ans);
	}
}

Submission Info

Submission Time
Task E - 2-SAT
User Ricky_pon
Language Java8 (OpenJDK 1.8.0)
Score 0
Code Size 3295 Byte
Status WA
Exec Time 2111 ms
Memory 388200 KB

Judge Result

Set Name All
Score / Max Score 0 / 200
Status
AC × 27
WA × 2
TLE × 11
MLE × 13
Set Name Test Cases
All 00-sample-00, 00-sample-10, 00-sample-20, 10-sat-00, 10-sat-01, 10-sat-02, 10-sat-03, 10-sat-04, 10-sat-05, 10-sat-06, 10-sat-07, 10-sat-08, 10-sat-09, 10-sat-10, 10-sat-11, 10-sat-12, 10-sat-13, 10-sat-14, 10-sat-15, 10-sat-16, 10-sat-17, 10-sat-18, 10-sat-19, 10-sat-20, 10-sat-21, 10-sat-22, 10-sat-23, 10-sat-24, 10-sat-25, 10-sat-26, 10-sat-27, 10-sat-28, 10-sat-29, 10-sat-30, 10-sat-31, 10-sat-32, 10-sat-33, 10-sat-34, 10-sat-35, 10-sat-36, 10-sat-37, 10-sat-38, 10-sat-39, 20-unsat-00, 20-unsat-01, 20-unsat-02, 20-unsat-03, 20-unsat-04, 20-unsat-05, 20-unsat-06, 20-unsat-07, 20-unsat-08, 20-unsat-09
Case Name Status Exec Time Memory
00-sample-00 AC 93 ms 21204 KB
00-sample-10 AC 133 ms 31820 KB
00-sample-20 AC 187 ms 42148 KB
10-sat-00 AC 260 ms 47360 KB
10-sat-01 AC 227 ms 46728 KB
10-sat-02 AC 491 ms 95952 KB
10-sat-03 WA 481 ms 96544 KB
10-sat-04 TLE 2110 ms 357264 KB
10-sat-05 AC 509 ms 100912 KB
10-sat-06 TLE 2110 ms 360580 KB
10-sat-07 TLE 2110 ms 358652 KB
10-sat-08 TLE 2110 ms 366460 KB
10-sat-09 TLE 2111 ms 364248 KB
10-sat-10 TLE 2110 ms 370472 KB
10-sat-11 TLE 2110 ms 366812 KB
10-sat-12 TLE 2110 ms 384756 KB
10-sat-13 TLE 2110 ms 367824 KB
10-sat-14 TLE 2110 ms 375144 KB
10-sat-15 MLE 1852 ms 375092 KB
10-sat-16 TLE 2106 ms 388200 KB
10-sat-17 MLE 682 ms 310332 KB
10-sat-18 MLE 1510 ms 382504 KB
10-sat-19 MLE 909 ms 333344 KB
10-sat-20 MLE 845 ms 344972 KB
10-sat-21 WA 591 ms 178748 KB
10-sat-22 AC 703 ms 205392 KB
10-sat-23 AC 619 ms 184592 KB
10-sat-24 AC 742 ms 224580 KB
10-sat-25 AC 686 ms 195048 KB
10-sat-26 AC 724 ms 217304 KB
10-sat-27 AC 629 ms 174472 KB
10-sat-28 AC 677 ms 223392 KB
10-sat-29 AC 573 ms 174304 KB
10-sat-30 AC 687 ms 209368 KB
10-sat-31 AC 561 ms 154836 KB
10-sat-32 AC 737 ms 243472 KB
10-sat-33 AC 575 ms 187000 KB
10-sat-34 AC 693 ms 202072 KB
10-sat-35 AC 462 ms 141424 KB
10-sat-36 AC 691 ms 204732 KB
10-sat-37 AC 446 ms 108180 KB
10-sat-38 AC 709 ms 223316 KB
10-sat-39 AC 506 ms 97464 KB
20-unsat-00 MLE 866 ms 340016 KB
20-unsat-01 MLE 708 ms 287932 KB
20-unsat-02 MLE 834 ms 342904 KB
20-unsat-03 AC 505 ms 192304 KB
20-unsat-04 MLE 819 ms 346592 KB
20-unsat-05 AC 568 ms 193248 KB
20-unsat-06 MLE 822 ms 340564 KB
20-unsat-07 MLE 763 ms 275908 KB
20-unsat-08 MLE 1042 ms 386220 KB
20-unsat-09 MLE 1126 ms 319060 KB