CNFgen
stable
Table of contents
Welcome to CNFgen’s documentation!
1. How to build and use a CNF
2. Testing satisfiability
3. Formula families
4. Graph based formulas
5. Post-process a CNF formula
6. The command line utility
7. Adding a formula family to CNFgen
CNFgen
Docs
»
Index
Edit on GitHub
Index
A
|
B
|
C
|
D
|
E
|
F
|
G
|
H
|
I
|
K
|
L
|
M
|
N
|
O
|
P
|
R
|
S
|
T
|
V
|
W
|
X
A
add_clause() (CNF method)
,
[1]
add_clause_unsafe() (CNF method)
,
[1]
add_variable() (CNF method)
,
[1]
all_clauses() (in module cnfformula.families.randomformulas)
AllEqualsSubstitutionCmd (class in cnfformula.transformations.substitutions)
AllEqualSubstitution (class in cnfformula)
(class in cnfformula.transformations.substitutions)
AND (class in cnfformula.families.simple)
B
BaseSubstitution (class in cnfformula.transformations.substitutions)
BinaryCliqueFormula() (in module cnfformula)
(in module cnfformula.families.subgraph)
BinaryKCliqueCmdHelper (class in cnfformula.families.subgraph)
BinaryPigeonholePrinciple() (in module cnfformula)
(in module cnfformula.families.pigeonhole)
bipartite_random_left_regular() (in module cnfformula.graphs)
bipartite_random_regular() (in module cnfformula.graphs)
bipartite_sets() (in module cnfformula.graphs)
BipartiteGraphHelper (class in cnfformula.cmdline)
Bits (CNF.binary_mapping attribute)
,
[1]
bitstring_to_image() (CNF.binary_mapping method)
,
[1]
BPHPCmdHelper (class in cnfformula.families.pigeonhole)
build_cnf() (AND static method)
(BPHPCmdHelper static method)
(BinaryKCliqueCmdHelper static method)
(CliqueColoringCmdHelper static method)
(CountingCmdHelper static method)
(DominatingSetCmdHelper static method)
(ECCmdHelper static method)
(EMPTY static method)
(EMPTY_CLAUSE static method)
(GAutoCmdHelper static method)
(GIsoCmdHelper static method)
(GOPCmdHelper static method)
(GPHPCmdHelper static method)
(KCliqueCmdHelper static method)
(KColorCmdHelper static method)
(OPCmdHelper static method)
(OR static method)
(PHPCmdHelper static method)
(PMatchingCmdHelper static method)
(PTNCmdHelper static method)
(ParityCmdHelper static method)
(PebblingCmdHelper static method)
(RWCmdHelper static method)
(RamseyCmdHelper static method)
(RandCmdHelper static method)
(SCCmdHelper static method)
(SparseStoneCmdHelper static method)
(StoneCmdHelper static method)
(SubGraphCmdHelper static method)
(TseitinCmdHelper static method)
C
clause_satisfied() (in module cnfformula.families.randomformulas)
clauses() (CNF method)
,
[1]
(CNF.binary_mapping method)
,
[1]
(CNF.unary_mapping method)
,
[1]
CliqueColoring() (in module cnfformula)
(in module cnfformula.families.cliquecoloring)
CliqueColoringCmdHelper (class in cnfformula.families.cliquecoloring)
CliqueFormula() (in module cnfformula)
(in module cnfformula.families.subgraph)
CNF (class in cnfformula)
(class in cnfformula.cnf)
CNF.binary_mapping (class in cnfformula)
(class in cnfformula.cnf)
CNF.unary_mapping (class in cnfformula)
(class in cnfformula.cnf)
cnfformula (module)
cnfformula.cmdline (module)
cnfformula.cnf (module)
cnfformula.cnfgen (module)
cnfformula.families (module)
cnfformula.families.cliquecoloring (module)
cnfformula.families.coloring (module)
cnfformula.families.counting (module)
cnfformula.families.dominatingset (module)
cnfformula.families.graphisomorphism (module)
cnfformula.families.ordering (module)
cnfformula.families.pebbling (module)
cnfformula.families.pigeonhole (module)
cnfformula.families.ramsey (module)
cnfformula.families.randomformulas (module)
cnfformula.families.simple (module)
cnfformula.families.subgraph (module)
cnfformula.families.subsetcardinality (module)
cnfformula.families.tseitin (module)
cnfformula.graphs (module)
cnfformula.prjdata (module)
cnfformula.transformations (module)
cnfformula.transformations.shuffle (module)
cnfformula.transformations.substitutions (module)
cnfformula.utils (module)
cnfformula.utils.cnfshuffle (module)
cnfformula.utils.dimacstransform (module)
cnfformula.utils.kthlist2pebbling (module)
cnfformula.utils.solver (module)
command_line_utility() (in module cnfformula.cnfgen)
(in module cnfformula.utils.cnfshuffle)
(in module cnfformula.utils.dimacstransform)
(in module cnfformula.utils.kthlist2pebbling)
Complete (CNF.unary_mapping attribute)
,
[1]
counterimages() (CNF.unary_mapping method)
,
[1]
CountingCmdHelper (class in cnfformula.families.counting)
CountingPrinciple() (in module cnfformula)
(in module cnfformula.families.counting)
D
dag_complete_binary_tree() (in module cnfformula.graphs)
dag_pyramid() (in module cnfformula.graphs)
description (AllEqualsSubstitutionCmd attribute)
(AND attribute)
(BPHPCmdHelper attribute)
(BinaryKCliqueCmdHelper attribute)
(CliqueColoringCmdHelper attribute)
(CountingCmdHelper attribute)
(DominatingSetCmdHelper attribute)
(ECCmdHelper attribute)
(EMPTY attribute)
(EMPTY_CLAUSE attribute)
(ExactlyOneSubstitutionCmd attribute)
(FlipCmd attribute)
(FormulaLiftingCmd attribute)
(GAutoCmdHelper attribute)
(GIsoCmdHelper attribute)
(GOPCmdHelper attribute)
(GPHPCmdHelper attribute)
(IfThenElseSubstitutionCmd attribute)
(KCliqueCmdHelper attribute)
(KColorCmdHelper attribute)
(MajCompressionCmd attribute)
(MajSubstitution attribute)
(NeqSubstitutionCmd attribute)
(NoSubstitutionCmd attribute)
(OPCmdHelper attribute)
(OR attribute)
(OrSubstitutionCmd attribute)
(PHPCmdHelper attribute)
(PMatchingCmdHelper attribute)
(PTNCmdHelper attribute)
(ParityCmdHelper attribute)
(PebblingCmdHelper attribute)
(RWCmdHelper attribute)
(RamseyCmdHelper attribute)
(RandCmdHelper attribute)
(SCCmdHelper attribute)
(ShuffleCmd attribute)
(SparseStoneCmdHelper attribute)
(StoneCmdHelper attribute)
(SubGraphCmdHelper attribute)
(TseitinCmdHelper attribute)
(XorCompressionCmd attribute)
(XorSubstitutionCmd attribute)
dimacs() (CNF method)
,
[1]
dimacs2cnf() (in module cnfformula.utils)
dimacs2compressed_clauses() (in module cnfformula.utils)
DirectedAcyclicGraphHelper (class in cnfformula.cmdline)
Domain (CNF.binary_mapping attribute)
,
[1]
(CNF.unary_mapping attribute)
,
[1]
domain() (CNF.unary_mapping method)
,
[1]
DominatingSet() (in module cnfformula)
(in module cnfformula.families.dominatingset)
DominatingSetCmdHelper (class in cnfformula.families.dominatingset)
E
ECCmdHelper (class in cnfformula.families.coloring)
EMPTY (class in cnfformula.families.simple)
EMPTY_CLAUSE (class in cnfformula.families.simple)
enumerate_edges() (in module cnfformula.graphs)
enumerate_vertices() (in module cnfformula.graphs)
equal_to_constraint() (cnfformula.CNF class method)
(cnfformula.cnf.CNF class method)
EvenColoringFormula() (in module cnfformula)
(in module cnfformula.families.coloring)
exactly_half_ceil() (cnfformula.CNF class method)
(cnfformula.cnf.CNF class method)
exactly_half_floor() (cnfformula.CNF class method)
(cnfformula.cnf.CNF class method)
ExactlyOneSubstitution (class in cnfformula)
(class in cnfformula.transformations.substitutions)
ExactlyOneSubstitutionCmd (class in cnfformula.transformations.substitutions)
F
FlipCmd (class in cnfformula.transformations.substitutions)
FlipPolarity (class in cnfformula)
(class in cnfformula.transformations.substitutions)
forbid_bitstring() (CNF.binary_mapping method)
,
[1]
forbid_image() (CNF.binary_mapping method)
,
[1]
FormulaLifting (class in cnfformula)
(class in cnfformula.transformations.substitutions)
FormulaLiftingCmd (class in cnfformula.transformations.substitutions)
Functional (CNF.unary_mapping attribute)
,
[1]
G
GAutoCmdHelper (class in cnfformula.families.graphisomorphism)
GIsoCmdHelper (class in cnfformula.families.graphisomorphism)
GOPCmdHelper (class in cnfformula.families.ordering)
GPHPCmdHelper (class in cnfformula.families.pigeonhole)
GraphAutomorphism() (in module cnfformula)
(in module cnfformula.families.graphisomorphism)
GraphColoringFormula() (in module cnfformula)
(in module cnfformula.families.coloring)
GraphIsomorphism() (in module cnfformula)
(in module cnfformula.families.graphisomorphism)
GraphOrderingPrinciple() (in module cnfformula)
(in module cnfformula.families.ordering)
GraphPigeonholePrinciple() (in module cnfformula)
(in module cnfformula.families.pigeonhole)
greater_or_equal_constraint() (cnfformula.CNF class method)
(cnfformula.cnf.CNF class method)
greater_than_constraint() (cnfformula.CNF class method)
(cnfformula.cnf.CNF class method)
H
has_bipartition() (in module cnfformula.graphs)
have_satsolver() (in module cnfformula.utils.solver)
header (CNF attribute)
,
[1]
I
IfThenElseSubstitution (class in cnfformula)
(class in cnfformula.transformations.substitutions)
IfThenElseSubstitutionCmd (class in cnfformula.transformations.substitutions)
image_to_bitstring() (CNF.binary_mapping method)
,
[1]
images() (CNF.unary_mapping method)
,
[1]
Injective (CNF.binary_mapping attribute)
,
[1]
(CNF.unary_mapping attribute)
,
[1]
is_cnf_generator() (in module cnfformula.families)
is_cnf_transformation() (in module cnfformula.transformations)
is_cnfgen_subcommand() (in module cnfformula.cmdline)
is_dag() (in module cnfformula.graphs)
is_satisfiable() (CNF method)
,
[1]
(in module cnfformula.utils.solver)
K
KCliqueCmdHelper (class in cnfformula.families.subgraph)
KColorCmdHelper (class in cnfformula.families.coloring)
L
latex() (CNF method)
,
[1]
less_or_equal_constraint() (cnfformula.CNF class method)
(cnfformula.cnf.CNF class method)
less_than_constraint() (cnfformula.CNF class method)
(cnfformula.cnf.CNF class method)
loose_majority_constraint() (cnfformula.CNF class method)
(cnfformula.cnf.CNF class method)
loose_minority_constraint() (cnfformula.CNF class method)
(cnfformula.cnf.CNF class method)
M
MajCompressionCmd (class in cnfformula.transformations.substitutions)
MajoritySubstitution (class in cnfformula)
(class in cnfformula.transformations.substitutions)
MajSubstitution (class in cnfformula.transformations.substitutions)
N
name (AllEqualsSubstitutionCmd attribute)
(AND attribute)
(BPHPCmdHelper attribute)
(BinaryKCliqueCmdHelper attribute)
(CliqueColoringCmdHelper attribute)
(CountingCmdHelper attribute)
(DominatingSetCmdHelper attribute)
(ECCmdHelper attribute)
(EMPTY attribute)
(EMPTY_CLAUSE attribute)
(ExactlyOneSubstitutionCmd attribute)
(FlipCmd attribute)
(FormulaLiftingCmd attribute)
(GAutoCmdHelper attribute)
(GIsoCmdHelper attribute)
(GOPCmdHelper attribute)
(GPHPCmdHelper attribute)
(IfThenElseSubstitutionCmd attribute)
(KCliqueCmdHelper attribute)
(KColorCmdHelper attribute)
(MajCompressionCmd attribute)
(MajSubstitution attribute)
(NeqSubstitutionCmd attribute)
(NoSubstitutionCmd attribute)
(OPCmdHelper attribute)
(OR attribute)
(OrSubstitutionCmd attribute)
(PHPCmdHelper attribute)
(PMatchingCmdHelper attribute)
(PTNCmdHelper attribute)
(ParityCmdHelper attribute)
(PebblingCmdHelper attribute)
(RWCmdHelper attribute)
(RamseyCmdHelper attribute)
(RandCmdHelper attribute)
(SCCmdHelper attribute)
(ShuffleCmd attribute)
(SparseStoneCmdHelper attribute)
(StoneCmdHelper attribute)
(SubGraphCmdHelper attribute)
(TseitinCmdHelper attribute)
(XorCompressionCmd attribute)
(XorSubstitutionCmd attribute)
neighbors() (in module cnfformula.graphs)
NeqSubstitutionCmd (class in cnfformula.transformations.substitutions)
NonDecreasing (CNF.binary_mapping attribute)
,
[1]
(CNF.unary_mapping attribute)
,
[1]
NoSubstitutionCmd (class in cnfformula.transformations.substitutions)
NotAllEqualSubstitution (class in cnfformula)
(class in cnfformula.transformations.substitutions)
O
obtain_graph() (BipartiteGraphHelper static method)
(DirectedAcyclicGraphHelper static method)
(SimpleGraphHelper static method)
OPCmdHelper (class in cnfformula.families.ordering)
OR (class in cnfformula.families.simple)
OrderingPrinciple() (in module cnfformula)
(in module cnfformula.families.ordering)
OrSubstitution (class in cnfformula)
(class in cnfformula.transformations.substitutions)
OrSubstitutionCmd (class in cnfformula.transformations.substitutions)
P
parity_constraint() (cnfformula.CNF class method)
(cnfformula.cnf.CNF class method)
ParityCmdHelper (class in cnfformula.families.counting)
Pattern (CNF.unary_mapping attribute)
,
[1]
PebblingCmdHelper (class in cnfformula.families.pebbling)
PebblingFormula() (in module cnfformula)
(in module cnfformula.families.pebbling)
PerfectMatchingPrinciple() (in module cnfformula)
(in module cnfformula.families.counting)
PHPCmdHelper (class in cnfformula.families.pigeonhole)
PigeonholePrinciple() (in module cnfformula)
(in module cnfformula.families.pigeonhole)
PMatchingCmdHelper (class in cnfformula.families.counting)
PTNCmdHelper (class in cnfformula.families.ramsey)
PythagoreanTriples() (in module cnfformula)
(in module cnfformula.families.ramsey)
R
RamseyCmdHelper (class in cnfformula.families.ramsey)
RamseyLowerBoundFormula() (in module cnfformula)
(in module cnfformula.families.ramsey)
RamseyWitnessFormula() (in module cnfformula)
(in module cnfformula.families.subgraph)
RandCmdHelper (class in cnfformula.families.randomformulas)
RandomKCNF() (in module cnfformula)
(in module cnfformula.families.randomformulas)
Range (CNF.binary_mapping attribute)
,
[1]
(CNF.unary_mapping attribute)
,
[1]
range() (CNF.unary_mapping method)
,
[1]
readGraph() (in module cnfformula)
(in module cnfformula.graphs)
register_cnf_generator() (in module cnfformula.families)
register_cnf_transformation() (in module cnfformula.transformations)
register_cnfgen_subcommand() (in module cnfformula.cmdline)
RWCmdHelper (class in cnfformula.families.subgraph)
S
sample_clauses() (in module cnfformula.families.randomformulas)
sample_clauses_dense() (in module cnfformula.families.randomformulas)
SCCmdHelper (class in cnfformula.families.subsetcardinality)
search_cmdline_input_file() (in module cnfformula.cnfgen)
setup_command_line() (AllEqualsSubstitutionCmd static method)
(AND static method)
(BPHPCmdHelper static method)
(BinaryKCliqueCmdHelper static method)
(BipartiteGraphHelper static method)
(CliqueColoringCmdHelper static method)
(CountingCmdHelper static method)
(DirectedAcyclicGraphHelper static method)
(DominatingSetCmdHelper static method)
(ECCmdHelper static method)
(EMPTY static method)
(EMPTY_CLAUSE static method)
(ExactlyOneSubstitutionCmd static method)
(FlipCmd static method)
(FormulaLiftingCmd static method)
(GAutoCmdHelper static method)
(GIsoCmdHelper static method)
(GOPCmdHelper static method)
(GPHPCmdHelper static method)
(IfThenElseSubstitutionCmd static method)
(KCliqueCmdHelper static method)
(KColorCmdHelper static method)
(MajCompressionCmd static method)
(MajSubstitution static method)
(NeqSubstitutionCmd static method)
(NoSubstitutionCmd static method)
(OPCmdHelper static method)
(OR static method)
(OrSubstitutionCmd static method)
(PHPCmdHelper static method)
(PMatchingCmdHelper static method)
(PTNCmdHelper static method)
(ParityCmdHelper static method)
(PebblingCmdHelper static method)
(RWCmdHelper static method)
(RamseyCmdHelper static method)
(RandCmdHelper static method)
(SCCmdHelper static method)
(ShuffleCmd static method)
(SimpleGraphHelper static method)
(SparseStoneCmdHelper static method)
(StoneCmdHelper static method)
(SubGraphCmdHelper static method)
(TseitinCmdHelper static method)
(XorCompressionCmd static method)
(XorSubstitutionCmd static method)
(in module cnfformula.utils.dimacstransform)
(in module cnfformula.utils.kthlist2pebbling)
setup_command_line_args() (in module cnfformula.cnfgen)
Shuffle() (in module cnfformula)
(in module cnfformula.transformations.shuffle)
ShuffleCmd (class in cnfformula.transformations.shuffle)
signal_handler() (in module cnfformula.cnfgen)
(in module cnfformula.utils.dimacstransform)
(in module cnfformula.utils.kthlist2pebbling)
SimpleGraphHelper (class in cnfformula.cmdline)
SparseStoneCmdHelper (class in cnfformula.families.pebbling)
SparseStoneFormula() (in module cnfformula)
(in module cnfformula.families.pebbling)
stone_formula_helper() (in module cnfformula.families.pebbling)
StoneCmdHelper (class in cnfformula.families.pebbling)
StoneFormula() (in module cnfformula)
(in module cnfformula.families.pebbling)
SubGraphCmdHelper (class in cnfformula.families.subgraph)
SubgraphFormula() (in module cnfformula)
(in module cnfformula.families.subgraph)
SubsetCardinalityFormula() (in module cnfformula)
(in module cnfformula.families.subsetcardinality)
supported_formats() (in module cnfformula.graphs)
supported_satsolvers() (in module cnfformula.utils.solver)
Surjective (CNF.unary_mapping attribute)
,
[1]
T
transform_a_literal() (AllEqualSubstitution method)
,
[1]
(BaseSubstitution method)
(ExactlyOneSubstitution method)
,
[1]
(FlipPolarity method)
,
[1]
(FormulaLifting method)
,
[1]
(IfThenElseSubstitution method)
,
[1]
(MajoritySubstitution method)
,
[1]
(NotAllEqualSubstitution method)
,
[1]
(OrSubstitution method)
,
[1]
(VariableCompression method)
,
[1]
(XorSubstitution method)
,
[1]
transform_cnf() (AllEqualsSubstitutionCmd static method)
(ExactlyOneSubstitutionCmd static method)
(FlipCmd static method)
(FormulaLiftingCmd static method)
(IfThenElseSubstitutionCmd static method)
(MajCompressionCmd static method)
(MajSubstitution static method)
(NeqSubstitutionCmd static method)
(NoSubstitutionCmd static method)
(OrSubstitutionCmd static method)
(ShuffleCmd static method)
(XorCompressionCmd static method)
(XorSubstitutionCmd static method)
transform_variable_preamble() (BaseSubstitution method)
(FormulaLifting method)
,
[1]
TseitinCmdHelper (class in cnfformula.families.tseitin)
TseitinFormula() (in module cnfformula)
(in module cnfformula.families.tseitin)
V
var_name() (CNF.binary_mapping static method)
,
[1]
(CNF.unary_mapping static method)
,
[1]
VariableCompression (class in cnfformula)
(class in cnfformula.transformations.substitutions)
variables() (CNF method)
,
[1]
(CNF.binary_mapping method)
,
[1]
(CNF.unary_mapping method)
,
[1]
varname() (in module cnfformula.families.ordering)
W
writeGraph() (in module cnfformula)
(in module cnfformula.graphs)
X
XorCompressionCmd (class in cnfformula.transformations.substitutions)
XorSubstitution (class in cnfformula)
(class in cnfformula.transformations.substitutions)
XorSubstitutionCmd (class in cnfformula.transformations.substitutions)
Read the Docs
v: stable
Versions
latest
stable
Downloads
pdf
htmlzip
epub
On Read the Docs
Project Home
Builds
Free document hosting provided by
Read the Docs
.