[go: up one dir, main page]
Skip to content

Commit

Permalink
SLIME SO
Browse files Browse the repository at this point in the history
  • Loading branch information
Oscar Riveros committed Oct 7, 2019
1 parent e6f4687 commit 43e882f
Show file tree
Hide file tree
Showing 29 changed files with 517 additions and 278 deletions.
13 changes: 13 additions & 0 deletions LICENSE
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,16 @@
SLIME SO -- Copyright (c) 2019, Oscar Riveros, oscar.riveros@peqnp.science, Santiago, Chile. https://maxtuno.github.io/slime-sat-solver

All technology of SLIME SO that make this software Self Optimized is property of Oscar Riveros, oscar.riveros@peqnp.science, Santiago, Chile,
It can be used for commercial or private purposes, as long as the condition of mentioning explicitly
"This project use technology property of Oscar Riveros Founder and CEO of www.PEQNP.science".

Any use that violates this clause is considered illegal.

The above copyright notice and this permission notice shall be included
in all copies or substantial portions of the Software.

Historical Licences:

SLIME -- Copyright (c) 2019, Oscar Riveros, oscar.riveros@peqnp.science, Santiago, Chile. https://maxtuno.github.io/slime-sat-solver

SLIME SAT Solver and The BOOST Heuristic or Variations cannot be used on any contest without express permissions of Oscar Riveros.
Expand Down
11 changes: 11 additions & 0 deletions README.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,17 @@

NOTE: This repository is the development version, for official releases go to https://github.com/maxtuno/slime-sat-solver/releases

SLIME SO: The Self Optimized SAT Solver.
- More Deepness (Solved More Unsolvable Instances).
- Self Optimization.
- Cutting edge technology property of www.PEQNP.science now Open Source.

SLIME 4.2: The most advanced SAT Solver on the planet.
- More performance.
- Pre Release from 5.0 version.
- Chronos property is deleted.
- No randomness is on SLIME.

SLIME 4.1.1:
- More performance.
- Pre Release from 5.0 version.
Expand Down
2 changes: 1 addition & 1 deletion build.sh
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
#!/usr/bin/env bash
echo
echo "SLIME 4.1.1 The most advanced SAT Solver on the planet."
echo "SLIME SO: The Self Optimized SAT Solver by http://www.peqnp.science"
echo
echo "Building..."
echo
Expand Down
4 changes: 4 additions & 0 deletions changes_so.txt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
SLIME SO: The Self Optimized SAT Solver.
- More Deepness (Solved More Unsolvable Instances).
- Self Optimization.
- Cutting edge technology property of www.PEQNP.science now Open Source.
5 changes: 5 additions & 0 deletions changes_v4.2.txt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
SLIME 4.2: The most advanced SAT Solver on the planet.
- More performance.
- Pre Release from 5.0 version.
- Chronos property is deleted.
- No randomness is on SLIME.
252 changes: 138 additions & 114 deletions index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,121 +3,145 @@
---
<body>

<h1>SLIME 4.1.1: The most advanced SAT Solver on the planet.</h1>
<ul>
<li>More performance.</li>
<li>Pre Release from 5.0 version.</li>
</ul>

<img src="media/v4.1.1/SATRace2019_new_instances.png" alt="SLIME 4.1.1 vs CaDiCaL">
<img src="media/v4.1.1/SATRace2019_new_instances_detail.png" alt="SLIME 4.1.1 vs CaDiCaL">
<img src="media/v4.1.1/factoring2018.png" alt="SLIME 4.1.1 vs CaDiCaL">

<h1>SLIME 4.1: The most advanced SAT Solver on the planet.</h1>
<ul>
<li>More performance.</li>
</ul>

<img src="media/v4.1/hard_normal.png" alt="SLIME 4.0 vs SLIME 4.1(XP)">
<img src="media/v4.1/2006_log.png" alt="SLIME 4.1 vs CaDiCaL vs Other">
<img src="media/v4.1/factoring.png" alt="SLIME 4.1 vs CaDiCaL vs Other">

