API

The specification of the Pindakaas API

class pindakaas.CNF

A representation for Boolean formulas in conjunctive normal form.

add_clause(clause)

Add a clause to the database.

Parameters:: clause (Iterable[Lit]) – An iterable of literals representing the clause to add
Raises:: Unsatisfiable – If the formula has become unsatisfiable

add_encoding(constraint, encoder=None, conditions=None)

Add an encoding of a constraint to the database.

Optionally, the constraint is implied by the given conditions (i.e. every: clause is extended by the conditions), and the given encoder is used for the encoding.

Parameters:

constraint (Formula) – The constraint or formula to encode and add to the database
encoder (Encoder | None)
conditions (Iterable[Lit] | None)

Raises:

Unsatisfiable – If the formula has become unsatisfiable

clauses()

Returns an iterator of the clauses currently included in the CNF.

Returns:: An iterable of lists of literals representing the clauses.
Return type:: Iterable[list[Lit]]

new_var_range(n)

Add a continuous range of n new variables to the database.

Parameters:: n (int) – The number of new variables
Returns:: The start and end of the range of the new variables (inclusive), given as literals.
Return type:: VarRange

to_dimacs()

Return a textual representation in the DIMACS format.

Returns:: The CNF as a DIMACS string
Return type:: str

variables()

Returns an iterator of the variables currently included in the CNF.

Returns:: An iterable of literals representing the variables.
Return type:: Iterable[Lit]

class pindakaas.ClauseDatabase

The abstract class to represent objects to which we can add clauses.

Examples of such classes include CNF, WCNF, and the various Solver: implementations.

abstractmethod add_clause(clause)

Add a clause to the database.

Parameters:: clause (Iterable[Lit]) – An iterable of literals representing the clause to add
Raises:: Unsatisfiable – If the formula has become unsatisfiable

add_encoding(constraint, encoder=None, conditions=None)

Add an encoding of a constraint to the database.

Optionally, the constraint is implied by the given conditions (i.e. every: clause is extended by the conditions), and the given encoder is used for the encoding.

Parameters:

constraint (Formula) – The constraint or formula to encode and add to the database
encoder (Encoder | None)
conditions (Iterable[Lit] | None)

Raises:

Unsatisfiable – If the formula has become unsatisfiable

new_var(): Add a new variable to the database.

abstractmethod new_var_range(n)

Add a continuous range of n new variables to the database.

Parameters:: n (int) – The number of new variables
Returns:: The start and end of the range of the new variables (inclusive), given as literals.
Return type:: VarRange

new_vars(n)

Add n new variables to the database.

Parameters:: n (int) – The number of new variables
Returns:: The new variables returned as literals
Return type:: Iterable[Lit]

pindakaas.Constraint: alias of Formula

class pindakaas.Encoder

Method used to encode a constraint.

Warning: Not all encoders can be used to encode each type of constraint. If an invalid encoder is selected, then an InvalidEncoder exception will be raised.

ADDER = Encoder.ADDER

BITWISE = Encoder.BITWISE

DECISION_DIAGRAM = Encoder.DECISION_DIAGRAM

LADDER = Encoder.LADDER

PAIRWISE = Encoder.PAIRWISE

SORTED_WEIGHT_COUNTER = Encoder.SORTED_WEIGHT_COUNTER

SORTING_NETWORK = Encoder.SORTING_NETWORK

TOTALIZER = Encoder.TOTALIZER

TSEITIN = Encoder.TSEITIN

class pindakaas.Formula: A propositional logic formula.

exception pindakaas.InvalidEncoder: Raised when the chosen encoder does not support the constraint (e.g. when the PairwiseEncoder encoder for AMO constraints is used to encode a PB constraint).

class pindakaas.Lit

A Boolean literal, representing a Boolean variable or its negation.

static from_raw(value)

is_negated(): Return whether the variable is negated

var(): Return the literal’s variable

exception pindakaas.Unsatisfiable: Raised when the given constraint is found to be Unsatisfiable during encoding.

class pindakaas.WCNF

A representation for conjunctive normal form with weighted clauses.

Note that WCNF.clauses only iterates over the hard clauses. Use WCNF.weighted_clauses to iterate over all clauses.

