Package operations_research.sat
package operations_research.sat
-
ClassDescriptionA list of clauses to delete.A list of clauses to delete.A clause to export, so that it can be imported from any worker.A clause to export, so that it can be imported from any worker.A clause imported from the input problem, or from another worker.A clause imported from the input problem, or from another worker.An LRAT inferred clause.An LRAT inferred clause.If `rat_infos` is empty, the last `unit_ids` clause must become empty after unit propagation.If `rat_infos` is empty, the last `unit_ids` clause must become empty after unit propagation.An LRAT UNSAT proof is a sequence of steps, starting from imported clauses and ending with the empty clause.An LRAT UNSAT proof is a sequence of steps, starting from imported clauses and ending with the empty clause.