Skip to main content
University of Nebraska Omaha logo University of Nebraska Omaha
APPLY MY UNO DIRECTORY

Students Faculty Staff Community
University of Nebraska Omaha logo
College of Information Science & Technology NLPKR Lab
APPLY MY UNO DIRECTORY
Students Faculty Staff Community
  • Research Backback to Main menu
    • Research Projects
    • Verifying ASP
    • Optimizations in ASP
  • Publications Backback to Main menu
    • Lierler, DBLP
    • Fandinno, DBLP
  • Software Backback to Main menu
    • Anthem-P2P
    • AspCCGtk
    • Cmodels
    • Cmodels-Diff
    • DualGrounder
    • EZSMT
    • PPattach
    • PREDICTOR
    • PROJECTOR
    • Sup
    • Text2ALM
    • Text2Drs
  • Teaching
  • Members

EZSMT

  1. UNO
  2. NLPKR Lab
  3. Software
  4. EZSMT

EZSMT version 3

EZSMT version 3 is a constraint answer set programming system that performs processing of logic programs with constraints using Satisfiability Modulo Theories (SMT) solving technology. It takes a program written in a Gringo 5 compatible input language extended with special theory atoms capable to capture constraints supported by EZSMT. It then translates this program into formulas written in SMT-LIB, and calls an SMT solver to compute program's answer sets. EZSMT-3 supports four kinds of constraints:

  • integer linear,
  • real linear constraints,
  • integer difference, and
  • mixed integer/real linear.

In addition, it supports optimization statements.

The github home of the system contains documentation, examples, and code of the system:
https://github.com/ylierler/ezsmtv3

Theoretical and practical groundings for EZSMT version 3 can be found in the manuscript titled "EZSMT Version 3, Matured" by Dhakal, Lierler, and Wilson posted here.

EZSMT version 2 or EZSMTPlus

EZSMT version 2.0.0 is available for download here (under GPLv3).

Download

Unlike version 3 of the system, EZSMT-2 takes a program written in EZCSP and produces an SMT-LIB compliant program. The resultant program can be run on Satisfiability Modulo Theories solvers such as CVC4, Z3, and Yices. EZSMT used EZCSP, Gringo, and CMODELS to perform its transformation procedures.

README file is present within the download content. In copmairson to its earlier version, EZSMT version 2.0.0 is able to process non-tight programs, enumerate multiple solutions, process programs with linear and nonlinear constraints over mixed real and integer variables (Note that it is compatible with Gringo version 4.5.3).

Theoretical and practical groundings for EZSMT version 2.0.0 can be found in:

  • Da Shen and Yuliya Lierler. SMT-based Constraint Answer Set Solver EZSMT+ for Non-tight Programs (PDF). 16th International Conference on Principles of Knowledge Representation and Reasoning (KR), 2018. Benchmarks discussed in this paper are posted here. Complete table presenting results on all experimental analyses discussed in the paper is posted here.
  • Da Shen and Yuliya Lierler. SMT-based Answer Set Solver CMODELS-DIFF (System Description) (PDF). 34th International Conference on Logic Programming (ICLP), 2018.

EZSMT version 1

Earlier version of the system EZSMT version 1.0.0 is available for download here (under GPLv3):

Download

Theoretical and practical groundings for EZSMT version 1.0.0 can be found in:

  • Benjamin Susman and Yuliya Lierler. System Description: SMT-based Constraint Answer Set Solver EZSMT (PDF). 32nd International Conference on Logic Programming (ICLP), 2016.
  • Yuliya Lierler and Benjamin Susman. Constraint Answer Set Programming versus Satisfiability Modulo Theories (PDF). 25th International Joint Conference on Artificial Intelligence (IJCAI) , 2016.
  • Benjamin Susman. The EZSMT Solver: Constraint Answer Set Solving meets SMT (PDF). Master Thesis, University of Nebraska Omaha, 2016.
  • Yuliya Lierler and Benjamin Susman. Constraint Answer Set Programming versus Satisfiability Modulo Theories Or Constraints versus Theories (PDF). 3rd Workshop on Grounding, Transforming, and Modularizing Theories with Variables (GTTV 2015), 2015.

Comments, questions, and/or bugs can be reported to Yuliya Lierler

Contact Us

  • Yuliya Lierler: ylierler@unomaha.edu

College of Information Science & Technology

Contact Us
  • College of Information Science & Technology
  • 172 Peter Kiewit Institute
  • 1110 South 67th Street
  • Omaha, NE 68182   map
  • 402.554.2380
  • Contact Us
Social media
College Resources
  • Advising
  • Jobs and Internships
  • Research
  • News and Events
  • IS&T Technology Systems and Facilities
Peter Kiewit Institute

Next Steps

  • Visit UNO
  • Request Information
  • Apply for Admission
  • The UNO Advantage
  • Our City (Omaha)

Just For You

  • Future Students
  • Current Students
  • Work at UNO
  • Faculty and Staff
  • A-Z List

Popular Services and Resources

  • my.unomaha.edu
  • Academic Calendar
  • Campus Buildings & Maps
  • Library
  • Pay Your Bill
  • Course Catalogs
  • Internships & Career Development
  • The Maverick Store
  • MavCARD Services
  • Military-Connected Resource Center
  • Speech Center
  • Writing Center
  • Human Resources
  • Center for Faculty Excellence

Affiliates

  • University of Nebraska System
  • NU Foundation
  • Buffett Early Childhood Institute
  • Daugherty Water for Food Institute
  • National Strategic Research Institute
  • Peter Kiewit Institute
  • Rural Prosperity Nebraska
  1. University Policies
  2. Privacy Statement
  3. Accessibility
  1. 402.554.2800
University of Nebraska Omaha
University of Nebraska Omaha, 6001 Dodge Street, Omaha, NE, 68182
  • ©  
  • Emergency Information Alert
  • MavsReport

Social Media

Omaha Skyline

Our Campus. Otherwise Known as Omaha.

The University of Nebraska does not discriminate based on race, color, ethnicity, national origin, sex, pregnancy, sexual orientation, gender identity, religion, disability, age, genetic information, veteran status, marital status, and/or political affiliation in its education programs or activities, including admissions and employment. The University prohibits any form of retaliation taken against anyone for reporting discrimination, harassment, or retaliation for otherwise engaging in protected activity. Read the full statement.