<h1>SLIME 4.0.1: Today the most advanced SAT Solver on the planet.</h1>
<ul>
<li>SLIME 4.0 vs 4.0.1 SAT Race 2006.</li>
<li>Increase general performance and scope of solvable instances.</li>
</ul>

<img src="media/v4/SATRace2016.png" alt="SLIME 4.0 vs SLIME 4.0.1">
<h1>SLIME SO: The Self Optimized SAT Solver.</h1>
<ul>
<li>More Deepness (Solved More Unsolvable Instances).</li>
<li>Self Optimization.</li>
<li>Cutting edge technology property of www.PEQNP.science now Open Source.</li>
</ul>

<h2>Uniform Random 3 SAT Instances SLIME SO (RED) vs CaDiCaL (BLUE) (*Winner of SAT Race 2019*)</h2>
<img src="media/so/3sat.png" alt="SLIME SO vs CaDiCaL">
<img src="media/so/3sat_log.png" alt="SLIME SO vs CaDiCaL">
<img src="media/so/details.png" alt="SLIME SO vs CaDiCaL">

<h1>SLIME 4.2: The most advanced SAT Solver on the planet.</h1>
<ul>
<li>More performance.</li>
<li>Pre Release from 5.0 version.</li>
<li>Chronos property is deleted.</li>
<li>No randomness is on SLIME.</li>
</ul>

<img src="media/v4.2/SATRace2019_new_instances.png" alt="SLIME 4.2 vs CaDiCaL">
<img src="media/v4.2/SATRace2019_new_instances_detail.png" alt="SLIME 4.2 vs CaDiCaL">
<img src="media/v4.2/factoring2018.png" alt="SLIME 4.2 vs CaDiCaL">

<h1>SLIME 4.1.1: The most advanced SAT Solver on the planet.</h1>
<ul>
<li>More performance.</li>
<li>Pre Release from 5.0 version.</li>
</ul>

<img src="media/v4.1.1/SATRace2019_new_instances.png" alt="SLIME 4.1.1 vs CaDiCaL">
<img src="media/v4.1.1/SATRace2019_new_instances_detail.png" alt="SLIME 4.1.1 vs CaDiCaL">
<img src="media/v4.1.1/factoring2018.png" alt="SLIME 4.1.1 vs CaDiCaL">

<h1>SLIME 4.1: The most advanced SAT Solver on the planet.</h1>
<ul>
<li>More performance.</li>
</ul>

<img src="media/v4.1/hard_normal.png" alt="SLIME 4.0 vs SLIME 4.1(XP)">
<img src="media/v4.1/2006_log.png" alt="SLIME 4.1 vs CaDiCaL vs Other">
<img src="media/v4.1/factoring.png" alt="SLIME 4.1 vs CaDiCaL vs Other">

<h1>SLIME 4.0.1: Today the most advanced SAT Solver on the planet.</h1>
<ul>
<li>SLIME 4.0 vs 4.0.1 SAT Race 2006.</li>
<li>Increase general performance and scope of solvable instances.</li>
</ul>

<img src="media/v4/SATRace2016.png" alt="SLIME 4.0 vs SLIME 4.0.1">

<h1>SLIME 4.0: Today the most advanced SAT Solver on the planet.</h1>
<ul>
<li>SLIME vs The Winner of the SAT Race 2019.</li>
<li>Increase performance and scope of solvable instances.</li>
<li>Better performance at 3000 seconds than the winner of the SAT Race 2019 on new Benchmarks.</li>
<li>Better UNSAT solving.</li>
</ul>

<img src="media/v4/SATRace2019_3000s.png" alt="CaDiCaL vs SLIME 4.0">
<img src="media/v4/SATRace2019_3000s_log.png" alt="CaDiCaL vs SLIME 4.0">
<img src="media/v4/SLIMEvsCaDiCaL.png" alt="CaDiCaL vs SLIME 4.0">

