logic#
嵌套逻辑表达式的基本思想是，与其尝试通过分布来消除嵌套，不如添加新变量。因此，如果我们有一些逻辑表达式 expr，我们用 x 替换它，并将 expr <-> x 添加到子句中，其中 x 是一个新变量，expr <-> x 以相同的方式递归评估，以便最终子句是原子的 ORs。
要使用此功能，请使用最大变量创建一个新的 Clauses 对象，例如，如果您已经有 [[1, 2, -3]]，您将使用 C = Clause(3)。所有函数都返回一个新的文字，它代表该函数，或者如果表达式可以完全解析，则返回 True 或 False。它们还可以向 C.clauses 添加新的子句，然后将其传递给 SAT 求解器。
所有函数都将原子作为参数（原子是一个整数，表示一个文字或一个否定文字，或布尔常量 True 或 False；也就是说，调用者有责任递归地转换表达式。这样做是因为我们没有表示各种逻辑类的数据结构，只有原子。
如果您知道正在使用的文字将仅在肯定或否定中使用（例如，您将仅使用 x，而不是 -x），则可以将极性参数设置为 True 或 False。这将生成更少的子句。如果您不直接利用此优势，而是通过 Require 和 Prevent 函数，则可能是最好的。
类#
函数#
|
给定一组子句，找到一个最小的不可满足子集（一个 |
属性#
- TRUE#
- FALSE#
- PycoSatSolver = 'pycosat'#
- PyCryptoSatSolver = 'pycryptosat'#
- PySatSolver = 'pysat'#
- class Clauses(m=0, sat_solver=PycoSatSolver)#
- property m#
- property unsat#
- get_clause_count()#
- as_list()#
- _check_variable(variable)#
- _check_literal(literal)#
- add_clause(clause)#
- add_clauses(clauses)#
- name_var(m, name)#
- new_var(name=None)#
- from_name(name)#
- from_index(m)#
- _assign(vals, name=None)#
- _convert(x)#
- _eval(func, args, no_literal_args, polarity, name)#
- Prevent(what, *args)#
- Require(what, *args)#
- Not(x, polarity=None, name=None)#
- And(f, g, polarity=None, name=None)#
- Or(f, g, polarity=None, name=None)#
- Xor(f, g, polarity=None, name=None)#
- ITE(c, t, f, polarity=None, name=None)#
如果 c 则 t 否则 f。
在此函数中，如果 c、t 或 f 中的任何一个是 True 和 False，则结果表达式将被解析。
- All(iter, polarity=None, name=None)#
- Any(vals, polarity=None, name=None)#
- AtMostOne_NSQ(vals, polarity=None, name=None)#
- AtMostOne_BDD(vals, polarity=None, name=None)#
- AtMostOne(vals, polarity=None, name=None)#
- ExactlyOne_NSQ(vals, polarity=None, name=None)#
- ExactlyOne_BDD(vals, polarity=None, name=None)#
- ExactlyOne(vals, polarity=None, name=None)#
- LinearBound(equation, lo, hi, preprocess=True, polarity=None, name=None)#
- sat(additional=None, includeIf=False, names=False, limit=0)#
计算当前子句集的 SAT 解。
返回的是这些解的列表。当子句不可满足时，将返回一个空列表。
- itersolve(constraints=None, m=None)#
- minimize(objective, bestsol=None, trymax=False)#
- minimal_unsatisfiable_subset(clauses, sat, explicit_specs)#
给定一组子句，找到一个最小的不可满足子集（一个不可满足核心）
如果不存在真子集是不可满足的，则集合是最小的不可满足子集。一组子句可能具有许多不同大小的最小不可满足子集。
sat 应该是一个函数，它接受一个子句元组，如果子句是可满足的则返回 True，如果不可满足则返回 False。该算法将适用于任何反向排序函数（反转子集顺序和顺序 False < True），即，任何函数，其中 (A <= B) iff (sat(B) <= sat(A))，其中 A <= B 表示 A 是 B 的子集，False < True）。