Formula Loading utilities

OptiLog provides three functions to load Boolean formulas, load_cnf(), load_wcnf() and load_qcnf().

optilog.formulas.loaders.load_cnf(file_path, *args, **kwargs)

Loads a CNF DIMACS 1 into a optilog.formulas.CNF object and returns it. This method is particularly useful when working with big formulas because it is very performant.

Parameters

file_path (Union[str, Path]) – The path of a CNF in DIMACS format.

Return type

CNF

>>> from optilog.formulas.loaders import load_cnf
>>> cnf = load_cnf('example.cnf')

optilog.formulas.loaders.load_wcnf(file_path, *args, **kwargs)

Loads a WCNF DIMACS 2 into a optilog.formulas.WCNF object and returns it. This method is particularly useful when working with big formulas because it is very performant.

Parameters

file_path (Union[str, Path]) – The path of a CNF in DIMACS format.

Return type

WCNF

>>> from optilog.formulas.loaders import load_wcnf
>>> wcnf = load_wcnf('example.wcnf')

optilog.formulas.loaders.load_qcnf(file_path)

Loads a QCNF DIMACS 3 into a optilog.formulas.QCNF object and returns it.

Parameters

path – The path of a qcnf in DIMACS format.

Return type

QCNF

Footnotes

1

SAT solvers commonly use the DIMACS format for CNFs. This format is used by SAT competitions requirements as originally described in DIMACS CNF suggested format.

2

Solvers for weighted (partial) MaxSAT commonly use an extended DIMACS format for CNFs. In particular, this format adds weights to each clause and a way to specify hard constraints (for partial MaxSAT). This extended format is used and described by MaxSAT competitions requirements.

3

Based on the QDIMACS standard