该题是在给定一系列的计算逻辑的基础上，询问一个表达式是否恒为真的问题，由于构成的表达式是一个以运算符开始的先序遍历的式子，所以可以利用递归进行求解。
什么是构造法呢？
1．对所讨论的对象能进行较为直观的描述；
2．实现的具体性，就是不只是判明某种解的存在性，而且要实现具体求解。
代码如下：
#include <cstring> #include <cstdio> #include <cstdlib> using namespace std; char s[105]; int K[2][2] = {0, 0, 0, 1}, A[2][2] = {0, 1, 1, 1}; int N[2] = {1, 0}, C[2][2] = {1, 1, 0, 1}, E[2][2] = {1, 0, 0, 1}; int pos; bool calc(int &x) // 引用只是为了是为了避免数据的复制 { ++pos; switch (s[pos]) { // 这个括号中的运算有一个先后顺序，所以出现G++（从左至右）能多，但是C++（从右至左）不能过 case 'K': return K[calc(x)][calc(x)]; case 'A': return A[calc(x)][calc(x)]; case 'N': return N[calc(x)]; case 'C': return C[calc(x)][calc(x)]; case 'E': return E[calc(x)][calc(x)]; case 'p': return x & 1; // 分别取到压缩后的字节中的状态即可 case 'q': return x & (1 << 1); case 'r': return x & (1 << 2); case 's': return x & (1 << 3); case 't': return x & (1 << 4); } } int main() { bool yes; while (scanf("%s", s), s[0] != '0') { yes = true; // 这里的一个for循环顶五个for循环 for(int i = 0; i < 32 && yes; ++i) { pos = -1; if (!calc(i)) { yes = false; } } printf(yes ? "tautology\n" : "not\n"); } return 0; }