Research Software

Model Checking

• MCSAT: A SAT-based bounded and unbounded model checker.

  
  

Boolean Satisfiability

• CQuest: A state of the art SAT solver, that ranked among the best 10 performers in the industrial category for the 2004 SAT competition.

• JQuest2: A state of the art SAT solver, implemented in Java, that ranked among the best 10 performers in the industrial category for the 2003 SAT competition.

• JQuest: A state of the art SAT solver, implemented in Java, inspired in GRASP and zChaff, but utilizing improved data structures.

• GRASP: The source code for GRASP, an algorithmic framework for solving instances of the Propositional Satisfiability (SAT) problem. GRASP implements several search pruning techniques for solving SAT, including non-chronological backtracking, clause recording, identification of necessary assignments, among others. (See the CP'00, EPIA'99, DATE'99, IWBP'98, IWLS'97, ICCAD'96 and ICTAI'96 papers, and my Ph.D. dissertation for additional details.)
  I maintain a web page for the GRASP SAT solver.
  (Please check the GRASP page for updated versions of the code.)

• nsat: The executable of a backtrack search algorithm for the Propositional Satisfiability problem. Consists of GRASP and a front-end for reading instances in the DIMACS format. (See the CP'00, EPIA'99, DATE'99, IWBP'98, IWLS'97, ICCAD'96 and ICTAI'96 papers, and my Ph.D. dissertation for additional details.)
  I maintain a web page for the GRASP SAT solver.

  
  

Boolean Optimization

• bsolo: A 0-1 Integer Linear Programming (ILP) algorithm. bsolo is a branch-and-bound algorithm for solving 0-1 ILPs, and it is built on top of the GRASP SAT algorithm. bsolo provides in a single algorithmic framework the search pruning ability of GRASP (e.g. by using non-chronological backtracking and clause recording) and the ability for bounding the search (e.g. by identifying lower/upper bound estimates on the value of the cost function). BSOLO is targeted at solving instances of the Binate Covering Problem (BCP). (See the ECAI'00, DATE'00, Ai-MATH'00, IWLS'98 and ICTAI'97 papers for additional details.)
  There exists a web page for the BSOLO 0-1 ILP/BCP solver.

• min-prime: A 0-1 Integer Linear Programming (ILP) algorithm for computing minimum-size prime implicants of boolean functions. The ILP algorithm is built on top of the GRASP SAT algorithm. (See the ICTAI'97, CTC'97 and IWLS'97 papers on prime implicants for additional details.)

  
  

Circuit Satisfiability

• CGRASP: The source code for CGRASP, a SAT solver for combinational circuits built on top of GRASP. CGRASP was built on top of the most recent version of GRASP, which implements a generalized form of recursive learning. (See the SBCCI'99, ILWS'99 and the two DATE'99 papers for additional details.)
  There exists a web page for the CGRASP circuit SAT solver.

  
  

EDA Applications

• rid-grasp: A SAT-based algorithm for Redundancy removal and IDentification (RID) in combinational circuits. (See the CTC'97 and IWLS'97 papers for additional details.)

• tg-grasp: A SAT-based algorithm for Automatic Test Pattern Generation (ATPG) of combinational circuits. (See the FTCS'97 paper for additional details.)

• tg-leap: An efficient structural Automatic Test Pattern Generation (ATPG) tool for combinational circuits. (See the DAC'94 paper and my Ph.D. dissertation for additional details.)

• ta-leap: An efficient Timing Analysis (TA) tool for combinational circuits using floating-mode sensitization. (See the ISCAS'94 paper and my Ph.D. dissertation for additional details.)

• sta: A Timing Analysis (TA) tool for combinational circuits based on SAT and static sensitization. The back-end SAT solver used by this tool implements some forms of non-chronological backtracking. (See the Euro-DAC'93 paper for additional details.)

Scripts

• scripts: Scripts used for converting formats, and/or interfacing SAT solvers.