add_weighted_clause(clause, weight)

Add a weighted clause to the database.

Parameters:

clause (Iterable[Lit]) – An iterable of literals representing the clause to add
weight (int) – the weight of the clause

weighted_clauses()

Returns an iterator of the weighted clauses currently included in the WCNF.

Returns:: An iterable of lists of literals representing the clauses.
Return type:: Iterable[tuple[int | None, list[Lit]]]

A module containing solvers and solving related classes.

class pindakaas.solver.CaDiCaL

The CaDiCaL SAT solver.

add_clause(clause)

Add a clause to the database.

Parameters:: clause (Iterable[Lit]) – An iterable of literals representing the clause to add
Raises:: Unsatisfiable – If the formula has become unsatisfiable

add_encoding(constraint, encoder=None, conditions=None)

Add an encoding of a constraint to the database.

Optionally, the constraint is implied by the given conditions (i.e. every: clause is extended by the conditions), and the given encoder is used for the encoding.

Parameters:

constraint (Formula) – The constraint or formula to encode and add to the database
encoder (Encoder | None)
conditions (Iterable[Lit] | None)

Raises:

Unsatisfiable – If the formula has become unsatisfiable

new_var_range(n)

Add a continuous range of n new variables to the database.

Parameters:: n (int) – The number of new variables
Returns:: The start and end of the range of the new variables (inclusive), given as literals.

class pindakaas.solver.CaDiCaLInner

add_clause(clause)

add_encoding(con, enc, conditions)

new_var_range(num_vars)

set_time_limit(limit)

solve_assuming(assumptions)

class pindakaas.solver.Kissat

The Kissat SAT solver.

add_clause(clause)

Add a clause to the database.

Parameters:: clause (Iterable[Lit]) – An iterable of literals representing the clause to add
Raises:: Unsatisfiable – If the formula has become unsatisfiable

add_encoding(constraint, encoder=None, conditions=None)

Add an encoding of a constraint to the database.

Optionally, the constraint is implied by the given conditions (i.e. every: clause is extended by the conditions), and the given encoder is used for the encoding.

Parameters:

constraint (Formula) – The constraint or formula to encode and add to the database
encoder (Encoder | None)
conditions (Iterable[Lit] | None)

Raises:

Unsatisfiable – If the formula has become unsatisfiable

new_var_range(n)

Add a continuous range of n new variables to the database.

Parameters:: n (int) – The number of new variables
Returns:: The start and end of the range of the new variables (inclusive), given as literals.

class pindakaas.solver.KissatInner

add_clause(clause)

add_encoding(con, enc, conditions)

new_var_range(num_vars)

set_time_limit(limit)

solve_assuming(assumptions)

class pindakaas.solver.Result

The Result object returned after calling solve().

It gives access to e.g. solver status and the values of variables.

abstractmethod failed(lit)

Check if the given assumption literal was used to prove the unsatisfiability.

The unsatisfiability of the formula is under the assumptions used for the last SAT search. Note also that for literals lit which are not assumption literals, the behavior of is not specified.

Parameters:: lit (Lit) – the assumption literal for which to return whether it contributed to the unsatisfiable result
Returns:: whether lit contributed to the unsatisfiable result
Return type:: bool | None

abstract property status: Status: Return result from solving the database.

abstractmethod value(lit)

Return value for literal lit, or None if lit is assigned.

Parameters:: lit (Lit) – the literal for which to return the value
Returns:: the value of lit if assigned
Return type:: bool | None

class pindakaas.solver.Solver

An abstract class which extends a ClauseDatabase with solving capabilities.

solve(assumptions=None, time_limit=None)

Solve the current ClauseDatabase.

Parameters:

assumptions (Iterable[Lit] | None) – an optional iterable of assumptions literals which must hold for this solve call
time_limit (timedelta | None) – an optional time limit before which the solver is terminated and the result is Unknown

Return type:

Iterator[Result]

class pindakaas.solver.Status

The resulting status of solving a problem.

SATISFIED = Status.SATISFIED

UNKNOWN = Status.UNKNOWN

UNSATISFIABLE = Status.UNSATISFIABLE