战术有不同的目的。您可以创建一个包含您的断言/约束条件的目标,然后在目标上运行战术,其结果将是一组新的(子)目标,即新的断言/约束条件。求解器确定可满足性并不会产生新的(子)目标。战术可以转换为求解器,使得生成的求解器将运行战术,如果结果是明确的(平凡的sat/unsat),它将返回该结果。如果战术产生的子目标不确定,它将返回“未知”。