| Name | Modified | Size | Downloads / Week |
|---|---|---|---|
| LIPSATrelease1.0.1.zip | 2018-02-02 | 22.8 MB | |
| README | 2018-02-02 | 2.1 kB | |
| Totals: 2 Items | 22.8 MB | 0 |
-------------------------------- LIPSAT release 1.0 (version 042) -------------------------------- LIPSAT is a constraint solver thaty decides the satisfiability of a set of Lukasiewicz Infinitely-valued Probabilistic assignments. This implementation allows one to choose between two types of auxiliary Lukasiewicz Infinitely-valued logic sovers, based on MIP solver SCIP or based on SMT(LA) nsolver YICES. Given a LIP-assignment instance in normal form as input, the program returns a solution, if there is one. The implemented method employs dual Simplex Algorithm with Column Generation. At each iteration, a Lukasiewicz Infinitely- valued logic instance is generated and a solver decides its satisfiability. Copying conditions about psat-minisat can be found in the 'LICENSE', 'LICENSE-minisat' and 'LICENSE-CoinCl' files. To contact the author: marcelo.finger@gmail.com ------------------- Before Installation ------------------- The following packages were required in Ubuntu/Debian distributions for the correct compilation of the sources: - libarmadillo-dev - libgmp-dev - libreadline-dev ------------------- Solver Installation ------------------- You must have in your computer the compilers gcc and g++. The necessary libraries (linux 64bits) are inserted in the package in the lib/ directory. To compile the LIPSAT solver, all you have to do is type, at the root of the distribution directory $ make or, equivalently, $ make LIPSAT.mak To remove all compiled files, just type $ make clean --------------------------- Test Generatir Installation --------------------------- A test generator has been provided to generate the phase-transition curves. To compile the LIPSATTestGenerator, all you have to do is type, at the root of the distribution directory $ make LIPSATTestGenerator.mak ------------------------------------ Using LIPSAT and LIPSATTestGenerator ------------------------------------ See the usage.txt file included in this package.