Skip to content

Loading and writing CNF/WCNF files

This guide shows you how to read and write DIMACS CNF and weighted CNF (WCNF) files using Paramita. You will learn how to load formulas from disk into containers (e.g., CnfFormula, SatSolver, WcnfFormula, MaxSatSolver...), and how to save formulas back to files.

Prerequisites

Loading a CNF file

Use load_cnf to read a DIMACS CNF file into any object that implements the ClauseContainer interface:

from paramita.containers import CnfFormula
from paramita.io import load_cnf
from paramita.solvers import SatSolver

f = CnfFormula()

load_cnf("problem.cnf", f)

s = SatSolver.from_name("Cadical300")
load_cnf("problem.cnf", s)

Reading a formula in a compressed format is also supported:

f = CnfFormula()

load_cnf("problem.cnf.zst", f)

s = SatSolver.from_name("Cadical300")
load_cnf("problem.cnf.zst", s)

Currently, Paramita supports files compressed in BZ2, XZ, ZSTD, and GZIP for all python versions.

Note

The compression format is detected using magic bytes instead of the extension.

Loading a WCNF file

Use load_wcnf to read a DIMACS WCNF file into any object that implements the WClauseContainer interface:

from paramita.containers import WcnfFormula
from paramita.io import load_wcnf
from paramita.solvers import MaxSatSolver

f = WcnfFormula()

load_wcnf("problem.wcnf", f)

s = MaxSatSolver.from_name("EvalMaxSAT2022")
load_wcnf("problem.wcnf", s)

load_wcnf also supports the compressed formats explained for load_cnf.

Paramita also detects automatically the format for WCNF:

  • Original format: header line p wcnf <nvars> <nclauses> <topweight>; hard clauses use <topweight> as weight.
  • Revised format: no header; hard clauses use h as weight. This is the recommended format.

Writing a CNF file

Use write_cnf to create a DIMACS CNF file from the clauses in a CnfFormula.

from paramita.io import write_cnf, CompressionFormat

f = CnfFormula()
f.add_clauses([
    [1, 2],
    [-1, -3],
    [2, 3]
])

write_cnf(f, "output.cnf")

You can also specify the compression format (one of NONE, GZIP, ZSTD, XZ, BZIP2, by default is NONE): 

write_cnf(f, "output.cnf.gz", compression=CompressionFormat.GZIP)

Writing a WCNF file

Use write_wcnf to create a DIMACS WCNF file from the clauses in a WcnfFormula.

from paramita.io import write_wcnf, CompressionFormat

f = WcnfFormula()
f.add_clause([1, 2, 3], 1)
f.add_clause([-1, -2], 3)
f.add_clause([-3], 2)
f.add_clause([1, -2])

# Revised format (recommended)
write_wcnf(f, "output.wcnf")

# Original format (with top weight header)
write_wcnf(f, "output_original.wcnf", format="original")

# Compressed output
write_wcnf(f, "output.wcnf.gz", compression=CompressionFormat.GZIP)

Next steps