My research is currently focused on analyzing infeasible constraint systems. Specifically, I have developed algorithms for extracting information about their infeasibility in the form of Minimal Unsatisfiable Subsets (MUSes) and Minimal Correction Sets (MCSes) of constraints in two tools, CAMUS and MARCO, as well as autarkies, which are independently satisfiable subsets of constraints.
These algorithms can be seen as tools for exploring unsatisfiable constraint systems, which have applications from planning and scheduling to microprocessor design verification. I have applied CAMUS to two digital logic verification tasks: an automated equivalence checker for Verilog with Zaher Andraus, and a logic error diagnosis tool with Sean Safarpour and others at the University of Toronto.
Seeing the value of cardinality constraints in CAMUS, my student Jordyn Maglalang and I developed a "cardinality solver" we call MiniCARD as an extension of MiniSAT. Source code for MiniCARD is available on Github.
I have also contributed to the development of Saucy, a tool for finding graph automorphisms. It has been used in systems that automatically find and break symmetries in constraint satisfaction problems to aid constraint solvers by reducing the size of the search tree.
I am also a semi-official maintainer of AMUSE (though I did not develop it), a tool for extracting an approximation of an MUS from a Boolean CNF instance. Please contact me if you would like a binary distribution of AMUSE.
And of course, feel free to contact me with questions or comments about any of my research or publications.