Lsids

[conp-solutions]

This implements the technique presented in the upcoming paper "Designing New Phase Selection Heuristics"

Additionally, I added a switch that allows to disable the technique from the CLI, to measure performance impact more easily.

Finally, I spotted modified behavior when disabling LSIDS, or using the version before the series, and hence, added another commit to fix this.

Output of a test wrt solver behavior:

git clone https://github.com/conp-solutions/mergesat.git mergesat cd mergesat git checkout 960d045d0e4fe7d3f5b3ff3972cddedee31bf5d2 make r -j cp build/release/bin/mergesat mergesat-960d045d0e4fe7d3f5b3ff3972cddedee31bf5d2 # go to unfixed variant git checkout e36cb6020274263014f5c83808565496aa78480f git show -s #commit e36cb6020274263014f5c83808565496aa78480f (HEAD) #Author: Norbert Manthey <nmanthey@conp-solutions.com> #Date: Sun Jun 14 21:42:18 2020 +0200 # # lsids: allow to activate separately # # Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com> make r -j # compare the 2 solvers --- use another input cnf ./tools/check-solver-behavior.sh ~/cnf/sudoku77.cnf.gz "build/release/bin/mergesat -no-lsids" ./mergesat-960d045 #Output of the command #Use input /home/nmanthey/cnf/sudoku77.cnf.gz #Run solver1: 'build/release/bin/mergesat -no-lsids' #Run solver2: './mergesat-960d045' #Run solver 1 ... #Run solver 2 ... #Evaluate ... #Conflicts do not match, 1917 vs 1012 #Decisions do not match, 5069 vs 2999 #Exit code match: 10 # use fixed version git checkout f3cf84282f8a33a6fcdd293f3190193346996049 make r -j # compare fixed version ./tools/check-solver-behavior.sh ~/cnf/sudoku77.cnf.gz "build/release/bin/mergesat -no-lsids" ./mergesat-960d045 #Output #Use input /home/nmanthey/cnf/sudoku77.cnf.gz #Run solver1: 'build/release/bin/mergesat -no-lsids' #Run solver2: './mergesat-960d045' #Run solver 1 ... #Run solver 2 ... #Evaluate ... #Conflicts match: 1012 #Decisions match: 2999 #Exit code match: 10