Manipulating CNF/WCNF formulas¶

This guide shows how to work directly with formulas in Conjunctive Normal Form (CNF) and Weighted CNF (WCNF) using Paramita. You will learn how to create formulas from scratch, load them from files, add clauses, and save them.

CNF formulas¶

Start by creating an empty CNF formula. In Paramita, you use the CnfFormula class:

from paramita.containers import CnfFormula

f = CnfFormula()

Variables are represented by positive integers (1, 2, 3, …). A literal is an integer: positive for the variable, negative for its negation. For example, literal 1 means variable 1 is true, -1 means variable 1 is false. To add a clause, use add_clause with a list of literals. For instance, the clause \(\{x_1, \neg x2, x3\}\) becomes [1, -2, 3]:

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

You can add multiple clauses at once too:

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

For compatibility with IPASIR, there is also a literal‑by‑literal method: call add_lit for each literal and finish the clause with 0. This is useful when building clauses incrementally.

Warning

This method is optional, and it is not implemented for CnfFormula. However, you might find that some SAT solvers do implement it (see this other section).

To inspect the formula, use num_clauses and max_var. The former returns the number of clauses (after any internal simplifications), the latter the largest variable index used.

print(f.num_clauses())
print(f.max_var())

You can retrieve all clauses as a list of lists with clauses:

all_clauses = f.clauses()
print(all_clauses)  # e.g., [[1, -2, 3], [1, 2], ...]

If you have a candidate assignment (where positive numbers represent variables assigned to True, and negative ones assigned to False), you can check whether it satisfies the formula using is_feasible:

assignment = [1, -2, 3]
result = f.is_feasible(assignment)  # True, False, or None if partial

WCNF formulas¶

Paramita also supports weighted CNF formulas, where some clauses are soft (have a weight) and others are hard. Weighted formulas are used for MaxSAT problems. Use the WcnfFormula class:

from paramita.containers import WcnfFormula

wf = WcnfFormula()

Hard clauses can be added with a special weight SPECIAL_WEIGHTS.TOP_WEIGHT, or by omitting the weight. Soft clauses require a weight value.

from paramita.containers import SPECIAL_WEIGHTS

# Hard clauses
wf.add_clause([1, -2], SPECIAL_WEIGHTS.TOP_WEIGHT)
wf.add_clause([-3, 2])

# Soft clause with weight 5
wf.add_clause([-3], 5)

Writing from and to files¶

Once you have a formula, you will often want to read or write DIMACS files. Paramita provides load_cnf and write_cnf for plain CNF, and load_wcnf and write_wcnf for weighted CNF. All of them support compressed files (gzip, zstd, xz, bz2) automatically.

To load a CNF file you can use:

from paramita.io import load_cnf

f = CnfFormula()
load_cnf("problem.cnf", f)

Compression formats will be detected automatically by their magic bytes.

Note

Loading a formula is not something specific of a CnfFormula. We can use any class that implements the ClauseContainer interface (for example, a SatSolver could be used here too, to load the formulas directly to the solver).

To write a cnf to a file:

from paramita.io import write_cnf, CompressionFormat

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

For weighted CNF, use load_wcnf and write_wcnf. The loader automatically detects both the original and the revised formats. Writing defaults to the revised format, which is recommended, but you can use format="original" if needed.

from paramita.io import load_wcnf, write_wcnf

wf = WcnfFormula()
load_wcnf("maxsat.wcnf", wf)

write_wcnf(wf, "output.wcnf")
write_wcnf(wf, "output_original.wcnf", format='original')
write_wcnf(wf, "output.wcnf.gz", compression=CompressionFormat.GZIP)

Next steps¶

Now you have seen how to start manipulating raw CNF and WCNF formulas.

You can follow up by learning how to use SAT solvers and MaxSAT solvers.