search

shnarazk / mios

A SAT solver written in Haskell.
https://gitlab.com/satisfiability01/mios/
GNU General Public License v3.0
39 stars 3 forks source link

Validate FirstUIP #38

Closed shnarazk closed 7 years ago

shnarazk commented 7 years ago

A dump list @ #37 contains a very strange lines. https://github.com/shnarazk/mios/pull/37#issuecomment-327047758

Why a level is dumped twice?!

It's normal.

shnarazk commented 7 years ago

11d39b6

mios-lbd 3-SAT/UF20/uf20-010.cnf 

!14@4, 18@4, 20@2, !15@3, LBD = 3
!2@4, !3@4, 20@2, LBD = 2
!14@3, 19@3, 20@2, LBD = 2
!19@2, 20@2, 1@1, LBD = 2
!14@2, !19@2, 1@1, LBD = 2
!2@2, 20@2, 1@1, LBD = 2
!3@4, !4@4, 1@1, !7@2, !17@3, 15@3, LBD = 4   -- var 17 is not a decision var!
[-1,-2,3,4,5,6,-7,8,9,-10,-11,12,-13,14,15,16,-17,-18,19,-20]
shnarazk commented 7 years ago

5d1de86

$ mios-lbd 3-SAT/UF20/uf20-010.cnf 
V20: decision var
V18: decision var
V15: required implication var     # by `analyzeRemovable`
!14@4, 18@4, 20@2, !15@3, LBD = 3

analyzeRemovable was transplaned from minisat 2.2 litRedundant