Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Markov Chain -- dSharp compiler results in prob >1 #113

Open
davidedema opened this issue Apr 16, 2024 · 8 comments
Open

Markov Chain -- dSharp compiler results in prob >1 #113

davidedema opened this issue Apr 16, 2024 · 8 comments
Labels
bug Something isn't working

Comments

@davidedema
Copy link

I wrote a simple program that describes a Markov chain composed by 3 states and the relative transition probabilities:

state(s1).
state(s2).
state(s3).


0.2::init(state(s1)).
0.8::init(state(s2)).

0.8::next(s1,s1).
0.2::next(s1,s2).

0.3::next(s2,s2).
0.4::next(s2,s3).
0.3::next(s2,s1).

0.7::next(s3,s3).
0.3::next(s3,s1).

prob_reach(state(State), 0) :-
    init(state(State)).

prob_reach(state(State), Steps) :-
    Steps > 0,
    Steps1 is Steps - 1,
    next(S, State),
    prob_reach(state(S), Steps1).

query(prob_reach(state(s1), 1)).

When I run this, the returned probability is not the one that it is found with the classic formula (e.g. probability found with problog to be in the state s1 after 1 step is 0.3616 but the real one is 0.4). There is something that I'm missing with the probability calculation done by problog or there are errors in this simple program? Thanks

@VincentDerk
Copy link
Collaborator

You most likely intended to use annotated disjunctions.

0.2::init(state(s1)).
0.8::init(state(s2)).

means there is 0.2 probability that init(state(s1)) is true, and 0.8 probability that init(state(s2)) is true, but that includes a scenario where they are both true.

Annotated disjunctions, like the one below, imply a mutual exclusivity constraint such that this rule makes init(state(s1)) true with probability 0.2, or (mutual exclusivity or) init(state(s2)) with 0.8, or (mutex or) nothing true with 0.0 probability. Annotated disjunctions must sum to at most 1.0. They are allowed to sum to less than 1.0, in which case there is a probability that none of the probabilistic facts become true.

0.2::init(state(s1)) ; 0.8::init(state(s2)).

By using

0.2::init(state(s1)) ; 0.8::init(state(s2)).

query(prob_reach(state(s1), 1)). is indeed 0.4. Possibly you also want to make your transitions mutually exclusive, but it depends on your semantics. If you model a network of a disease spreading then you would for instance also allow it to spread to multiple.

Hope that helps.

@davidedema
Copy link
Author

Thank you very much for the explanation, helped a lot!

@VincentDerk
Copy link
Collaborator

VincentDerk commented Apr 16, 2024

Perhaps also good to be aware of in your program, your next predicate is currently independent of Step so whether s1 connects to s2 (next(s1,s2)) is decided once and stays true/false throughout the steps. This is different semantics from

0.8::next(s1,s1, Step).
0.2::next(s1,s2, Step).

0.3::next(s2,s2, Step).
0.4::next(s2,s3, Step).
0.3::next(s2,s1, Step).

0.7::next(s3,s3, Step).
0.3::next(s3,s1, Step).

where the connection between s1 to s2 may differ per timestep. (This comment is on top of the annotated disjunction you probably wanted to use here.)

@davidedema
Copy link
Author

Oh, thanks. Now it works as intended. Thank you very much!

@davidedema
Copy link
Author

I adapted the program in this way

state(s1).
state(s2).
state(s3).

% Possible init states
0.2::init(state(s1)); 0.8::init(state(s2)).

% Transition model
0.8::next(s1,s1, Step); 0.2::next(s1,s2, Step).

0.3::next(s2,s1, Step); 0.3::next(s2,s2, Step); 0.4::next(s2,s3, Step).

0.3::next(s3,s1, Step); 0.7::next(s3,s3, Step). 

prob_reach(state(State), 0) :-
    init(state(State)).

prob_reach(state(State), Steps) :-
    Steps > 0,
    next(S, State, Steps),
    Steps1 is Steps - 1,
    prob_reach(state(S), Steps1).

query(prob_reach(state(s1), 5)).

It works as intended but if I pump up the number of steps (e.g. 40) it will return strange results:

prob_reach(state(s1),40):       156.13047

Is it some sort of overflow? For other numbers of steps < ~35 it works as intended

@davidedema davidedema reopened this Apr 20, 2024
@VincentDerk
Copy link
Collaborator

VincentDerk commented Apr 20, 2024

That output is very concerning, thanks for reporting!

It will require some deeper investigation, but for now I have the following information and workaround:

  • If I swap out the dsharp knowledge compiler with c2d, the answer becomes 0.5999999999996348 (instructions below). I assume that is the correct probability.
  • Presumably the problem then lies with the dsharp binary, and our pipeline using PySDD is unaffected. For your specific problem the PySDD compilation seems to take a long time, so I suggest you use the c2d compiler workaround for now.

Swapping dsharp with c2d.

  1. Download c2d from http://reasoning.cs.ucla.edu/c2d/
  2. Rename c2d to cnf2dDNNF and copy the executable to the folder problog/bin/linux/ OR make it available through PATH
  3. That is all. ProbLog will then automatically detect and use the c2d binary instead of dsharp.

Debugging information (for myself)

The dsharp compiler produces a wrong d-DNNF.

  1. dSharp's unweighted model count is 3.97+61, which does not correspond to the count of its compiled NNF (according to query-ddnnf reasoner that is 1e+64).
  2. The expected unweighted model count is 3.97e+61, according to D4, dsharp stats, and the NNF of c2d.
  • D4: The unweighted model count: 39708868943559345451429439397652844050730171778133720697929728
  • c2d: The unweighted model count of the nnf: 39708868943559345451429439397652844050730171778133720697929728
  • dsharp: The unweighted model count of the nnf: 1539200437371327859536739816372250725181561293303903889456627712
  • dsharp: The unweighted model count is 3.97089e+61

issue-113.cnf.txt

@VincentDerk VincentDerk changed the title Markov chain prob after t step Markov Chain -- dSharp compiler results in prob >1 Apr 20, 2024
@VincentDerk VincentDerk added the bug Something isn't working label Apr 20, 2024
@davidedema
Copy link
Author

Thanks for the answer, the workaround works

@VincentDerk
Copy link
Collaborator

Glad the workaround works!

This is potentially related to the following bug QuMuLab/dsharp#12

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants