All posts by msoos

Ganakv2 Released

Development, Research, SAT, Tools, ,

Finally, after many months of waiting for our paper to be accepted (preliminary PDF here), Ganak2 is finally released (GitHub code, released binaries) and easily accessible and modifiable. I wish this release had come earlier, but double-blind requirements didn’t allow us to release the code any sooner.

Basically, Ganakv2 has been re-written in many ways. Some of the original ideas by Thurley for SharpSAT has been kept alive, but many-many things are completely different and completely re-written — well over 10’000 lines of change in total. This set of changes has allowed Ganak2 to win every available track at the Model Counting Competition of 2024. In other words, Ganak2 is incredibly fast, making it a state-of-the-art tool.

Chonological Backtracking, Enhanced SAT solving, S- and D-sets

The new Ganak has a pretty powerful SAT solver engine with its own restart strategy, polarity and variable branching strategy. This SAT solver is tightly integrated into Ganak, and reuses the same datastructures a Ganak, hence the counter/SAT transitions are smooth. This relies on the observation that once every variable in the (minimal) independent set has been assigned, there is at most one solution, so we can just run a SAT solver, there is no need to a full-blown model counter. This idea has existed at least since GPMC, but we improved on it in important ways.

A very complicated but very important aspect of Ganak2 is our integration of Chronological Backtracking which we adopted to the model counting setting. This required a lot of attention to detail, and in order to debug this, we took full advantage of the fuzzer written and maintained by Anna Latour. We further added very serious and thorough checking into Ganak2, with varying levels of internal checking and per-node checking of counts. This allows to perform effective debugging: the first node that the count is incorrect will immediately stop and error-out, along with a full human-readable debug log of what had happened. This was necessary to do, as some of the issues that Chonological Backtracking leads to are highly non-trivial, as mentioned in the paper.

Ganak2 now understands something we call a D-set, which is a set of variables that’s potentially much larger than the projection set but when branched on, the count is the same. This allows Ganak to branch on far more variables than any other current model counter. We run an algorithm that takes advantage of Padoa’s theorem to make this D-set as large as possible. Further, Ganak2 takes advantage of projection set minimization, calling he minimal set an S-set, and running a SAT solver as soon as all variables from the S-set have been decided. This allows us to run a SAT solver much earlier than any other model counter.

Component Discovery, Subsumption and Strengthening, and Counting over any Field

Since the paper, I have also added a number of pretty interesting improvements, especially related to component generation, which is now a highly cache-optimized datastructure, using time stamping, a trick I learned from Heule et al’s brilliant tree-based lookahead paper (worth a read). I also changed the hash function used to chibihash, it’s not only faster (on the small inputs we run it on) but also doesn’t rely on any specific instruction set, so it can be compiled to emscripten, and so Ganak2 can run in your browser.

There is also a pretty experimental on-the-fly subsumption and strengthening that I do. It actually rewrites the whole search tree in order to achieve this, which is a lot harder to do than I imagined. It’s the most trivial subsumption & strengthening code you can imagine, but then the rewriting is hell on earth. However, the rewriting is necessary in case we want to be able to continue counting without restarting the whole counting process.

Ganak, unlike many of its counterparts, also manages memory very tightly and tries not to die due to memory-out. The target memory usage of the cache can be given via –maxcache in MB. A cache size of 2500MB is default, which should cap out at about 4GB total memory usage. More cache should lead to better performance, but we actually won (every available track of) the Model Counting Competition 2024 with rather low memory usage, I think I restricted it to 8-12GB — other competitors ran with ~2x that.

Furthermore, Arjun, our CNF minimizer has also been tuned. While this is not specifically Ganak, it gives a nice improvement, and has some cool ideas that I am pretty happy about. In particular, it runs the whole preprocessing twice, and it incorporates Armin Biere’s CadiBack for backbone detection. I wish I could improve this system a bit, because sometimes CadiBack takes >1000s to run, but without it, it’s even slower to count in most cases. But not always, and sometimes backbone is just a waste of time.

