A1049. 命题逻辑

题目http://www.tsinsen.com/A1049

这道题的目的是是求一个命题表达式是否恒正确或者衡错误，但是她很贴心的把表达式中的子式拆开。举个例子(!p+p)^(!a+a),他会拆分成：

A1 !p+p

A2 !a+a

A3 A1^A2

显然A1，2，3都是重言式。

于是这道题的思路就是：

1.求出所有变量的排列组合：比如三个变量就是000,001,011,101.....

2.对每一个排列组合给出结果也就是按先后顺序求出A1,2,3...

如果所得结果全是1，重言，0，矛盾，不然-1.

因为这很有可能是个整体式子所以必须先确定赋值，比如000，才能给出每个式子A123的结果，只有结果全出来（变量三个那就一共有九个结果）才能确定是不是矛盾重言。

对于求排列组合，可以用递归法，但是由于这道题就四个变量也可以四个循环，推荐递归，因为循环不具有推广性。我用的递归，到最底层之后调用表达式求值的式子。对于这个例子，由于都是01的组合所以可以用bitset函数从0-7翻译成二进制来枚举3个变量的可能，或者0-15枚举四个变量。

题目可能含有低级式子不会包含高级式子的意思，但是我还是要在算每个式子之前判断一下他所涉及的变量是不是已经计算过了。

如果看不明白可以删掉cout之前的//，看一下关键的输出。

下面是代码：

#include <iostream>
#include <stdio.h>
using namespace std;
char str[10][12];
int a[11][17];//每行是给出的变量，列代表对每个排列组合的结果
int m,n;
bool c[10];//将递归结果存入该数组
int no=0;//每递归到底，序号加一，代表本次递归完成，可以开始计算了
//函数用来计算前驱的值，是拓扑的。pre表示A后面的序号，A0这样
void cal(int pre)
{
    bool re;
    bool le,ri;
    if(str[pre][3]=='A'&&a[str[pre][4]-'0'][no]==0)//逻辑式包含了一个没有赋值的Ai
    {
        cal(str[pre][4]-'0');
    }
    else if(str[pre][3]=='A')
    {
        if(a[str[pre][4]-'0'][no]==1)
            le=true;
        else if(a[str[pre][4]-'0'][no]==-1)
            le=false;
    }
    if(str[pre][8]=='A'&&a[str[pre][9]-'0'][no]==0)
    {
        cal(str[pre][9]-'0');
    }
    else if(str[pre][8]=='A')
    {
        if(a[str[pre][9]-'0'][no]==1)
            ri=true;
        else if(a[str[pre][9]-'0'][no]==-1)
            ri=false;
    }
    if(str[pre][3]=='P')
        le=c[str[pre][4]-'0'];
    if(str[pre][8]=='P')
        ri=c[str[pre][9]-'0'];
  //      cout<<"le = "<<le<<endl;
  //      cout<<"ri = "<<ri<<endl;
    switch(str[pre][6])
    {
    case'>':
        re=le<=ri;
        break;
    case'^':
        re=le&&ri;
        break;
    case'v':
        re=le||ri;
        break;
    case'~':
    {
        if(str[pre][3]=='p')
            re=!le;
        else
            re=!ri;
            break;
    }
    }
    if(re==true)
        a[pre][no]=1;
    else
        a[pre][no]=-1;
}
//函数用来判断是否是重言式，只需要对每个变量挨个赋值，得到结果后直接将子式看成变量
void findall(int all)
{
    if(all>0)
    {
        c[n-all]=true;
        findall( all-1);
        c[n-all]=false;
        findall(all-1);
    }
    else if(all==0)
    {
 //       cout<<no<<endl;
  //      cout<<c[0]<<" "<<c[1]<<" "<<c[2]<<" "<<c[3]<<endl;
        for(int i=0; i < m; i++)
        {
            if(a[i][no]==0)
                cal(i);
//cout<<"result is "<<a[i][no]<<" in "<<str[i][6]<<endl;;
        }
        no++;

    }
}
int main()
{

    cin>>n;
    cin>>m;

//用getchar获取上一行剩余的空格
    getchar();
    for(int i = 0; i <m; i++)
    {
        cin.getline(str[i],12);
    }

    /*for(int i = 0; i < m; i++)
    {
        cout<<str[i]<<endl;
    }
    for(int i=0;i<16;i++){
        for(int j=0;j<4;j++)
        cout<<b[i][j];
        cout<<endl;
    }
    */
    findall(n);

    int one=0;
    int zero=0;
    for(int j=0; j<no; j++)
    {
        if(a[m-1][j]==1)
            one++;
        else if(a[m-1][j]==-1)
            zero++;
        else
            cout<<"wrong"<<j<<endl;
    }
    if(one==no)
        cout<<1<<endl;
    else if(zero==no)
        cout<<-1<<endl;
    else
        cout<<0<<endl;


    return 0;
}