Polynomials for WFOMC

This tool is for computing Weak Connectedness Polynomial (WCP), Strict Strong Connectedness Polynomial (SSCP), Non-strict Strong Connectedness Polynomial (NSCP), Extended WCP and Tutte Polynomial from a given $C^2$ sentence with cardinality constraints.

Input format

1. First-order sentence with at most two logic variables, see fol_grammar.py for details, e.g.,
   • \forall X: (\forall Y: (R(X, Y) <-> Z(X, Y)))
   • \forall X: (\exists Y: (R(X, Y)))
   • \exists X: (F(X) -> \forall Y: (R(X, Y)))
   • ..., even more complex sentence...
2. Domain:
   • domain=3 or
   • domain={p1, p2, p3}
3. Weighting (optional): positve_weight negative_weight predicate
4. Cardinality constraint (optional):
   • |P| = k
   • |P| > k
   • |P| >= k
   • |P| < k
   • |P| <= k
   • ...

Example input file

2 colored graphs:

\forall X: (\forall Y: ((E(X,Y) -> E(Y,X)) &
                        (R(X) | B(X)) &
                        (~R(X) | ~B(X)) &
                        (E(X,Y) -> ~(R(X) & R(Y)) & ~(B(X) & B(Y)))))

V = 10

2 regular graphs:

\forall X: (~E(X,X)) &
\forall X: (\forall Y: ((E(X,Y) -> E(Y,X)) &
                        (E(X,Y) <-> (F1(X,Y) | F2(X,Y))) &
                        (~F1(X, Y) | ~F2(X,Y)))) &
\forall X: (\exists Y: (F1(X,Y))) & 
\forall X: (\exists Y: (F2(X,Y)))

V = 6
|E| = 12

Note: You can also directly input the SC2 sentence

2 regular graphs (sc2):

\forall X: (~E(X,X)) &
\forall X: (\forall Y: (E(X,Y) -> E(Y,X))) &
\forall X: (\exists_{=2} Y: (E(X,Y)))

V = 6

Sampling possible worlds from friends-smokes MLN:

\forall X: (~fr(X,X)) &
\forall X: (\forall Y: (fr(X,Y) -> fr(Y,X))) &
\forall X: (\forall Y: (aux(X,Y) <-> (fr(X,Y) & sm(X) -> sm(Y)))) &
\forall X: (\exists Y: (fr(X,Y)))

person = 10
2.7 1 aux

Note: You can also directly input the MLN in the form defined in mln_grammar.py

~friends(X,X).
friends(X,Y) -> friends(Y,X).
2.7 friends(X,Y) & smokes(X) -> smokes(Y)
\forall X: (\existes Y: (fr(X,Y))).
# or 
\exists Y: (fr(X,Y)).

person = 10

More examples are in models

Installation

Install the package:

$ pip install -e .

How to use

see $ python sampling_fo2/main.py -h. The usage is as follows.

usage: main.py [-h] --input INPUT [--output_dir OUTPUT_DIR] [--func {wcp,scp,ewcp,tutte}] --pred PRED [--debug]

Computing Polynomials from a C2 sentence

optional arguments:
  -h, --help            show this help message and exit
  --input INPUT, -i INPUT
                        mln file
  --output_dir OUTPUT_DIR, -o OUTPUT_DIR
  --func {wcp,nscp,sscp,ewcp,tutte}, -f {wcp,nscp,sscp,ewcp,tutte}
                        the function wanted
  --pred PRED, -p PRED  the special binary predicate
  --debug

E.g., to get the WCP for the predicate E in the sentence encoding an arbitrary undirected graph, the command is:

$ python sampling_fo2/main.py -i models/arbitrary-undirected-graph.wfomcs -f wcp -p E

References

@misc{kuang2024bridgingweightedordermodel,
      title={Bridging Weighted First Order Model Counting and Graph Polynomials}, 
      author={Qipeng Kuang and Ondřej Kuželka and Yuanhong Wang and Yuyi Wang},
      year={2024},
      eprint={2407.11877},
      archivePrefix={arXiv},
      primaryClass={cs.LO},
      url={https://arxiv.org/abs/2407.11877}, 
}