ModSAT is "SAT Modulo SAT" solver - that is, like a SAT Modulo Theory solver, but where the `theory' is itself Boolean satisfiability.
There are several reasons why we might want to solve a SAT instance modulo another SAT instance (or, recursively, modulo SAT modulo SAT modulo SAT...). The first is that if we are trying to solve an instance with known, `modular' structure (.i.e., the instance is composed of several CNFs, each of which share relatively few variables with each other), then the theories in this SAT modulo SAT solver are a way of capturing and exploiting that structure (by improving memory locality). One very common example of such `modular' instances is anything produced by unrolling a transition function, such as during bounded model checking. However, since in general most things that human design have some degree of modularity built in, many types of SAT instances produced by translating real-world problems into CNF will also have such structure - for example, software verification instances (even before unrolling loops) will generally produce a CNF with modular structure.
You can get source for the current release (based on Minisat 2.2) here: source code (for previous versions, look here). This initial release is a cleaned up, simplified version of the one that I am currently experimenting with; it is packaged with a very simple incremental bounded model checker. This bounded model checker may not be particularly fast - it is just intended to provide an easy source of modular SAT instances with which to test out ModSAT. Also note that this still a beta release; although I have tested it, it most likely has bugs, and it isn't yet as heavily optimized as it could be.
Please send any questions, concerns or comments to Sam Bayless