构建一阶谓词逻辑和有限域上多项式方程的同构
基于命题逻辑的布尔可满足SAT存在描述能力弱、抽象层次低、求解复杂度高等问题,而基于一阶逻辑的可满足性模理论SMT(或称之为FOLMS问题:一阶逻辑的可满足性问题)采用高层建模语言,表达能力更强,更接近于字级设计, 避免将问题转化到位级求解,在硬件RTL级验证、程序验证与实时系统验证等领域得到了广泛应用;因此寻找一种一阶谓词逻辑和有限域上多项式方程的同构,将SMT问题和有限域上多项式方程组的求解问题进行相互转化具有重要的意义.
一阶谓词逻辑
(定义:一阶谓词逻辑)一阶逻辑(first order logic,FOL)也叫一阶谓词演算,允许量化陈述的公式.包含的符号有常量(Constant symbol),谓词符号(Predicate symbol),函数符号(Function symbol),变量(Variable),连词(∧,∨,→,↔)(\wedge,\vee,\rightarrow,\leftrightarrow)(∧,∨,→,↔),量词(Quantifiers)∃,∀\exists,\forall∃,∀,例如:
Father(Mary) === Bob;isFatherOf(Mary, Bob);
(定义:FOLMS问题)FOLMS问题和FOLMS问题实例判断任意一阶公式是否是可满足的问题被称为一阶公式的可满足性问题(first-order logic Satisfiablity problem,简写为FOSAT 问题),它等价于该一阶公式是否存在模型的问题.所以,一阶逻辑公式的可满足性问题也可以被称为一阶逻辑公式的模型生成(first-order logic model generating)问题或模型搜索(first-order logic model searching,简写为 FOLMS)问题.一个具体的FOLMS问题被称为是一个FOLMS问题实例.
由此可见,一阶逻辑是命题逻辑的一种推广(一阶逻辑包括命题逻辑).
同构映射
考虑一个同构映射ρ:P→F2[x1...xn]\rho:\mathcal{P} \rightarrow \mathbb{F}_2[x_1...x_n]ρ:P→F2[x1...xn],其中P\mathcal{P}P是一阶谓词的集合,P\mathcal{P}P的变元域是X\mathcal{X}X.接下来讨论怎么寻找这样的同构映射ρ\rhoρ以及它的用途.
考虑p∈p \inp∈一阶谓词的集合P\mathcal{P}P:
p:X→{True,False}tree,water↦needs(tree,water)=True\begin{aligned} p:& \mathcal{X} \rightarrow \{\text{True,False} \} \\ &\text{tree,water} \mapsto \text{needs(tree,water)=True} \end{aligned}p:X→{True,False}tree,water↦needs(tree,water)=True
那么和p∈p \inp∈一一对映的有限域上的多项式函数f∈F2[x1...xn]f \in \mathbb{F}_2[x_1...x_n]f∈F2[x1...xn]满足:
f:F2n→{1,0}v1,v2↦f(v1,v2)=1\begin{aligned} f:& \mathbb{F}_2^n \rightarrow \{\text{1,0} \} \\ &v1,v2 \mapsto f(v_1,v_2)=1 \end{aligned}f:F2n→{1,0}v1,v2↦f(v1,v2)=1
也就是说同构映射ρ\rhoρ满足:若ρ(p)=f∈F2[x1...xn]\rho(p) = f \in \mathbb{F}_2[x_1...x_n]ρ(p)=f∈F2[x1...xn],则有:
p(w1,...,wm)=True⇔f(v1,...,vm)=1p(w_1,...,w_m) = \text{True} \Leftrightarrow f(v_1,...,v_m)=1p(w1,...,wm)=True⇔f(v1,...,vm)=1
这里p(...)p(...)p(...)为mmm元谓词,v1,v2v1,v2v1,v2是F2[x1...xn]\mathbb{F}_2[x_1...x_n]F2[x1...xn]上的nnn维变量且和谓词的变元一一对应.
为什么ρ\rhoρ一定是同构不能仅仅是同态?这是因为我们希望将MQ问题转化为FOLMS问题求解后能够再等价转化回去,完成原问题的求解.
总结
在本文中我们展示了一种构建一阶谓词逻辑和有限域上多项式方程的同构的构想,事实上这可以看作SAT问题和MQ问题转化的一种泛化推广,因为一阶逻辑是命题逻辑的推广,而当一阶逻辑可满足问题和MQ问题转化中的一阶逻辑谓词为000元谓词时,就直接退化成了SAT问题.
