3.1.4. cnfgen.families.ordering module

Implementation of the ordering principle formulas

GraphOrderingPrinciple(graph, total=False, smart=False, plant=False, knuth=0)

Generates the clauses for graph ordering principle

Arguments: - graph : undirected graph - total : add totality axioms (i.e. “x < y” or “x > y”) - smart : “x < y” and “x > y” are represented by a single variable (implies total) - plant : allow last element to be minimum (and could make the formula SAT) - knuth : Don Knuth variants 2 or 3 of the formula (anything else suppress it)

OrderingPrinciple(size, total=False, smart=False, plant=False, knuth=0)

Generates the clauses for ordering principle

Arguments: - size : size of the domain - total : add totality axioms (i.e. “x < y” or “x > y”) - smart : “x < y” and “x > y” are represented by a single variable (implies totality) - plant : allow a single element to be minimum (could make the formula SAT) - knuth : Donald Knuth variant of the formula ver. 2 or 3 (anything else suppress it)