消解算法

淩亂°似流年 2022-06-02 08:58 122阅读 0赞

实现功能：消解算法

输入：合式公式 A 的合取范式

输出：当 A 是可满足时，回答“YES ”；否则回答“NO”。

输入公式的符号说明：

! 非，相当于书面符号中的 “ ¬ ”

& 与，相当于书面符号中的 “ ∧ ”

| 或，相当于书面符号中的 “ ∨ ”

\- 蕴含联结词，相当于书面符号中的 “ → ”

\+ 等价联结词，相当于书面符号中的 “ ↔ ”

( 前括号

) 后括号

<table style="width:1615px; margin-bottom:20px; background-color:transparent"> 
 <thead> 
  <tr> 
   <th style="padding:4px; line-height:20px; vertical-align:bottom; border-top-width:0px"> &nbsp;</th> 
   <th style="padding:4px; line-height:20px; vertical-align:bottom; border-top-width:0px"> 测试输入<span><a href="http://online.bit.edu.cn/moodle/help.php?component=programming&amp;identifier=input&amp;lang=zh_cn" title="关于“测试输入”的帮助" style="color:rgb(67,142,185)" rel="nofollow"><img src="http://online.bit.edu.cn/moodle/theme/image.php/lambda/core/1510491239/help" alt="关于“测试输入”的帮助" style="vertical-align:text-bottom; border:0px; height:16px; padding-left:3px; width:16px"></a></span></th> 
   <th style="padding:4px; line-height:20px; vertical-align:bottom; border-top-width:0px"> 期待的输出<span><a href="http://online.bit.edu.cn/moodle/help.php?component=programming&amp;identifier=expectedoutput&amp;lang=zh_cn" title="关于“期待的输出”的帮助" style="color:rgb(67,142,185)" rel="nofollow"><img src="http://online.bit.edu.cn/moodle/theme/image.php/lambda/core/1510491239/help" alt="关于“期待的输出”的帮助" style="vertical-align:text-bottom; border:0px; height:16px; padding-left:3px; width:16px"></a></span></th> 
   <th style="padding:4px; line-height:20px; vertical-align:bottom; border-top-width:0px"> 时间限制<span><a href="http://online.bit.edu.cn/moodle/help.php?component=programming&amp;identifier=timelimit&amp;lang=zh_cn" title="关于“时间限制”的帮助" style="color:rgb(67,142,185)" rel="nofollow"><img src="http://online.bit.edu.cn/moodle/theme/image.php/lambda/core/1510491239/help" alt="关于“时间限制”的帮助" style="vertical-align:text-bottom; border:0px; height:16px; padding-left:3px; width:16px"></a></span></th> 
   <th style="padding:4px; line-height:20px; vertical-align:bottom; border-top-width:0px"> 内存限制<span><a href="http://online.bit.edu.cn/moodle/help.php?component=programming&amp;identifier=memlimit&amp;lang=zh_cn" title="关于“内存限制”的帮助" style="color:rgb(67,142,185)" rel="nofollow"><img src="http://online.bit.edu.cn/moodle/theme/image.php/lambda/core/1510491239/help" alt="关于“内存限制”的帮助" style="vertical-align:text-bottom; border:0px; height:16px; padding-left:3px; width:16px"></a></span></th> 
   <th style="padding:4px; line-height:20px; vertical-align:bottom; border-top-width:0px"> 额外进程<span><a href="http://online.bit.edu.cn/moodle/help.php?component=programming&amp;identifier=nproc&amp;lang=zh_cn" title="关于“{$a} 个额外进程”的帮助" style="color:rgb(67,142,185)" rel="nofollow"><img src="http://online.bit.edu.cn/moodle/theme/image.php/lambda/core/1510491239/help" alt="关于“{$a} 个额外进程”的帮助" style="vertical-align:text-bottom; border:0px; height:16px; padding-left:3px; width:16px"></a></span></th> 
  </tr> 
 </thead> 
 <tbody> 
  <tr> 
   <td style="padding:4px; line-height:20px; vertical-align:middle; background-color:rgb(249,249,249)"> 测试用例 1</td> 
   <td style="padding:4px; line-height:20px; vertical-align:middle; background-color:rgb(249,249,249)"> <a href="http://online.bit.edu.cn/moodle/mod/programming/testcase/download_io.php?id=57585&amp;test=69885&amp;type=in&amp;download=0" style="color:rgb(67,142,185); font-size:9pt" rel="nofollow">以文本方式显示</a> 
    <div style="vertical-align:top; padding:0px 5px 0px 0px; width:10em; height:10em; overflow:auto"> 
     <ol style="padding-left:0px; margin-bottom:0px; margin-left:2.5em; overflow:visible"> 
      <li style="line-height:20px; font-family:Consolas,'Courier New',Courier,mono,serif; margin:0px; padding:0px; overflow:visible"> <span style="margin:0px; padding:0px; white-space:nowrap; background-color:rgb(211,211,211)">(!p|q)&amp;(p|q)&amp;(!q)↵</span></li> 
     </ol> 
    </div> </td> 
   <td style="padding:4px; line-height:20px; vertical-align:middle; background-color:rgb(249,249,249)"> <a href="http://online.bit.edu.cn/moodle/mod/programming/testcase/download_io.php?id=57585&amp;test=69885&amp;type=out&amp;download=0" style="color:rgb(67,142,185); font-size:9pt" rel="nofollow">以文本方式显示</a> 
    <div style="vertical-align:top; padding:0px 5px 0px 0px; width:10em; height:10em; overflow:auto"> 
     <ol style="padding-left:0px; margin-bottom:0px; margin-left:2.5em; overflow:visible"> 
      <li style="line-height:20px; font-family:Consolas,'Courier New',Courier,mono,serif; margin:0px; padding:0px; overflow:visible"> <span style="margin:0px; padding:0px; white-space:nowrap; background-color:rgb(211,211,211)">NO↵</span></li> 
     </ol> 
    </div> </td> 
   <td style="padding:4px; line-height:20px; vertical-align:middle; background-color:rgb(249,249,249)"> 无限制</td> 
   <td style="padding:4px; line-height:20px; vertical-align:middle; background-color:rgb(249,249,249)"> 64M</td> 
   <td style="padding:4px; line-height:20px; vertical-align:middle; background-color:rgb(249,249,249)"> 0</td> 
  </tr> 
  <tr> 
   <td style="padding:4px; line-height:20px; vertical-align:middle"> 测试用例 2</td> 
   <td style="padding:4px; line-height:20px; vertical-align:middle"> <a href="http://online.bit.edu.cn/moodle/mod/programming/testcase/download_io.php?id=57585&amp;test=69886&amp;type=in&amp;download=0" style="color:rgb(67,142,185); font-size:9pt" rel="nofollow">以文本方式显示</a> 
    <div style="vertical-align:top; padding:0px 5px 0px 0px; width:10em; height:10em; overflow:auto"> 
     <ol style="padding-left:0px; margin-bottom:0px; margin-left:2.5em; overflow:visible"> 
      <li style="line-height:20px; font-family:Consolas,'Courier New',Courier,mono,serif; margin:0px; padding:0px; overflow:visible"> <span style="margin:0px; padding:0px; white-space:nowrap; background-color:rgb(211,211,211)">p&amp;(p|q)&amp;(p|!q)&amp;(q|!r)&amp;(q|r)↵</span></li> 
     </ol> 
    </div> </td> 
   <td style="padding:4px; line-height:20px; vertical-align:middle"> <a href="http://online.bit.edu.cn/moodle/mod/programming/testcase/download_io.php?id=57585&amp;test=69886&amp;type=out&amp;download=0" style="color:rgb(67,142,185); font-size:9pt" rel="nofollow">以文本方式显示</a> 
    <div style="vertical-align:top; padding:0px 5px 0px 0px; width:10em; height:10em; overflow:auto"> 
     <ol style="padding-left:0px; margin-bottom:0px; margin-left:2.5em; overflow:visible"> 
      <li style="line-height:20px; font-family:Consolas,'Courier New',Courier,mono,serif; margin:0px; padding:0px; overflow:visible"> <span style="margin:0px; padding:0px; white-space:nowrap; background-color:rgb(211,211,211)">YES↵</span></li> 
     </ol> 
    </div> </td> 
   <td style="padding:4px; line-height:20px; vertical-align:middle"> 无限制</td> 
   <td style="padding:4px; line-height:20px; vertical-align:middle"> 64M</td> 
   <td style="padding:4px; line-height:20px; vertical-align:middle"> 0</td> 
  </tr> 
 </tbody> 
