API Reference¶

`paramita.io` module¶

load_cnf ¶

load_cnf(filename, container, strict=True)

Read a CNF from a file into a CnfContainer.

Read a CNF file in DIMACS format. This format defines a header line as p cnf <numvars> <numclauses> and then, line by line, the clauses that conform the formula as a sequence of integers separated by spaces with a '0' indicating the end of the clause. A minus means that the literal is a negated variable. The absolute value of each integer refers to a unique variable.

This reader supports reading files in the following formats:

Plain text.
Compressed using GZIP, ZSTD, XZ, and BZIP2.

Setting strict mode to false disables the following checks:

Check for duplicated literals
Check for opposite literals
Check for a header
Check for a valid header

Parameters:

Name	Type	Description	Default
`filename`	`str \| PathLike`	The path to the instance. Compressed instances are supported.	required
`container`	`ClauseContainer`	The container where the clauses will be added to.	required
`strict`	`bool`	Verify that the loaded formula conforms to the DIMACS format.	`True`

load_wcnf ¶

load_wcnf(filename, container, strict=True)

Read a WCNF from a file into a WClauseContainer.

Read a WCNF file in DIMACS format. Two formats are accepted:

Original format

The original format is similar to the format for DIMACS CNF (see load_cnf). Initially, the file contains a text header indicating the number of variables, the number of clauses, and the top weight (interpreted as the weight for hard clauses). The header has this format: p wcnf ${nvars} ${nclauses} ${maxweight}

After the header, the clauses that conform the formula are defined. For each clause, first we find an integer value defining the weight of the clause, and then a sequence of integers representing the literals separated by spaces, with the number '0' indicating the end of clause.

Note that a clause could span multiple lines if it does not end with '0'.

Each literal is represented by a numeric value, where its absolute value refers to a unique variable, and a minus means that the literal is the egation of that variable.

Lines starting by the character c are treated as comments.

An example of a formula is:

c below are two hard clauses:
p wcnf 2 3 2
2 1 2 0
2 -1 0
c and a soft clause with weight 1:
1 -2 0

Revised format

The revised format removes the p line, and instead of marking the hard clauses with the max weight, now they use the character h as the weight.

The previous formula would be written as:

c below are two hard clauses:
h 1 2 0
h -1 0
c and a soft clause with weight 1:
1 -2 0

This reader supports reading files in the following formats:

Plain text.
Compressed using GZIP, ZSTD, XZ, and BZIP2.

Setting strict mode to false disables the following checks:

Check for duplicated literals
Check for opposite literals
Check for a header
Check for a valid header

Parameters:

Name	Type	Description	Default
`filename`	`str \| PathLike`	The path to the instance. Compressed instances are supported.	required
`container`	`WClauseContainer`	The container where the clauses will be added to.	required
`strict`	`bool`	Verify that the loaded formula conforms to the DIMACS format.	`True`

write_cnf ¶

write_cnf(formula, filepath, compression=CompressionFormat.NONE)

write_wcnf ¶

write_wcnf(formula, filepath, compression=CompressionFormat.NONE, format='revised')

CompressionFormat ¶

Bases: Enum