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