</table>

#include<stdio.h> 
    #include<stdlib.h> 
    #include<math.h> 
    #include<string.h> 
    #define N 100 
    int s[30][30]; 
    //每行存储一个简单析取式，第二维下标0~25代表命题变项a~z 
    //取值 0: 该变项没有出现，1: 该变项出现，2: 该变项出现且为否定 
    int s0,s1,s2;//实现对集合0，集合1，集合2 的指向 
    void save(char str[]);//将输入字符串存到s数组，标记到集合2 
    int i_same(int a[],int b[]); 
    int check(int c[]); 
    int res(int a[],int b[]); 
    int main() 
    {int i,j; 
     char str[N]; 
     scanf("%s",str); 
     save(str);  
     do{ 
        s0=s1;s1=s2;//将集合1并到集合0中，令集合1等于集合2，清空集合2 
        for(i=0;i<=s0;i++) 
      for(j=s0+1;j<=s1;j++) 
        { 
            if(!res(s[i],s[j])) 
            {printf("NO\n"); 
           return 0;} 
       } 
          for(i=s0+1;i<=s1;i++) 
       for(j=i+1;j<=s1;j++) 
        { 
          if(!res(s[i],s[j])) 
        {printf("NO\n"); 
       return 0;} 
          } 
          
         } while(s2>s1);//若集合2为空，结束 
      printf("YES\n"); 
       return 0; 
    } 
    void save(char str[]) 
    { 
       int i,j,len=strlen(str); 
       s0=s1=-1;s2=0;   
       for(i=0;i<30;i++)    for(j=0;j<30;j++) s[i][j]=0; 
       
        
       i=0;  
       while(i<len) 
       { 
        if(str[i]>='a'&&str[i]<='z') 
         s[s2][str[i]-'a']=1; 
         else if(str[i]=='&') s2++; 
         else if(str[i]=='!') 
         s[s2][str[++i]-'a']=2; 
         i++; 
       } 
    } 
    int i_same(int a[],int b[])//判断两简单析取式是否相同 
    { 
     int i; 
     for(i=0;i<26;i++) 
       if(a[i]!=b[i]) 
         return 0; 
      return 1; 
      
    } 
    int check(int c[])//检查集合0，集合1，集合2中是否有重复 
    { 
        int i; 
     for(i=0;i<=s2;i++) 
      if(i_same(s[i],c)) 
     return 0; 
       
       return 1; 
    } 
    int res(int a[],int b[])//消解函数，若得到空子句，返回0，否则返回1 
    { 
      int single=0;//不能消解的变项个数 
       int couple=0;//可消解的变项个数 
        int c[30];//消解结果 
       int i; 
     for(i=0;i<26;i++) 
       {    
           if(!a[i]&&!b[i])  continue; 
            if((a[i]==1&&b[i]==2)||(a[i]==2&&b[i]==1)) couple++; 
           else single++; 
     } 
      if(couple!=1) return 1;//不能消解或有多对可以消解 
      if(!single)   return 0;//只有一对可消解且没有不能消解的变项，得到空子句 
        
       for(i=0;i<26;i++) 
       { 
          if((!a[i]&&!b[i])||(a[i]+b[i]==3)) c[i]=0; 
         else if (a[i]==1||b[i]==1) c[i]=1; 
         else c[i]=2; 
       } 
      if(check(c))//检查c在集合0.集合1，集合2中是否出现过 
        { 
          s2++;//将c加入集合2 
         for(i=0;i<26;i++) s[s2][i]=c[i]; 
        } 
      return 1; 
    }