<h1>SLIME 3.1.1: The Unofficial State of The Art</h1>
<ul>
<li>SLIME vs The Winners of the SAT Race 2019.</li>
</ul>

<img src="media/v3.1.1/5000s.png" alt="CaDiCaL vs MapleLCMDiscChronoBT-DL-v3 vs SLIME 3.1.1">

<img src="media/v3.1.1/vs.png" alt="CaDiCaL vs MapleLCMDiscChronoBT-DL-v3 vs SLIME 3.1.1">
<img src="media/v3.1.1/result.png" alt="CaDiCaL vs MapleLCMDiscChronoBT-DL-v3 vs SLIME 3.1.1">

<h1>SLIME 3.1: The Unofficial State of The Art</h1>
<ul>
<li>Support long term executions without overflow on counters and variables.</li>
<li>The State of The Art Performance.</li>
</ul>

<img src="media/v3/satrace2019_alone.png" alt="SAT Race 2019 (Secondhalf)">
<img src="media/v3/satrace2019_alone_log.png" alt="SAT Race 2019 (Secondhalf)">
<img src="media/v3/satrace2019_alone_rep.png" alt="SAT Race 2019 (Secondhalf)">

<h1>SLIME 3.0: The Unofficial State of The Art</h1>
<ul>
<li>Implementation of Alternating Dual BOOST Heuristic.</li>
<li>The State of The Art Performance.</li>
</ul>

<img src="media/v3/satrace2019.png" alt="SAT Race 2019 (Secondhalf)">
<img src="media/v3/satrace2019_log.png" alt="SAT Race 2019 (Secondhalf)">
<img src="media/v3/satrace2019_rep.png" alt="SAT Race 2019 (Secondhalf)">

<img src="media/v3/satrace2006.png" alt="SAT Race 2006">

<h1>SLIME 2.2: A Free World Class Multiplatform High Performance SAT Solver</h1>
<ul>
<li>Windows support - include a precompiled executable</li>
<li>usage: slime_cli cnf-file [sat-model-file] [unsat-proof-file]</li>
<li>2.0 performance</li>
</ul>

<h1>SLIME 2.1: A Free World Class High Performance SAT Solver</h1>
<ul>
<li>Full ANSI C++
<li>Remove ZLib dependency
<li>Extreme simplification of unused components
<li>2.0 performance
<li>More compatibility with all OS. (Full Raspbian Compatibility)</li>
</ul>

<h1>SLIME 2.0: A Free World Class High Performance SAT Solver</h1>
<h3>SAT Race 2015</h3>
<ul>
<li>v1.0 PAR-2 605079.2646</li>
<li>v2.0 PAR-2 591812.0663</li>
</ul>

(The solvers will ranked using the PAR-2 scheme: The score of a solver is defined as the sum of all runtimes for solved instances + 2*timeout for unsolved instances, lowest score wins.)

<img src="media/v2/results.png" alt="SAT Race 2006">
<img src="media/v2/default.png" alt="SAT Race 2015">
<img src="media/v2/log.png" alt="SAT Race 2006">

<h1>SLIME: A Minimal Heuristic to Boost SAT Solving</h1>
<br>

On CDCL Based SAT Solvers the trail size is strictly related to progress or to the total conflicts on the current assignment,
such that if the trail size is the same that the number of variables, then current assignment is valid.

On the other hand, in the selection of the current variable it is necessary to assign a predetermined polarity to the resulting literal, which in most implementations is a predefined value.

SLIME implement a simple heuristic with minimal complexity, that correlated the trail size and the polarity of the current variable to assign.

The selection of variable is not related to trail size, this decouple the both concepts.

<br>
<br>

<embed src="slime/doc/slime.pdf" type="application/pdf" width="100%" height="600px"/>
<ul>
<li>SLIME vs The Winner of the SAT Race 2019.</li>
<li>Increase performance and scope of solvable instances.</li>
<li>Better performance at 3000 seconds than the winner of the SAT Race 2019 on new Benchmarks.</li>
<li>Better UNSAT solving.</li>
</ul>

