Consider the certifier for the 3-satisfiability problem (3-SAT) The definition o
ID: 3832265 • Letter: C
Question
Consider the certifier for the 3-satisfiability problem (3-SAT) The definition of the problem, certificate, and certifier are listed below. 3-SAT. Given a CNF formula phi, is there a satisfying truth assignment? Certificate. An assignment t of truth values to the n Boolean variables. Certifier. An algorithm which checks if, for the given assignment t, each clause in phi has at least one true literal. Write a program in java to implement the certifier algorithm. Given the CNF formula (x^-_1 x_2 x_3) (x_1 x^-_2 x_3) (x_1 x_2 x_4) (x^-_1 x^- _3 x^-_4) encoded in your program as a string "(NOT x1 OR X2 OR x3) AND (x1 OR NOT x2 OR x3) AND (x1 OR x2 OR x4) AND (NOT x1 OR NOT x3 OR NOT x4)", the program should certify if each of the following certificates is a satisfying truth assignment or not. (Encode each certificate as a string and parse it in your program code.) (x1 = 1, x2 = 1, x3 = 0, x4 = 1) (x1 = 1, x2 = 1, x3 = 1, x4 = 1) (x1 = 0, x2 = 0, x3 = 0, x4 = 1) (x1 = 0, x2 = 1, x3 = 0, x4 = 1)Explanation / Answer
First split the input with AND. then take each part and remove the brackets. Then split each part with OR and check all the splitted parts (if starting with NOT ,then check the value of the variable is 0 or not, otherwise check if it is 1 or not).
code:
import java.util.Scanner;
public class CNF {
public static void main(String args[]){
String s="(NOT x1 OR x2 OR x3) AND (x1 OR NOT x2 OR x3) AND (x1 OR x2 OR x4) AND (NOT x1 OR NOT x3 OR NOT x4)";
Scanner sc=new Scanner(System.in);
int x1,x2,x3,x4;
System.out.println("Enter value of variables :");
System.out.println("x1=");
x1=sc.nextInt();
System.out.println("x2=");
x2=sc.nextInt();
System.out.println("x3=");
x3=sc.nextInt();
System.out.println("x4=");
x4=sc.nextInt();
String ss[]=s.split("AND");
for(String a:ss){
a=a.trim();
a=a.substring(1,a.length()-1);
String aa[]=a.split("OR");
int trueval=0;
for(String as: aa){
if(as.trim().startsWith("NOT")){
String var=as.trim().split("NOT")[1].trim();
if(var.equals("x1") && x1==0){
trueval=1;
break;
}else if(var.equals("x2") && x2==0)
{
trueval=1;
break;
}else if(var.equals("x3") && x3==0){
trueval=1;
break;
}else if(var.equals("x4") && x4==0){
trueval=1;
break;
}
}
else{
String var=as.trim();
if(var.equals("x1") && x1==1){
trueval=1;
break;
}else if(var.equals("x2") && x2==1)
{
trueval=1;
break;
}else if(var.equals("x3") && x3==1){
trueval=1;
break;
}else if(var.equals("x4") && x4==1){
trueval=1;
break;
}
}
}
if(trueval==0){
System.out.println("does not certify");
return;
}
}
System.out.println("certifies");
}
}