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 <[email protected]>
#Date:   Sun Jun 14 21:42:18 2020 +0200
#
#    lsids: allow to activate separately
#    
#    Signed-off-by: Norbert Manthey <[email protected]>
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