A simplistic simplex solver for checking satisfiability of a set of equations.
There are some encodings for different systems in the examples folder:
$ clingo-lpx -c n=132 encoding-lp.lp tai4_4_1.lp
clingo-lpx version 1.1.0
Reading from encoding-lp.lp ...
Solving...
Answer: 1
[...]
Assignment:
(1,1)=132 (1,2)=0 (1,3)=71 (1,4)=69 \
(2,1)=19 (2,2)=98 (2,3)=126 (2,4)=28 \
(3,1)=60 (3,2)=98 (3,3)=0 (3,4)=132 \
(4,1)=132 (4,2)=98 (4,3)=21 (4,4)=28
SATISFIABLE
$ clingo-dl -c n=132 encoding-dl.lp tai4_4_1.lp
[...]
$ clingcon -c n=132 encoding-casp.lp tai4_4_1.lp
[...]
$ clingo -c n=132 encoding.lp tai4_4_1.lp
[...]
Precompiled packages are available:
- https://anaconda.org/potassco/clingo-lpx
- https://anaconda.org/conda-forge/clingo-lpx
- https://pypi.org/project/clingo-lpx/
- https://launchpad.net/~potassco/+archive/ubuntu/stable
To install the conda packages, please install miniconda first. Note that packages from the conda-forge channel offer better performance than the ones from the potassco channel.
The system supports &sum constraints over rationals with relations among <=, >=, and =.
The elements of the sum constraints and terms of guards must be linear expressions.
Quoted strings can be used to represent decimal numbers of arbitrary precision.
Terms can be nested using operators +, -, *, /.
Usage of multiplication and division is limited.
Only expressions of form c * t, t * c, and t / c are accepted
where c must not refer to variables and must be non-zero in the latter case.
If functions are used as variable names, operators +, -, *, / in their arguments are evaluated as well.
There is no special handling of strings for function arguments though.
For example, the following program is accepted:
{ x }.
&sum { 2*var(1+2) } = "0.3".
&sum { var(3) } <= 3 * ("0.75"*z) :- x.
&sum { var(3); (100*y)/2 } <= 0 :- not x.
Furthermore, &dom constraints are supported, which are shortcuts for &sum constraints.
Terms in braces must be numbers and the right-hand-side must be a variable.
The program
{ x }.
&dom { 1..2 } = x.
is equivalent to
{ x }.
&sum { x } >= 1.
&sum { x } <= 2.
Another shortcut (for compatibility with clingo-dl) are &diff constraints.
The same relations as for &sum constraints are accepted.
Terms in braces must should be variables and the right-hand-side should be a number.
The program
{ x }.
&diff { a-b } <= 5.
is equivalent to
{ x }.
&sum { a-b } <= 5.
When option --strict is passed to the solver, then also strict constraints are supported:
{ x }.
&sum { x } > 1.
&sum { x } < 2.
The assignment will then contain an epsilon component for each variable.
For example, with the above program, x>=1+e will appear in the output.
This feature could also be used to support constraints in rule bodies and the != relation;
neither is implemented at the moment.
Finally, the solver supports &minimize and &maxmize objectives where the former is a shortcut for the latter negating coefficients.
The terms between the braces have the same syntax as for &sum constraints.
However, objectives do not have a guard.
For example, the following objective is accepted:
&maximize { 2*x; -2*y }.
By default, the optimal objective value is reported w.r.t. a stable model.
Using option --objective=global together with --models=0 can be used to enumerate globally optimal solutions.
It is also possible to give a step value requiring the next objective to be greater than or equal to the current one plus the step value.
In strict mode with option --strict, it is possible to use a symbolic epsilon value as step value,
that is, by passing option --objective=global,e.
| Option | Description |
|---|---|
--[no-]strict |
Enable support for strict constraints. |
--[no-]propagate-conflicts |
Add binary clauses for conflicting bounds involving the same variable. |
--[no-]propagate-bounds |
Enable propagation of conflicting bounds. The current algorithm should be considered preliminary. It is neither as exhaustive as it could be nor is it very efficient. |
--objective={local,global[,step]} |
Configure how to treat the objective function. Values local and global compute optimal assignments w.r.t. to one and all stable models, respectively. When computing global optima, it is also possible to give a step value requiring the next objective to be greater than or equal to the current one plus the step value. In strict mode with option --strict, it is possible to use a symbolic epsilon value as step value, that is, by passing option --objective=global,e. |
--select={none,match,conflict} |
Configure the sign heuristic for linear constraints. It can be set to none to use the sign heuristic of the ASP solver, match to make literals true whenever the corresponding constraint does not violate the current assignment, or conflict to do the opposite. |
--store={no,partial,total} |
Configure whether to maintain satisfying assignments when backtracking. Value partial and total determine whether this is done w.r.t. to partial or total propagation fixed points. The latter is especially interesting when enumerating models to reduce the number of pivots. |
--[no-]enable-python |
Enable Python script tags. Only works when running the python module, e.g., python -m clingolpx. |
To compile and profile the package, cmake, gperftools, clingo, and a C++ compiler supporting C++17 have to be installed. All these requirements can be installed with conda-forge.
conda create -n profile -c conda-forge cmake libflint clingo cxx-compiler gperftools
conda activate profile
cmake -B build -DCMAKE_BUILD_TYPE=RelWithDebInfo -DCLINGOLPX_PROFILE=ON
cmake --build buildThe resulting binary can then be profiled using the following calls:
CPUPROFILE_FREQUENCY=1000 ./build/bin/clingo-lpx examples/encoding-lp.lp examples/tai4_4_1.lp --stats -c n=132 -q 0
google-pprof --gv ./build/bin/clingo-lpx clingo-lpx-solve.prof- "Integrating Simplex with
DPLL(T)" by Bruno Dutertre and Leonardo de Moura - "SPASS-SATT: A CDCL(LA) Solver" by Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach
The project currently uses FLINT for arithmetics.
Alternatively, the slower but more lightwight IMath library can be used when configuring with CLINGOLPX_MATH_LIBRARY=imath.
Furthermore, note that IMath uses the MIT and FLINT the LGPL license.