Clingcon

Jul 20, 2023

Extension of clingo to handle constraints over integers

Clingcon is an answer set solver for constraint logic programs, building upon the answer set solver clingo. It extends the high-level modeling language of ASP with constraint solving capacities. Constraints over finite domain integer variables can be used in logic programs. Clingcon adopts state-of-the-art techniques from the area of SMT, like conflict-driven learning and theory propagation. It uses lazy nogood and variable generation on the order encoding and features several preprocessing techniques.



Checkout these related ports:
  • Zn_poly - C library for polynomial arithmetic
  • Zimpl - Language to translate the LP models into .lp or .mps
  • Zegrapher - Software for plotting mathematical objects
  • Zarray - Dynamically typed N-D expression system based on xtensor
  • Z3 - Z3 Theorem Prover
  • Yices - SMT solver
  • Yacas - Yet Another Computer Algebra System
  • Xtensor - Multi-dimensional arrays with broadcasting and lazy computing
  • Xtensor-python - Python bindings for xtensor
  • Xtensor-io - Xtensor plugin to read/write images, audio files, numpy npz and HDF5
  • Xtensor-blas - BLAS extension to xtensor
  • Xspread - Spreadsheet program for X and terminals
  • Xppaut - Graphical tool for solving differential equations, etc
  • Xplot - X11 plotting package
  • Xlife++ - XLiFE++ eXtended Library of Finite Elements in C++