This package provides a range of SAT solvers, including the sequential lingeling and its parallel variants plingeling and treengeling. A bounded model checker is also included.

IT++ is a C++ library of mathematical, signal processing and communication classes and functions. Its main use is in simulation of communication systems and for performing research in the area of communications. The kernel of the library consists of generic vector and matrix classes, and a set of accompanying routines. Such a kernel makes IT++ similar to MATLAB, GNU Octave or SciPy.

LinAsm is collection of very fast and SIMD optimized assembly written libraries for x86-64.

It implements many common and widely used algorithms for array manipulations: searching, sorting, arithmetic and vector operations, unit conversions; fast mathematical and statistic functions; numbers and time converting algorithms; finite impulse response (FIR) digital filters; spectrum analysis algorithms, Fast Hartley transformation; CPU cache friendly functions and extremely fast abstract data types (ADT) such as hash tables b-trees, and much more.

GNU Octave is a high-level interpreted language that is specialized for numerical computations. It can be used for both linear and non-linear applications and it provides great support for visualizing results. Work may be performed both at the interactive command-line as well as via script files.

This package provides a tool to determine the backbone of a satisfiable formula. The backbone is the set of literals that are set to true in all models.

muParser is an extensible high performance math parser library. It is based on transforming an expression into a bytecode and precalculating constant parts of it.

Numdiff compares files line by line and field by field, ignoring small numeric differences and differences in numeric formats.

This package provides a Django front end for Mathics3.

SCOTCH is a set of programs and libraries which implement the static mapping and sparse matrix reordering algorithms developed within the SCOTCH project. Its purpose is to apply graph theory, with a divide and conquer approach, to scientific computing problems such as graph and mesh partitioning, static mapping, and sparse matrix ordering, in application domains ranging from structural mechanics to operating systems or bio-chemistry.

PDELab is a partial differential equations solver toolbox built on top of DUNE, the Distributed and Unified Numerics Environment.

Z3 is a theorem prover and satisfiability modulo theories (SMT) solver. It provides a C/C++ API, as well as Python bindings.

This package uses PLT trampolines to provide a BLAS and LAPACK demuxing library.

SPEX is a set of routines for sparse exact linear algebra. It contains the SPEX Left LU library for computing a sparse exact left-looking LU factorization for solving unsymmetric sparse linear systems.

The dune-subgrid module marks elements of another hierarchical dune grid. The set of marked elements can then be accessed as a hierarchical dune grid in its own right. Dune-Subgrid provides the full grid interface including adaptive mesh refinement.

DUNE, the Distributed and Unified Numerics Environment is a modular toolbox for solving partial differential equations (PDEs) with grid-based methods. It supports the easy implementation of methods like Finite Elements (FE), Finite Volumes (FV), and also Finite Differences (FD).

This package contains the basic DUNE grid classes.

PETSc, pronounced PET-see (the S is silent), is a suite of data structures and routines for the scalable (parallel) solution of scientific applications modeled by partial differential equations.

GNU Units converts numeric quantities between units of measure. It can handle scale changes through adaptive usage of standard scale prefixes (micro-, kilo-, etc.). It can also handle nonlinear conversions such as Fahrenheit to Celsius. Its interpreter is powerful enough to be used effectively as a scientific calculator.

TypeTree is a template library for constructing and operating on statically typed trees of objects.

PDELab is a partial differential equations solver toolbox built on top of DUNE, the Distributed and Unified Numerics Environment.

GKlib is a library of various helper routines and frameworks used by software from KarypisLab, such as METIS.

BTF (Block Triangular Form) is a C library for permuting a matrix into block upper triangular form.

AIGER is a format, library and set of utilities for AIGs. The focus is on conversion utilities and a generic reader and writer API.

The OSQP (Operator Splitting Quadratic Program) solver is a numerical optimization package for solving convex quadratic programs.

It uses a custom ADMM-based first-order method requiring only a single matrix factorization in the setup phase. All the other operations are extremely cheap. It also implements custom sparse linear algebra routines exploiting structures in the problem data.

The proof checker DRAT-trim can be used to check whether a propositional formula in the DIMACS format is unsatisfiable. Given a propositional formula and a clausal proof, DRAT-trim validates that the proof is a certificate of unsatisfiability of the formula.