logoalt Hacker News

kachnuv_ocasektoday at 4:19 PM1 replyview on HN

Can you share more about the connection between MCMC and SAT/SMT? That's a crossover I never thought I'd see.


Replies

mdritchtoday at 4:41 PM

Sure! Roughly we are using hierarchical models for reads on underlying count or prevalence data. We use those higher-order means or other fit params to kick off remediation tasks at different levels of that hierarchy depending on those higher level params. We assume some correlation between sibling nodes in that hierarchy.

Question: Can one or another of those thresholds in sibling or parent nodes ever be met if some number of the samples are below some floor reading? Or, how many zeros does it take to silence a threshold check on the node itself, a sibling, or a parent?

To make this tractable I have tried gridding fit parameters, freezing randomness, and using simplified algs like original Metropolis-Hastings