<img src="media/v4/SATRace2019_3000s.png" alt="CaDiCaL vs SLIME 4.0">
<img src="media/v4/SATRace2019_3000s_log.png" alt="CaDiCaL vs SLIME 4.0">
<img src="media/v4/SLIMEvsCaDiCaL.png" alt="CaDiCaL vs SLIME 4.0">

<h1>SLIME 3.1.1: The Unofficial State of The Art</h1>
<ul>
<li>SLIME vs The Winners of the SAT Race 2019.</li>
</ul>

<img src="media/v3.1.1/5000s.png" alt="CaDiCaL vs MapleLCMDiscChronoBT-DL-v3 vs SLIME 3.1.1">

<img src="media/v3.1.1/vs.png" alt="CaDiCaL vs MapleLCMDiscChronoBT-DL-v3 vs SLIME 3.1.1">
<img src="media/v3.1.1/result.png" alt="CaDiCaL vs MapleLCMDiscChronoBT-DL-v3 vs SLIME 3.1.1">

<h1>SLIME 3.1: The Unofficial State of The Art</h1>
<ul>
<li>Support long term executions without overflow on counters and variables.</li>
<li>The State of The Art Performance.</li>
</ul>

<img src="media/v3/satrace2019_alone.png" alt="SAT Race 2019 (Secondhalf)">
<img src="media/v3/satrace2019_alone_log.png" alt="SAT Race 2019 (Secondhalf)">
<img src="media/v3/satrace2019_alone_rep.png" alt="SAT Race 2019 (Secondhalf)">

<h1>SLIME 3.0: The Unofficial State of The Art</h1>
<ul>
<li>Implementation of Alternating Dual BOOST Heuristic.</li>
<li>The State of The Art Performance.</li>
</ul>

<img src="media/v3/satrace2019.png" alt="SAT Race 2019 (Secondhalf)">
<img src="media/v3/satrace2019_log.png" alt="SAT Race 2019 (Secondhalf)">
<img src="media/v3/satrace2019_rep.png" alt="SAT Race 2019 (Secondhalf)">

<img src="media/v3/satrace2006.png" alt="SAT Race 2006">

<h1>SLIME 2.2: A Free World Class Multiplatform High Performance SAT Solver</h1>
<ul>
<li>Windows support - include a precompiled executable</li>
<li>usage: slime_cli cnf-file [sat-model-file] [unsat-proof-file]</li>
<li>2.0 performance</li>
</ul>

<h1>SLIME 2.1: A Free World Class High Performance SAT Solver</h1>
<ul>
<li>Full ANSI C++
<li>Remove ZLib dependency
<li>Extreme simplification of unused components
<li>2.0 performance
<li>More compatibility with all OS. (Full Raspbian Compatibility)</li>
</ul>

<h1>SLIME 2.0: A Free World Class High Performance SAT Solver</h1>
<h3>SAT Race 2015</h3>
<ul>
<li>v1.0 PAR-2 605079.2646</li>
<li>v2.0 PAR-2 591812.0663</li>
</ul>

(The solvers will ranked using the PAR-2 scheme: The score of a solver is defined as the sum of all runtimes for solved instances + 2*timeout for unsolved instances, lowest score wins.)

<img src="media/v2/results.png" alt="SAT Race 2006">
<img src="media/v2/default.png" alt="SAT Race 2015">
<img src="media/v2/log.png" alt="SAT Race 2006">

<h1>SLIME: A Minimal Heuristic to Boost SAT Solving</h1>
<br>

On CDCL Based SAT Solvers the trail size is strictly related to progress or to the total conflicts on the current assignment,
such that if the trail size is the same that the number of variables, then current assignment is valid.

On the other hand, in the selection of the current variable it is necessary to assign a predetermined polarity to the resulting literal, which in most implementations is a predefined value.

