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