可满足式(satisfiable)是一个数学公式,设A为任一命题公式,若A在各种真值指派下至少存在一组成真指派,则A是可满足式,反之为矛盾式。

换言之,对于命题公式A,若A不是矛盾式,则称A是可满足式