Encoding Module

This module for defining the encoding of some Problem. In essence, this module is a wrapper over the formula module of the pysat library, providing the lazy initialization feature. It also provides a feature to cache initialized object for the executing process.

Encoding

Module interface for determining the Problem encoding. It has one inherited method: get_formula(…), which should return an instance of the corresponding formula.
class lib_satprob.encoding.Encoding()
Base Encoding class constructor haven’t any arguments.
get_formula(copy)
This method returns instance of encoding formula.
Input arguments:

  • copy (Optional[bool]) - a flag to return a copy of pysat formula instance instead of original lazily created instance.

Return type: Any (defined in a specific implementation).

Clause

An alias for the clause type.
type lib_satprob.encoding.Clause = List[int]

CNF

Module implementation for encodings in conjunctive normal form (CNF). This class is a wrapper over the pysat.formula.CNF class.
class lib_satprob.encoding.CNF(from_file=None: str, from_string=None: str, extract_hard=False: bool, from_clauses=None: List[Clause], comment_lead=['c']: List[str])
Init arguments:

  • from_file (Optional[str]) - a path to the file containing CNF in DIMACS format. This argument involves lazily creation by reading from the given file. Default: None.

  • from_string (Optional[str]) - a string with CNF in DIMACS format. Default: None.

  • extract_hard (Optional[bool]) - a flag to extract hard clauses from the WCNF encoding specified in the given file. Only works with the from_file argument. Default: False.

  • from_clauses (Optional[List[Clause]) - a list of clauses to bootstrap the formula with. Default: None.

  • comment_lead (Optional[List[str]) - a list of characters leading comment lines. Default: ['c'].

Important

To create a CNF instance specify only one initialization argument (from_file or from_string or from_clauses).

get_formula(copy)
Input arguments:

  • copy (Optional[bool]) - a flag to return a copy of pysat.formula.CNF instance instead of original lazily created instance.

Return type: pysat.formula.CNF

CNFPlus

Module implementation for CNF encodings augmented with native cardinality constraints. This class is a wrapper over the pysat.formula.CNFPlus class.
class lib_satprob.encoding.CNF(from_file=None: str, from_string=None: str, comment_lead=['c']: List[str])
Init arguments:

  • from_file (Optional[str]) - a path to the file containing CNF+ in DIMACS format. This argument involves lazily creation by reading from the given file. Default: None.

  • from_string (Optional[str]) - a string with CNF+ in DIMACS format. Default: None.

  • comment_lead (Optional[List[str]) - a list of characters leading comment lines. Default: ['c'].

Important

To create a CNFPlus instance specify only one initialization argument (from_file or from_string).

get_formula(copy)
Input arguments:

  • copy (Optional[bool]) - a flag to return a copy of pysat.formula.CNFPlus instance instead of original lazily created instance.

Return type: pysat.formula.CNFPlus

WCNF

Module implementation for partial (weighted) CNF encodings. This class is a wrapper over the pysat.formula.WCNF class.
class lib_satprob.encoding.WCNF(from_file=None: str, from_string=None: str, comment_lead=['c']: List[str])
Init arguments:

  • from_file (Optional[str]) - a path to the file containing WCNF in WDIMACS format. This argument involves lazily creation by reading from the given file. Default: None.

  • from_string (Optional[str]) - a string with WCNF in WDIMACS format. Default: None.

  • comment_lead (Optional[List[str]) - a list of characters leading comment lines. Default: ['c'].

Important

To create a WCNF instance specify only one initialization argument (from_file or from_string).

get_formula(copy)
Input arguments:

  • copy (Optional[bool]) - a flag to return a copy of pysat.formula.WCNF instance instead of original lazily created instance.

Return type: pysat.formula.WCNF

WCNFPlus

Module implementation for CNF encodings augmented with native cardinality constraints. This class is a wrapper over the pysat.formula.WCNFPlus class.
class lib_satprob.encoding.WCNFPlus(from_file=None: str, from_string=None: str, comment_lead=['c']: List[str])
Init arguments:

  • from_file (Optional[str]) - a path to the file containing WCNFPlus in WDIMACS format. This argument involves lazily creation by reading from the given file. Default: None.

  • from_string (Optional[str]) - a string with WCNFPlus in WDIMACS format. Default: None.

  • comment_lead (Optional[List[str]) - a list of characters leading comment lines. Default: ['c'].

Important

To create a WCNFPlus instance specify only one initialization argument (from_file or from_string).

get_formula(copy)
Input arguments:

  • copy (Optional[bool]) - a flag to return a copy of pysat.formula.WCNFPlus instance instead of original lazily created instance.

Return type: pysat.formula.WCNFPlus