SAT解算器 :robot: 为了使用SAT求解器,您需要导入sat_solver.sat_engine ,然后调用其中定义了公式的函数solve_sat(formula) ,如下所示 原子命题应为'p'...'z'中的字母,并可选地后面跟数字序列。 例如:“ p”,“ y12”,“ z035”。 可以有“ T”和“ F”(分别为True和False)。 〜φ其中,φ是有效的命题公式。 '(φ&ψ)',其中φ和ψ均为有效命题公式。 '(φ|ψ)',其中φ和ψ均为有效命题公式。 '(φ->ψ)',其中φ和ψ均为有效的命题公式。 例子: from sat_solver.sat_eng