SLIME implement a simple heuristic with minimal complexity, that correlated the trail size and the polarity of the current variable to assign.

The selection of variable is not related to trail size, this decouple the both concepts.

<br>
<br>

<embed src="slime/doc/slime.pdf" type="application/pdf" width="100%" height="600px"/>

</body>
Binary file added media/so/3sat.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added media/so/3sat_log.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added media/so/details.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
2 changes: 1 addition & 1 deletion slime/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${PROJECT_SOURCE_DIR}/lib)
include_directories(. include)
link_directories(${PROJECT_SOURCE_DIR}/lib)

set(CMAKE_CXX_FLAGS "-std=c++98 -O3 -Wno-reorder -Wno-unused-value -D NDEBUG -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -D LOG")
set(CMAKE_CXX_FLAGS "-std=c++11 -O3 -Wno-reorder -Wno-unused-value -D NDEBUG -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -D LOG")

add_library(slime
src/Main.cc
Expand Down
2 changes: 1 addition & 1 deletion slime/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ RCOBJS = $(addsuffix r, $(COBJS))


CXX ?= g++
CFLAGS ?= -ansi -Wno-parentheses
CFLAGS ?= -std=c++11 -Wno-parentheses
LFLAGS ?=

COPTIMIZE ?= -O3
Expand Down
Binary file modified slime/bin/slime_cli-w64.exe.zip
View file
Binary file not shown.
4 changes: 2 additions & 2 deletions slime/include/Dimacs.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,9 +70,9 @@ template <class B, class Solver> static void parse_DIMACS_main(B &in, Solver &S)
}
}
if (vars != S.nVars())
fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of variables.\n");
fprintf(stderr, "c WARNING! DIMACS header mismatch: wrong number of variables.\n");
if (cnt != clauses)
fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of clauses.\n");
fprintf(stderr, "c WARNING! DIMACS header mismatch: wrong number of clauses.\n");
}

// Inserts problem into solver.
Expand Down
31 changes: 7 additions & 24 deletions slime/include/SimpSolver.h
View file
Original file line number Diff line number Diff line change
@@ -1,31 +1,14 @@
/************************************************************************************[SimpSolver.h]
SLIME -- Copyright (c) 2019, Oscar Riveros, oscar.riveros@peqnp.science, Santiago, Chile. - Implementation of the The Booster Heuristic.
SLIME SO -- Copyright (c) 2019, Oscar Riveros, oscar.riveros@peqnp.science, Santiago, Chile. https://maxtuno.github.io/slime-sat-solver
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007, Niklas Sorensson
All technology of SLIME SO that make this software Self Optimized is property of Oscar Riveros, oscar.riveros@peqnp.science, Santiago, Chile,
It can be used for commercial or private purposes, as long as the condition of mentioning explicitly
"This project use technology property of Oscar Riveros Founder and CEO of www.PEQNP.science".
Chanseok Oh's MiniSat Patch Series -- Copyright (c) 2015, Chanseok Oh
Any use that violates this clause is considered illegal.
Maple_LCM, Based on MapleCOMSPS_DRUP -- Copyright (c) 2017, Mao Luo, Chu-Min LI, Fan Xiao: implementing a learnt clause minimisation approach
Reference: M. Luo, C.-M. Li, F. Xiao, F. Manya, and Z. L. , “An effective learnt clause minimization approach for cdcl sat solvers,” in IJCAI-2017, 2017, pp. to–appear.
Maple_LCM_Dist, Based on Maple_LCM -- Copyright (c) 2017, Fan Xiao, Chu-Min LI, Mao Luo: using a new branching heuristic called Distance at the beginning of search
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
The above copyright notice and this permission notice shall be included
in all copies or substantial portions of the Software.
**************************************************************************************************/

#ifndef SLIME_SimpSolver_h
Expand Down
Loading

0 comments on commit 43e882f

Please sign in to comment.