Other CSP Formats# DIMACS# The DIMACS format is used to encode boolean satisfiability problems in conjunctive normal form. CNF# load_cnf(fp) Load a constraint satisfaction problem from a .cnf file.