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