`_logic`#

Classes#

`_ClauseList`	Storage for the CNF clauses, represented as a list of tuples of ints.
`_ClauseArray`	Storage for the CNF clauses, represented as a flat int array.
`_SatSolver`	Simple wrapper to call a SAT solver given a _ClauseList/_ClauseArray instance.
`_PycoSatSolver`	Simple wrapper to call a SAT solver given a _ClauseList/_ClauseArray instance.
`_PyCryptoSatSolver`	Simple wrapper to call a SAT solver given a _ClauseList/_ClauseArray instance.
`_PySatSolver`	Simple wrapper to call a SAT solver given a _ClauseList/_ClauseArray instance.
`Clauses`

Attributes#

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

TRUE#

FALSE#

class _ClauseList#

Storage for the CNF clauses, represented as a list of tuples of ints.

get_clause_count()#: Return number of stored clauses.

save_state()#: Get state information to be able to revert temporary additions of supplementary clauses. _ClauseList: state is simply the number of clauses.

restore_state(saved_state)#: Restore state saved via save_state. Removes clauses that were added after the state has been saved.

as_list()#: Return clauses as a list of tuples of ints.

as_array()#: Return clauses as a flat int array, each clause being terminated by 0.

class _ClauseArray#

Storage for the CNF clauses, represented as a flat int array. Each clause is terminated by int(0).

extend(clauses)#

append(clause)#

get_clause_count()#: Return number of stored clauses. This is an O(n) operation since we don't store the number of clauses explicitly due to performance reasons (Python interpreter overhead in self.append).

save_state()#: Get state information to be able to revert temporary additions of supplementary clauses. _ClauseArray: state is the length of the int array, NOT number of clauses.

restore_state(saved_state)#: Restore state saved via save_state. Removes clauses that were added after the state has been saved.

as_list()#: Return clauses as a list of tuples of ints.

as_array()#: Return clauses as a flat int array, each clause being terminated by 0.

class _SatSolver(**run_kwargs)#

Simple wrapper to call a SAT solver given a _ClauseList/_ClauseArray instance.

get_clause_count()#

as_list()#

save_state()#

restore_state(saved_state)#

run(m, **kwargs)#

abstract setup(m, **kwargs)#: Create a solver instance, add the clauses to it, and return it.

abstract invoke(solver)#: Start the actual SAT solving and return the calculated solution.

abstract process_solution(sat_solution)#: Process the solution returned by self.invoke. Returns a list of satisfied variables or None if no solution is found.

class _PycoSatSolver(**run_kwargs)#

Bases: _SatSolver

Simple wrapper to call a SAT solver given a _ClauseList/_ClauseArray instance.

setup(m, limit=0, **kwargs)#: Create a solver instance, add the clauses to it, and return it.

invoke(iter_sol)#: Start the actual SAT solving and return the calculated solution.

process_solution(sat_solution)#: Process the solution returned by self.invoke. Returns a list of satisfied variables or None if no solution is found.

class _PyCryptoSatSolver(**run_kwargs)#

Bases: _SatSolver

Simple wrapper to call a SAT solver given a _ClauseList/_ClauseArray instance.

setup(m, threads=1, **kwargs)#: Create a solver instance, add the clauses to it, and return it.

invoke(solver)#: Start the actual SAT solving and return the calculated solution.

process_solution(solution)#: Process the solution returned by self.invoke. Returns a list of satisfied variables or None if no solution is found.

class _PySatSolver(**run_kwargs)#

Bases: _SatSolver

Simple wrapper to call a SAT solver given a _ClauseList/_ClauseArray instance.

setup(m, **kwargs)#: Create a solver instance, add the clauses to it, and return it.

invoke(solver)#: Start the actual SAT solving and return the calculated solution.

process_solution(sat_solution)#: Process the solution returned by self.invoke. Returns a list of satisfied variables or None if no solution is found.

_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#

Classes#

Attributes#

`_logic`#