Basically, it halves the solution space approximately correctly each time. So you keep on adding them, until you have say, 10 solutions. Then you multiply the 10 with 2^k, where k is the number of XORs you added. That's it! So cool, no? And it's super-scalable, because it haves it each time, so you'll get to, say, 10 pretty quick!
Some research papers are here [2,3]. I work on this, the tools are here [4,5]. In the last model counting competition, it dominated all other competitors, when combined with an exact counter, slides of the competition here [6].
[1] https://www.msoos.org/2018/12/how-approximate-model-counting... [2] https://arxiv.org/abs/1306.5726 [3] https://www.cs.toronto.edu/~meel/Papers/cav20-sgm.pdf [4] https://github.com/meelgroup/approxmc [5] https://github.com/meelgroup/unigen [6] https://mccompetition.org/assets/files/2024/MC2024_awards.pd...