`_logic`#

类#

`_ClauseList`	CNF 子句的存储，表示为整数元组的列表。
`_ClauseArray`	CNF 子句的存储，表示为扁平的整数数组。
`_SatSolver`	调用 SAT 求解器的简单包装器，给定 _ClauseList/_ClauseArray 实例。
`_PycoSatSolver`	调用 SAT 求解器的简单包装器，给定 _ClauseList/_ClauseArray 实例。
`_PyCryptoSatSolver`	调用 SAT 求解器的简单包装器，给定 _ClauseList/_ClauseArray 实例。
`_PySatSolver`	调用 SAT 求解器的简单包装器，给定 _ClauseList/_ClauseArray 实例。
`子句`

属性#

`TRUE`
`FALSE`
`_sat_solver_str_to_cls`
`_sat_solver_cls_to_str`

TRUE#

FALSE#

class _ClauseList#

CNF 子句的存储，表示为整数元组的列表。

get_clause_count()#: 返回存储的子句数量。

save_state()#: 获取状态信息，以便能够恢复临时添加的补充子句。_ClauseList：状态仅仅是子句的数量。

restore_state(saved_state)#: 恢复通过 save_state 保存的状态。移除在状态保存后添加的子句。

as_list()#: 将子句作为整数元组的列表返回。

as_array()#: 将子句作为扁平的整数数组返回，每个子句以 0 结尾。

class _ClauseArray#

CNF 子句的存储，表示为扁平的整数数组。每个子句以 int(0) 结尾。

extend(clauses)#

append(clause)#

get_clause_count()#: 返回存储的子句数量。这是一个 O(n) 操作，因为我们没有显式存储子句的数量，这出于性能原因（Python 解释器在 self.append 中的开销）。

save_state()#: 获取状态信息，以便能够恢复临时添加的补充子句。_ClauseArray：状态是整数数组的长度，而不是子句的数量。

restore_state(saved_state)#: 恢复通过 save_state 保存的状态。移除在状态保存后添加的子句。

as_list()#: 将子句作为整数元组的列表返回。

as_array()#: 将子句作为扁平的整数数组返回，每个子句以 0 结尾。

class _SatSolver(**run_kwargs)#

调用 SAT 求解器的简单包装器，给定 _ClauseList/_ClauseArray 实例。

get_clause_count()#

as_list()#

save_state()#

restore_state(saved_state)#

run(m, **kwargs)#

abstract setup(m, **kwargs)#: 创建求解器实例，将子句添加到其中，并返回它。

abstract invoke(solver)#: 启动实际的 SAT 求解并返回计算出的解。

abstract process_solution(sat_solution)#: 处理 self.invoke 返回的解。如果未找到解，则返回满足变量的列表或 None。

class _PycoSatSolver(**run_kwargs)#

基类： _SatSolver

调用 SAT 求解器的简单包装器，给定 _ClauseList/_ClauseArray 实例。

setup(m, limit=0, **kwargs)#: 创建求解器实例，将子句添加到其中，并返回它。

invoke(iter_sol)#: 启动实际的 SAT 求解并返回计算出的解。

process_solution(sat_solution)#: 处理 self.invoke 返回的解。如果未找到解，则返回满足变量的列表或 None。

class _PyCryptoSatSolver(**run_kwargs)#

基类： _SatSolver

调用 SAT 求解器的简单包装器，给定 _ClauseList/_ClauseArray 实例。

setup(m, threads=1, **kwargs)#: 创建求解器实例，将子句添加到其中，并返回它。

invoke(solver)#: 启动实际的 SAT 求解并返回计算出的解。

process_solution(solution)#: 处理 self.invoke 返回的解。如果未找到解，则返回满足变量的列表或 None。

class _PySatSolver(**run_kwargs)#

基类： _SatSolver

调用 SAT 求解器的简单包装器，给定 _ClauseList/_ClauseArray 实例。

setup(m, **kwargs)#: 创建求解器实例，将子句添加到其中，并返回它。

invoke(solver)#: 启动实际的 SAT 求解并返回计算出的解。

process_solution(sat_solution)#: 处理 self.invoke 返回的解。如果未找到解，则返回满足变量的列表或 None。

_sat_solver_str_to_cls#

_sat_solver_cls_to_str#

class Clauses(m=0, sat_solver_str=_sat_solver_cls_to_str[_PycoSatSolver])#

get_clause_count()#

as_list()#

new_var()#

assign(vals)#

Combine(args, polarity)#

Eval(func, args, polarity)#

Prevent(func, *args)#

Require(func, *args)#

Not(x, polarity=None, add_new_clauses=False)#

And(f, g, polarity, add_new_clauses=False)#

Or(f, g, polarity, add_new_clauses=False)#

Xor(f, g, polarity, add_new_clauses=False)#

ITE(c, t, f, polarity, add_new_clauses=False)#

All(iter, polarity=None)#

Any(iter, polarity)#

AtMostOne_NSQ(vals, polarity)#

AtMostOne_BDD(vals, polarity=None)#

ExactlyOne_NSQ(vals, polarity)#

ExactlyOne_BDD(vals, polarity)#

LB_Preprocess(lits, coeffs)#

BDD(lits, coeffs, nterms, lo, hi, polarity)#

LinearBound(lits, coeffs, lo, hi, preprocess, polarity)#

_run_sat(m, limit=0)#

sat(additional=None, includeIf=False, limit=0)#

Calculate a SAT solution for the current clause set.

Returned is the list of those solutions. When the clauses are unsatisfiable, an empty list is returned.

minimize(lits, coeffs, bestsol=None, trymax=False)#: Minimize the objective function given by (coeff, integer) pairs in zip(coeffs, lits). The actual minimization is multiobjective: first, we minimize the largest active coefficient value, then we minimize the sum.

_logic#

类#

属性#

`_logic`#