Validate LBD implementation

[shnarazk]

• [x] check the initial lbd value of various clauses
• [ ] validate update algorithm
• [x] check reduceDB's implemetation
  • [x] monotonicity of the order of clause in learnts
  • [x] reduction rate of the number of stored clauses

[shnarazk]

5d040823

$ stack install && mios-lbd 3-SAT/UF20/uf20-013.cnf 

16 @ 3, 17 @ 3, 19 @ 3, [(0,(0,0)),(1,(-1,1)),(2,(0,-1)),(3,(0,-1)),(4,(0,4)),(5,(1,3)),(6,(0,4)),(7,(0,-1)),(8,(1,2)),(9,(0,4)),(10,(0,4)),(11,(-1,3)),(12,(0,-1)),(13,(0,4)),(14,(0,4)),(15,(0,-1)),(16,(1,3)),(17,(-1,3)),(18,(-1,3)),(19,(-1,3)),(20,(-1,2))]
(3," -> ",1)
[16,17,19]
[-1,-2,-3,-4,5,-6,7,8,9,-10,-11,12,-13,-14,-15,16,-17,-18,-19,-20]

$ mios-lbd 3-SAT/UF20/uf20-015.cnf 
-10 @ 4, 18 @ 4, 19 @ 3, [(0,(0,0)),(1,(-1,1)),(2,(0,-1)),(3,(0,6)),(4,(0,-1)),(5,(0,-1)),(6,(0,-1)),(7,(0,6)),(8,(0,6)),(9,(0,6)),(10,(-1,4)),(11,(0,6)),(12,(0,6)),(13,(0,6)),(14,(1,4)),(15,(0,6)),(16,(0,5)),(17,(-1,4)),(18,(-1,4)),(19,(-1,3)),(20,(-1,2))]
(3," -> ",2)
[-10,18,19]
-3 @ 4, 7 @ 4, 18 @ 4, -14 @ 4, [(0,(0,0)),(1,(-1,1)),(2,(0,-1)),(3,(-1,4)),(4,(0,-1)),(5,(0,5)),(6,(0,-1)),(7,(-1,4)),(8,(0,5)),(9,(0,5)),(10,(-1,4)),(11,(-1,4)),(12,(0,5)),(13,(0,5)),(14,(1,4)),(15,(0,5)),(16,(0,5)),(17,(-1,4)),(18,(-1,4)),(19,(-1,3)),(20,(-1,2))]
(4," -> ",1)
[-3,7,18,-14]
[-1,-2,-3,-4,5,-6,-7,-8,-9,-10,-11,-12,13,14,15,-16,-17,-18,-19,-20]

[shnarazk]

9640cfd -- seems normal

# 2017-09-05T10:25 ; mios lbd:PR#36
# p='', t=1260 on xingu @ 2017-09-05T10:25:31+09:00
"mios-lbd", 1, 100,      0.67
"mios-lbd", 2, 125,      1.14
"mios-lbd", 3, 150,      2.07
"mios-lbd", 4, 175,      6.16
"mios-lbd", 5, 200,      17.22
"mios-lbd", 6, 225,      50.61
"mios-lbd", 7, 250,      146.27
"mios-lbd", 8, "een",    4.84
"mios-lbd", 9, "bmc",    2.81
"mios-lbd", 10, "38b",   25.26

[shnarazk]

cff10ba6

$ mios-lbd 3-SAT/UF100/uf100-024.cnf 
3, 3, 2, 3, 4, 1, 6, 5, 2, 2, 8, 10, 9, 6, 7, 8, 5, 5, 6, 9, 4, 8, 5, 3, 3, 4, 2, 3, 7, 11, 3, 1, 10, 9, 2, 8, 3, 6, 7, 8, 4, 3, 7, 7, 5, 5, 7, 4, 6, 6, 6, 4, 5, 5, 2, 6, *, 7, 7, 3, 6, 6, 6, 8, 8, 6, 7, 5, 3, 3, 2, 4, 6, 2, 5, 5, 6, 6, 5, 5, 5, 5, 7, 7, 7, 1, 6, 5, 5, 7, 6, 5, 4, 6, 5, 5, 5, 7, 6, 5, 4, 6, 5, 6, 8, 7, 2, 7, 3, 5, 3, 6, 5, 4, 5, 5, 7, 2, 9, 2, 6, 5, 5, 2, 6, 1, 6, 4, 5, 4, 5, 5, 2, 5, 3, 5, 4, 4, 7, 7, 9, 5, 2, 7, 2, 7, 2, 5, 5, 1, 7, 3, 4, 6, 3, 5, 4, 2, 6, 5, 5, 6, 6, 5, 4, 5, 5, 5, 5, 3, 4, 5, 4, 4, 1, 8, 5, 1, 3, 5, 5, 8, 6, 9, 8, 7, 6, 3, 5, 4, 4, 5, 2, 4, 5, 4, 5, 4, 4, 4, 4, 4, 4, 3, 7, 6, 6, 6, 2, 5, 5, 6, 6, 6, 4, 5, 5, 6, 7, 8, 7, 10, 9, 6, 7, 5, 4, 6, 5, 4, 5, 2, 4, 6, 6, 5, 5, 2, 5, 4, 5, 2, 6, 6, 5, 6, 5, 4, 6, 6, 5, 5, 3, 3, 4, 5, 6, 6, 6, 5, 4, 6, 5, 6, 5, 4, 5, 4, 3, 5, 2, 4, 4, 3, 2, 5, 3, 4, 4, 3, 3, 3, 5, 4, 3, 5, 4, 3, 2, 2, 3, 2, 3, 2, 3, *, 4, 5, 4, 8, 5, 8, 7, 5, 6, 4, 5, 6, 6, 6, 6, 4, 7, 4, 3, 5, 6, 5, 5, 7, 7, 6, 3, 4, 3, 6, 4, 6, 5, 4, 5, 4, 5, 7, 6, 4, 5, 4, 5, 1, 5, 4, *, 3, 4, 6, 4, 4, 5, 5, 4, 4, 3, 4, 2, 6, 6, 5, 4, *, size = 360
1, 1, *, 1, 1, 1, 1, 1, *, 1, *, *, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, size = 180
[1,2,3,-4,-5,6,-7,8,-9,-10,11,-12,13,14,15,-16,-17,-18,-19,20,-21,22,23,-24,-25,26,-27,28,-29,30,31,32,33,-34,-35,-36,37,38,39,40,41,-42,43,44,45,46,47,48,49,-50,51,-52,-53,-54,55,-56,57,58,-59,60,61,62,-63,64,65,-66,-67,-68,69,-70,-71,72,-73,-74,75,76,77,-78,-79,-80,-81,82,-83,-84,85,-86,-87,-88,-89,-90,91,92,-93,-94,95,-96,-97,-98,-99,100]

[shnarazk]

It seems work well :+1: