SatEEn

Contents

• SatEEn (SAT Enumeration Engine) is an SMT (Satisfiability Modulo Theories) solver that deals with Quantifier-Free Linear Arithmetic Logic and Quantifier-Free Difference Logic. SatEEn combines a SAT solver CirCUs and theory solvers. SatEEn adopts the simplex based algorithm for Linear Arithmetic Logic and uses finite instantiation method adaptively for Difference Logic. As an application, it has been applied to Constrained Random Simulation in Cadence simulator. SatEEn has been developed by VLSI/CAD Research Group in University of Colorado at Boulder. The current members who are working on SatEEn are Hyondeuk Kim, HoonSang Jin (Cadence Design Systems), Hyojung Han, and Fabio Somenzi.


• SatEEn won first places in QF_LIA and QF_IDL divisions and second place in QF_RDL division of SMT-COMP'09. The detailed results can be found in SMT-COMP'09.


• The SatEEn Group


• Getting SatEEn-1.0: SatEEn-1.0 is included in CUSP-1.1


• Getting SatEEn-3.5


• Getting SMT benchmarks

Publications

• "Efficient Term ITE Conversion for Satisfiability Modulo Theories", H. Kim, F. Somenzi, H. Jin. Twelfth International Conference on Theory and Applications of Satisfiability Testing (SAT'09) [pdf]


• "On-the-Fly Clause Improvement", H. Han, F. Somenzi. Twelfth International Conference on Theory and Applications of Satisfiability Testing (SAT'09) [pdf]


• "Application of Formal Word-Level Analysis to Constrained Random Simulation", H. Kim, H. Jin, K. Ravi, P. Spacek, J. Pierce, B. Kurshan, F. Somenzi. 20th International Conference on Computer Aided Verification (CAV'08) [pdf]


• "Alembic: An efficient algorithm for CNF preprocessing", H. Han, F. Somenzi. Proceedings of the Design Automation Conference (DAC'07) [pdf]


• "Disequality Management in Integer Difference Logic via Finite Instantiations", H. Kim, H. Jin, F. Somenzi. Journal on Satisfiability, Boolean Modeling and Computation (JSAT'07) [pdf]


• "Finite Instantiations for Integer Difference Logic", H. Kim, F. Somenzi. International Conference on Formal Methods in Computer Aided Design (FMCAD'06) [pdf]


• "Strong conflict analysis for propositional satisfiability", H. Jin, F. Somenzi. Proceedings of the conference on Design, automation and test in Europe (DATE'06) [pdf]


• "Efficient conflict analysis for finding all satisfying assignments of a Boolean circuit", H. Jin, H. Han, F. Somenzi. International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'05) [pdf]

Comments, suggestions, complaints