11357 - Ensuring Truth
Posted: Sun Nov 25, 2007 5:27 pm
SAT is NPC, so... how to solve it? Is there something about randomization algorithm? 

Code: Select all
// Remove after Acc
Code: Select all
//Problem: Ensuring Truth-11357
//Status :
//Algorithm : Boolean Exp. slution.
#include<stdio.h>
#include<string.h>
#define max 300
char stack [max];
void result(void)
{
int res[max];
int i,top=0;
for(i=0; stack[i]; i++)
{
if(stack[i] >='a' && stack[i] <='z')
res[top++] = 1;
else if(stack[i] == '&')
{
res[top-2] = res[top-2] & res[top-1];
top--;
}
else if(stack[i] == '|')
{
res[top-2] = res[top-2] | res[top-1];
top--;
}
else if(stack[i]=='~' && res[top-1])
res[top-1]=0;
else if(stack[i]=='~' && (!res[top-1]))
res[top-1]=1;
}
if(res[top-1])
printf("YES\n");
else
printf("NO\n");
}
void process(char *input)
{
char save[max];
int i,j=0,k=0,l;
l = strlen(input);
input[l]=')'; input[l+1]='\0';
save[k] = '('; k = 1;
for(i=0; input[i]; i++)
{
if(input[i] == '(')
save[k++] = input[i];
else if(input[i] >='a' && input[i] <='z')
stack[j++] = input[i];
else if(input[i] == '~')
save[k++] = input[i];
else if(input[i] == ')')
{
while(k>0 && save[k-1]!='(')
stack[j++] = save[--k];
k--;
}
else if(input[i] == '&' || input[i] == '|')
{
while(k >0 && save[k-1]!= '(')
stack[j++] = save[--k];
save[k++] = input[i];
}
}
save[k]='\0';
stack[j]='\0';
}
void take_input(void)
{
char input[max];
int i,j=0;
gets(input);
for(i=0;input[i];i++)
{
if(input[i]==' ' || input[i]=='\t')
continue;
else
input[j++]=input[i];
}
input[j]='\0';
process(input);
result();
}
int main(void)
{
int test;
//freopen("f:\\acm\\in.txt","rt",stdin);
scanf("%d\n",&test);
while(test--)
{
take_input();
}
return 0;
}
So for test case:A formula is called satisfiable if it is possible to assign values to its variables in such a way as to make the formula evaluate to true.
Code: Select all
1
(~x)
Hint: there is a non-backtracking way to solve this problemRC's wrote:I got TLE for this problem.
Is there any fast method to solve this problem ?
I use backtracking to determine if it is possible to evaluate the function and if one solution can generate 'TRUE' then i stop the backtrack..
Code: Select all
#include<stdio.h>
#include<string.h>
int main()
{
int op,len,j,i,l,k,t,stack[1001],exp[1001],car;
char in[300],_in[300];
bool is;
scanf("%d",&t);
gets(_in);
for(j=0;j<t;j++)
{
k=0;
l=0;
op=0;
car=0;
gets(_in);
len=strlen(_in);
in[0]='(';
int ct=1;
for(i=0;i<len;i++)
{
if((_in[i]>='a' && _in[i]<='z') || _in[i]=='&' || _in[i]=='|' || _in[i]=='~' || _in[i]=='(' || _in[i]==')')
{
in[ct]=_in[i];
ct++;
}
}
in[ct]=')';
in[ct+1]='\0';
len=strlen(in);
for(i=0;i<len;i++)
{
if((in[i]=='(') || (in[i]=='&') || (in[i]=='|') || (in[i]=='~'))
{
stack[k]=in[i];
k++;
if(in[i]=='&'||in[i]=='|'||in[i]=='~')
{
op++;
}
}
else if(in[i]>='a'&&in[i]<='z')
{
exp[l]=in[i];
l++;
car++;
}
else if(in[i]==')')
{
while(k>0)
{
k--;
if(stack[k]!='(')
{
exp[l]=stack[k];
l++;
}
}
}
else
{
}
}
stack[k]='\0';
exp[l]='\0';
char st2[300];
int top=0,_p=0;
for(int i=0;i<l;i++)
{
if(exp[i]=='&'||exp[i]=='|'||exp[i]=='~')
{
if(exp[i]=='&')
{
st2[top-2]=st2[top-2]&st2[top-1];
top--;
}
else if(exp[i]=='|')
{
st2[top-2]=st2[top-2] | st2[top-1];
top--;
}
else
{
for(int p=0;p<len;p++)
{
if(in[p]==st2[top-1])
{
_p++;
}
}
if(_p>1)
{
st2[top-1]=!st2[top-1];
}
}
}
else
{
st2[top]=exp[i];
top++;
}
}
if((st2[top-1]!=false) || op<=1 || car<=1)
{
printf("YES\n");
}
else
{
printf("NO\n");
}
}
return 0;
}
Code: Select all
(x&~y)|(y&~y)