3.1.4. cnfformula.families.ordering module

Implementation of the ordering principle formulas

class GOPCmdHelper

Bases: object

Command line helper for Graph Ordering principle formulas

Methods

build_cnf(args)	Build a Graph ordering principle formula according to the arguments
setup_command_line(parser)	Setup the command line options for Graph ordering principle formula

static build_cnf(args)

Build a Graph ordering principle formula according to the arguments

Arguments: - args: command line options

description = 'graph ordering principle'

name = 'gop'

static setup_command_line(parser)

Setup the command line options for Graph ordering principle formula

Arguments: - parser: parser to load with options.

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)

class OPCmdHelper

Bases: object

Command line helper for Ordering principle formulas

Methods

build_cnf(args)	Build an Ordering principle formula according to the arguments
setup_command_line(parser)	Setup the command line options for Ordering principle formula

static build_cnf(args)

Build an Ordering principle formula according to the arguments

Arguments: - args: command line options

description = 'ordering principle'

name = 'op'

static setup_command_line(parser)

Setup the command line options for Ordering principle formula

Arguments: - parser: parser to load with options.

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)

varname(v1, v2)