The system also now allows to use any field, all you need to do is implement the +/-/*/div operators and the 0 and 1 constants. I have implemented integers, rationals, modulo prime counting, and counting over a the field of polynomials with rational coefficients. All you need to do is override the Field and FieldGen interfaces. I made it work for modulo prime counting in under 20 minutes, it’s like 30 lines of code.

Floating Point Numbers

Notice that floating point numbers don’t form a field, because 0.1+0.2 is not equal to 0.2+0.1, i.e. it’s not commutative. Actually, Ganak2’s weighted model counting doesn’t currently support floating point numbers, because it doesn’t need to — we won literally every available track with infinite rational numbers: 0.3 is simply interpreted as 3/10. This sounds minor, but it also means that it’s actually trivial to check if Ganak runs correctly — it simply needs to be run with a different configuration and it should produce the same solution. Notice that this is not at all true for any other weighted model counter. Literally all of them, except for Ganak, will give different solutions if ran with different seeds. Which is hilarious, since there is obviously only one correct solution. But since 0.1+0.2 is not equal to 0.2+0.1 in floating point, they can’t do anything… rational.

This whole floating point saga is actually quite annoying, as it also means we can’t check Ganak against any other counter — at least not easily. All other counters give wrong answers, given that floating point is incorrect, and so we can only compare Ganak2 to other counters if we allow a certain deviation. Which is pretty hilarious, given that counters all claim to use “infinite precision”. In fact, the only thing infinite about their results is likely the error. Since (0.1+02)-(0.2+0.1) is not 0, it is actually possible to have theoretically infinite error in case of negative weights.

Approximate Counting and Ganak

Ganak2 incorporates ApproxMC, and can seamlessly transition into counting via approximate model counting methods. To do this, simply pass the “–appmct T” flag, where T is the number of seconds after which Ganak will start counting in approximate mode. This can only be done for unweighted counting, as ApproxMC can only do unweighted counting. However, this seamless transition is very interesting to watch, and demonstrates that using a multi-modal counting framework, i.e. exact+approximate is a very viable strategy.

What happens under the hood is currently unpublished, but basically, we stop the exact counting, check how much we have counted so far, subtract that from the formula, and pass it to ApproxMC. We then get the result from ApproxMC and add the partial count that Ganak counted, and display the result to the user. So the final count is partially approximate, and partially exact, so we actually give better approximation (epsilon and delta) guarantees than what we promise.

Compiling Ganak

The new Ganak incorporates 8 libraries: GNU MP, CryptoMiniSat, Arjun, ApproxMC, SBVA, CadiCal, CadiBack, and BreakID. Furthermore, it and compiles in (optinally) BuDDy, Oracle (from Korhonen and Jarvisalo) and Flowcutter. These are all individually mentioned and printed to the console when running. However, this means that building Ganak is not trivial. Hence, with the very generous help of Noa Aarts, Ganak has a flake nix, so you can simply:

git clone https://github.com/meelgroup/ganak
cd ganak
nix-shell

And it will reproducibly build Ganak and make it available in the path. All this needs is for one to have installed Nix, which is a single-liner and works incredibly reliably. Otherwise, the Ganak repository can be cloned together with its GitHub Actions, and then each push to the repository will build Ganak2 for 4 different architectures: Linux x86&ARM, Mac x86&ARM.

Submit your Version of Ganak to the 2025 Competition

Ganak2 is highly extensible/modifiable. I strongly encourage you to extend/change/improve it and submit your improvement to the Model Counting Competition of 2025. Deadline is in 3 weeks, it’s time to get your idea into Ganak and win. I promise I will have all my changes publicly available until then, and you can literally submit the same thing I will, if you like. I’d prefer if you put in some cool change, though.

Ethereum in the age of AOL

Ethereum

Imagine you are super-excited about some new technology that’s enabled by the internet, say, Google, and instead of investing in Google, i.e. buying Google stock, you start buying AT&T stock. Or let’s say Facebook just came out, and it’s the hottest thing. Everyone wants Facebook. So instead of investing in Facebook stock, you start buying AT&T stock. It’d be just weird, right? But that’s what seems to be happening in the crypto space.

The more I spend in this space, the more I’m baffled by people buying and holding ETH, the native currency of Ethereum, hoping that if the next Facebook comes around, the value of ETH will go up. And to be fair, AT&T and Cisco stock probably did go up when Netflix became popular. But ultimately, AT&T, Cisco, T-mobile — they are just the underlying pipes. Sure enough, Cisco should go up somewhat when Netflix is becoming popular, because you definitely need routers to watch Netflix. But we all understand that the Internet is just the piping.

This is reminiscent of AOL. Back in the dark ages of the Internet, AOL was “the” internet, it provided all the services in one place. From directory to mail services. If you wanted to invest in the internet, you bought AOL stock. But that’s no longer the case, and for a good reason.

Electricity, the Internet, and Infrastructure

Electricity plug designed to fit into a socket for light bulbs

I think most people would find it rather insane to buy electricity suppliers’ stocks when a new type of home appliance, say robot vacuums come around. However, electricity stocks were a big deal back in the day. The original use-case for electricity at home was light bulbs. Light bulbs were huge — lighting was expensive (you had to get candles or oil) and was painful to light up, and sometimes it burned down buildings. In fact, the original washing machines’ electric plugs actually plugged into a socket for light bulbs! You had to screw it in — and unscrew it in case there was an accident. Which was very-very dangerous, hence the new sockets that are very easy to unplug. But it’s interesting to observe that there was an original use-case, and it was so popular that “electricity”just straight up meant light bulbs, and nothing else.

The original use-case of cryptocurrencies was liquid, fast transfer of fungible value over the network without a central system. But we moved way beyond that now. We have currencies and banks operating over Ethereum. We have casinos and online games and betting platforms. We have exchanges and brokers. However, somehow people still hope that the infrastructure value will go up.

Hoping your AT&T bill goes up

Imagine buying a monthly internet subscription from AT&T and hoping that the subscription costs go up. That’s what’s happening in crypto. The native currency of Ethereum is used to regulate the transactions on the chain, so that the competition of which transaction makes it into the chain can be decided. When you hold ETH, you are effectively hoping that transaction costs go up. It’s like hoping that your AT&T bill gets higher. Who the hell would want that? It’s infrastructure cost, it’s not supposed to go up over time. It’s supposed to go down.

The secondary use-case of ETH is the consensus protocol, making sure the things that do make it into the transaction block are what one would more or less expect. So it’s used to also secure the chain in a manner that’s called Proof-of-Stake. Here, the value of ETH is used to make sure it’s not economically viable to cheat. However, it wouldn’t be too difficult to move staking to stablecoins such as Dai, or other value-holders, e.g. a combination of the most used systems on the chain. After all, it’s in everyone’s best interest for the most value-generating systems to survive.

Betting on success

In my view, if you want to bet on the crypto system to be successful, you need to start betting on not only ETH, but much more importantly all the systems that make Ethereum useful. Looking at e.g. a DeFi token list is a good start. Ultimately, the internet is not useful because of AT&T. It’s useful because of email, websites, and online systems such as Ethereum itself, which wouldn’t exist without the Internet. Yet I’m pretty sure ETH holders are not in a rush to buy AT&T stock. In the same vain, they should not be in a rush to buy ETH. Rather, they should be investing in all the systems and tools built on top of Ethereum. Ethereum is “just” the infrastructure, similarly how the internet on which Ethereum runs, is “just” the infrastructure, which itself is built on electricity, which is “just” the infrastructure. Sure, we need the infrastructure. And we need to invest in the infrastructure (I have a separate rant on how little is actually being invested by anyone other than the Ethereum Foundation). But only investing in the infrastructure, and not on the systems built on top of it, is weird.

Post Scriptum: Bitcoin

Bitcoin is forever stuck at being electricity for light bulbs only. Make of that what you will. Light bulbs are useful, of course. But I’m typing this on a computer, that’s connected to the internet, and my light bulbs are not even on. If electricity was only capable of lighting the light bulb, and not powering my computer, my router, and the system of routers that route my packets to you, we would still be writing&reading articles in physical newspapers, and sending mail via physical post.

References

You may be interested in this article and this tweet thread for ideas and thoughts that others had independently, but well before me. Thanks to M. at the EF for these references, they are actually really relevant. I’m glad others are seeing things similarly to me.

Computing Tricky Probabilities

Uncategorized

Probabilities of certain events are really hard to estimate sometimes. Often, it’s because we lack information of the underlying causal chains, but sometimes, it’s because the causes are so intertwined that even if we know the underlying probabilities of certain events happening along with the causal chains, it’s still impossible for us to untangle the web.

Let’s say there’s an event X has a probability of 0.4, Y has a probability of 0.6, and Z happens if either X or Y happens, but X and Y can’t happen at the same time, with a probability of 0.8. What’s the probability of Z happening?

             0.4                  0.6          
         ┌───────┐            ┌───────┐       
         │       │    0.8     │       │       
         │   X   │◄────!─────►│   Y   │       
         │       │            │       │       
         └──┬────┘            └────┬──┘       
            │                      │                    
            │      ┌───────┐       │          
            │      │       │       │          
            └─────►│   Z   │◄──────┘          
                   │       │                  
                   └───────┘

Translating to a Model Counting Problem

The solution is easy to compute if you know how to use propositional model counters. They allow you to create a set of rules, such as:

X = 0.4
Y = 0.6
X or Y = True
0.8 -> NOT (X & Y)

The above perfectly describes the probability landscape, by using “->”, i.e. implication (if the left side is true, the right side must also be true), and using “&” (i.e. logical AND). Basically, for Z to happen, X or Y has to happen. And with probability 0.8, they must not happen at the same time. To solve the above, we add a helper variable H1, that will allow us to translate the last equation into an implication:

X = 0.4
Y = 0.6
X or Y = True
H1 = 0.8
H1 -> NOT (X & Y)

To translate this to propositional model counting, we can do the following, where “-” is negation:

weight X = 0.4
weight Y = 0.6
weight H1 = 0.8
X or Y = True
-H1 or -X or -Y = True

The highlighted lines are what’s call the Tseitin transformation, which basically means that when H1 is TRUE, (NOT X or NOT y) must be TRUE, i.e. at least one of them has to be FALSE, i.e. they can’t happen at the same time (but it’s possible that neither of them happens). The above is what’s called a conjunctive normal form, or CNF for short.

The model counting DIMACS representation (formal description here) of the above is:

c t pwmc
p cnf 3 2
c comment X = 1, Y = 2, H1 = 3
c p weight 1 0.4 0
c p weight 2 0.6 0
c p weight 3 0.8 0
1 2 0
-3 -1 -2 0
c p show 1 2 3 0

Which is a straightforward 1-to-1 translation of the above, except we have to tell the counter that this is a projected weighted model counting problem (“pwmc”) and that it has 3 variables, and 2 constraints (“p cnf 3 2”).

Solving with a Model Counter

Once you have a CNF representation, you can run a modern propositional weighted model counter to count the number of weighted solutions, i.e. the probability of Z. I recommend the one I develop, ganak (linux binary here, open source code will be available soon, ask me if you need it):

./ganak problem.cnf
c s type pwmc
s SATISFIABLE
c s exact arb float 5.68E-01

So Z has a probability of 0.568. This can easily be verified to be correct:

Python 3.13.1
>>> 0.6*(1-.4)+0.4*(1-0.6)+0.4*0.6*(1-0.8)
0.568

Which adds up the probabilities that the left fires (but not the right), the right fires (but not the left), and that both fire, but the conflict does not happen (with 1-0.8 probability).

Of course, the above is a rather simple problem. However, with the above steps, one can create arbitrarily complicated causal chains, with complex constraints between partial, or intermediate elements of the chain, conditional probabilities, etc. Although there are limits to scalability, it’s many-many orders of magnitude faster than anything by hand, or by some form of brute-force checking/estimation.

Use-cases

In certain scenarios, it’s really important to know what the probability of some event is. For example, if you want to run a hazardous process such as a nuclear reactor or a chemical plant, or you want to provide insurance for some complicated (financial) product, accurately computing the probabilities of bad events happening is extremely important. I think it’s rather obvious that nuclear plants have very complicated causal chains for bad events happening — and they tend to be intertwined. If the external power lines are damaged, then likely it’s a major event (e.g. earthquake) and you likely also lost the majority of your transport capabilities, and along them, much of potential external help.

Similarly, if you want to bet for/against market moves, where you know or have a good idea of the underlying causal chains and associated probabilities, you can build quant trading, or expert advice systems based on the above. In other words, weighted model counting is not only useful for party tricks. Complex probability chains with thousands of interdependent random variables can easily be analyzed using the above system.

Some food for thought: great content on the Internet

Personal

The Internet is a pretty vast place. So I decided to curate a few links for you all for this special end-of-year period:

Ágnes Dénes – Wheatfield – A Confrontation, 1982, Battery Park Landfill, Downtown Manhattan, photo: John McGrall

On SAT/SMT Model Counting

Docs/Faqs, SAT, SMT

I have recently had a few discussions with people who wanted to do some form of model counting, and I decided to put my thoughts about this problem into a single blog post, hopefully bringing some light to this area. Firstly, when talking about model counting, it’s very important to think through what one actually needs to achieve. When people talk about a model, they often mean a solution to a problem, described as a set of constraints over either purely boolean variables (so-called propositional model counting) expressed in so-called CNF, or over higher-level constraints, often expressed in SMT-LIB format.

Let’s look at a CNF example:

c this is a comment
c below line means there are 5 boolean variables and 2 constraints
p cnf 5 2
1 -2 0
1 -2 3 0

The above CNF has 5 boolean variables and 2 constraints: “v1 or (not v2) = true”, and “v1 or (not v2) or v3 = true”. In this case, if “v1 or (not v2) = true” is satisfied, the other constraint is also satisfied. So we effectively only have to satisfy the “v1 or -v2” constraint. There are 3 solutions over the variables v1 and v2 to this constraint: (1, 0), (1, 1), and (0,0). For variables v3, v4, and v5 we can choose anything. So there are a total of 3*2^3 = 24 solutions to this CNF.

Let’s look at an SMT problem:

(set-logic QF_BV) ; Set the logic to Quantifier-Free BitVectors
(declare-fun bv () (_ BitVec 8)) ; Declare an 8-bit value
(assert (not (= bv #x00))) ; Assert that 'bv' is not equal to zero

In this SMT-LIB problem, we declared that the logic we will be using is the so-called quantifier-free bitvector logic, which basically gives you access to fixed-width variables such as uint8_t, and of course all the logical and fixed-bit bitwector operators such as modulo addition, division, subtraction, etc. In this particular case, we declared an 8-bit variable and banned it from being 0, so this problem has 2^8-1 solutions, i.e. 255.

Whichever format is being used, “counting” of solutions is something that may sound trivial (it’s just a number!), but once we get a bit more fiddly, it turns out that we can do many things that are actually easier, or even harder, than just counting, even though they sound very close to, or are even synonymous with, counting :

  • Figuring out if there is at least one solution. This is more appropriately called satisfiability checking. This is significantly easier than any notion of counting listed below. However, even this can be challenging. Typically, in the SMT/SAT competition, this is the so-called SMT single query track or the SAT competition Main Track. All SAT and SMT solvers such as kissat or cvc5 can run this kind of task.
  • Next up in complexity is to figure out if there is exactly one solution. This is actually very close to satisfiability checking, and requires only two so-called “incremental calls” to the SMT/SAT solver. I have seen this question pop up a lot in zero-knowledge (ZK) circuit correctness. What is needed is to run the query as per the above, but then add a constraint that bans the solution that is output by the solver, and ask the system to be solved again. If the solver outputs UNSAT, i.e. unsatisfiable, then we know there are no more solutions, and we are happy with the result. If not, it gives us another solution, which is a witness that there are at least two solutions. These queries are answered by so-called incremental SMT solvers (SMT competition track here), or incremental SAT solvers (incremental SAT competition track here). Almost all SAT and SMT solvers can work incrementally, for example cvc5 or z3. Most SAT solvers work incrementally, too, but e.g. kissat does not, and you need to use CaDiCaL instead.
  • Next up in complexity is to approximately count the solutions. Here, we are not interested that there are exactly, say, 87231214 solutions, instead, we are happy to know that there are approx 2^26 solutions. This is often good enough, in case one wants to e.g. figure out probabilities. There are very few such systems available, for SMT there is csb, and for SAT there is ApproxMC. For the special case of approximate DNF counting, I’d recommend pepin.
  • Next up in the complexity is exactly counting the solutions. Here, we want to know how many solutions there are, exactly, and we really-really need the exact number. There are few solutions to doing this over SMT, but doing this over SAT is quite developed. For SMT, I would recommend following the csb approach, and running Ganak on the blasted SAT formula instead of ApproxMC, and for SAT, there is the annual model counting competition, where Ganak won every single category this year, so I’d recommend Ganak.
  • Next up is model enumeration where it’s not enough to count the solutions, but we need a way to compactly represent and store them all. This of course requires quite a bit of disk space, as there could be e.g. 2^100 solutions, and representing them all, even in a very compact format with lots of smart ideas can take a lot of space — but not necessarily exponential amount. Currently, there is no such system for SMT, and my understanding is that only the d4 model counter can do this on SAT/CNF problems, thanks to its proof checking system, in part thanks to Randal Byrant. Once Ganak can output a proof, it will also be able to do this.

All in all, there is a very large gap between “find if there is exactly one solution” and “enumerate all solutions” — even though I have seen these two notions being mixed up a few times. The first might take only a few seconds to solve, while the other might not even be feasible, because compactly representing all solutions may be too expensive in terms of space (and that’s not even discussing time).

One aspect to keep in mind is that often, one does not need all solutions. For example, if one only wants to find a good set of example solutions, then it is possible to use uniform-like samplers, that give a “somewhat uniform” set of example solutions from the solution space (without guarantees of uniformity). A good tool for this is cmsgen for CNF/SAT problems. If one needs a guaranteed uniform set of samples (to be exact, a probabilistically approximately uniform sample), then unigen is the way to go. Obviously, it’s quite easy to find a uniform sample once we have an enumeration of all solutions — simply pick a random one from the whole set — but that’s way more expensive than running unigen.

While all of the above is about counting, it’s often the case that one wants to optimize for something within the solution space. Basically, we have some kind of objective function that we want to optimize for (e.g. maximize profit, minimize loss) , and so we are looking for a solution that maximizes/minimizes some property. Of course, once we have done model enumeration, it’s quite easy to do this — simply run the objective function on all solutions, and pick the best! But that’s really hard. Instead, one can formulate the problem as a so-called MaxSAT or an SMT problem with an objective function. These systems run some really smart algorithms to significantly cut down search time, and even often keep a “best so far” solution around, so we can early-abort them and still get some kind of “best so far” solution.

All in all, it’s extremely important to figure out what one actually needs, because there are vast gaps in complexity between the problems (and corresponding algorithms) above. Even between something like approximate and exact counting, the gap is gigantic, as there are huge swaths of problems that are almost trivial to count approximately, but essentially impossible to exactly count with current technology:

Here, the green line is a tool that changes its behaviour from exact to approximate model counting after 1800 seconds of solving, and the number of solved instances jumps significantly. Notice that the red line, the original system it runs for 1800s, is the best in class here, by a wide margin, and still the approximate counting that Ganak+ApprocMC switches into shows a massive difference.