Open Source Software

My research work is at the intersection of theory and practice. I strongly believe in developing algorithms that can be implemented as it is. This philosophy has not only provided us with strong insights into practical problems but with interesting theoretical questions. With my collaborators, I have developed the following open source softwares that extensively utililze and influence theoretical component of our research.

ApproxMC

ApproxMC is a hashing-based algorithm for approximate discrete integration over finite domains and provides (epsilon,delta) guarantees. This implementation handles the case when the function is implicitely defined by SAT formula. To the best of our knowledge, the current implementation has the best runtime performance among approximate counting algorithms. We are actively improving algorithm as well as implementation and would love to hear your feedback.
Repository: Click Here
Relevant Papers: IJCAI 2016 Constraints 2016 CP 2013

UniGen

UniGen is a hashing-based algorithm to generate uniform samples subject to given set of constraints. The primary application of UniGen is in random stimuli generation for hardware and software verification. The current versioni of the tool has been developed over the years and is parallelizable without losing theoretical guarantees.
Repository: Click Here
Relevant Papers: TACAS 2015 DAC 2014 CAV 2013

WeightMC

WeightMC is hashing-based algorithm for weighted counting (discrete integration) over Boolean domains. It takes a CNF formula and weight function as inputs and returns weighted count. In contrast to previous attempts to develop weighted counting that rely on use of Optimization oracles, WeightMC only uses feasibility oracle. A simple reworking of this algorithm was used by Belle et al to predicate delays in UK transportation network.
Repository: Click Here
Relevant Papers: AAAI 2014

WeightGen

Given a set of constraints and weight function over assignments, WeightGen outputs samples that satisfy constraints according to weight function.
Repository: Click Here
Relevant Papers: AAAI 2014

SMTApproxMC

first approximate model counter that uses word-level hashing functions, and can directly leverage the power of sophisticated SMT solvers. Empirical evaluation over an extensive suite of benchmarks demonstrates the promise of the approach.
Repository: Click Here
Relevant Papers: AAAI 2016

MIS

MIS computes minimal Independent Support for a given CNF formula. The implementation is based on MIS algorithm proposed in our CP'15 paper, which also won the Best Student Paper Award.
Repository: Click Here
Relevant Papers: Constraints 2016 (The CP paper was invited for a Special Issue of Constraints)