write_cnf(file,
clause_generators,
hard_clause_cost=None,
comments=True)
| source code
|
Write a CNF file using the provided clause_generators
Ideally the cost of a hard clause is +infinity, but ... If the cost of
hard clauses is too high then an assignment with an overflowing total
cost may be produced, possibly confusing a SAT solver. If it is too low,
then an assignment which breaks a hard clause may be optimal.
The default is to set it to x such that cost_of_soft_clauses * x|hard
clauses| = sys.maxint. Then even breaking all clauses will not give an
overflow. This is reasonable as long as the SAT solver will be running on
the same machine as this Python process. If this value of x is below the
cost of a soft clause an error is raised.
This method returns the tuple (atom_ids, inv_atom_ids, extra_cost).
atom_ids is a dictionary mapping logical ground atoms to the integers
representing them inv_atom_ids is the inverse of atom_ids. It is a list
(note that inv_atom_ids[0]=None, since 0 is never used to represent an
atom in WCNF files.) extra_cost is the total cost of all soft empty
clauses which (ideally) would be in the WCNF file. Such clauses are
not written to the WCNF file since solvers (eg UBCSAT) don't like
them. This cost should be added to the cost of any assigment found by a
SAT solver.
- Parameters:
file (Writable file object) - Where to write the WCNF fileclause_generators (Sequence) - Sequence of clause generator iterators. For example,
clause_generators = (
probadg.clauses_justorder(float_weights=True),
probadg.clauses_no3cycles()) is a valid choice, where
probadg is a RandomGraphs.RandomADG object.hard_clause_cost (Number of None) - The cost of breaking a 'hard' clause. If None a
suitable value is computed internally.comments (Boolean) - Whether to include comments in the generated WCNF stating what
the atoms and clauses mean - Returns: Tuple
- atom_ids, inv_atom_ids, extra_cost (see above)
- Raises:
RuntimeError - If a hard empty clause is generated. (Such a clause can never be
satisfied.)ValueError - If soft clauses have such high costs that a sensible hard clause
cost cannot be chosen.
|