原子集A：
　　为研究子句集S中的不可满足性，需要讨论H域上S中各谓词的真值。这里原子集A为公式中出现的谓词套上H域的元素组成的集合。