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

comparison of clause layouts #80

Closed shnarazk closed 6 years ago

shnarazk commented 6 years ago

Ditching Float fields from Clause.

stack install --profile

comparison base : mios-76 (WIP-for-1.6.1)

$ sat-benchmark -3 250 -s mios-76 mios-80.1                                                         
solver, num, target, time                                                                           
# sat-benchmark 0.14.1, j=1, t=510, p='' on xingu @ 2018-04-02T17:18:18+09:00                       
# 2018-04-02T17:12 mios-76; # mios-1.6.1WIP#72#73#74#77#78 -- https://github.com/shnarazk/mios/commit/cb5e772087f573655ed1ab1560695b1cea8144e1
"mios-76", 1, 250,       167.50                                                                     
"mios-76", 2, "itox",    14.97                                                                      
"mios-76", 3, "m283",    70.00                                                                      
"mios-76", 4, "38b",     23.61                                                                      
"mios-76", 5, "44b",     120.82
shnarazk commented 6 years ago 
        Sun Apr  1 16:58 2018 Time and Allocation Profiling Report  (Final)

           mios-80.0 +RTS -p -RTS /home/narazaki/Documents/SAT-RACE/SC17main/g2-T75.2.0.cnf

        total time  =       35.48 secs   (35476 ticks @ 1000 us, 1 processor)
        total alloc = 21,107,812,848 bytes  (excludes profiling overheads)

COST CENTRE               MODULE                        SRC                                               %time %alloc

primitive                 Control.Monad.Primitive       Control/Monad/Primitive.hs:94:3-16                 36.4   12.2
injectClausesFromCNF.loop SAT.Mios                      src/SAT/Mios.hs:(280,7)-(281,57)                    7.9    5.4
clauseNew                 SAT.Mios.Criteria             src/SAT/Mios/Criteria.hs:(141,1)-(163,27)           6.0    2.8
pushClauseWithKey         SAT.Mios.ClauseManager        src/SAT/Mios/ClauseManager.hs:(237,1)-(252,25)      5.5    2.6
modify'                   SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:260:3-81                        3.5    9.0
clauseNew.loop            SAT.Mios.Criteria             src/SAT/Mios/Criteria.hs:(145,7)-(150,61)           3.2    0.4
getNth                    SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:174:3-50                        3.1    8.3
setNth                    SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:176:3-55                        3.0   11.1
basicUnsafeIndexM         Data.Vector                   Data/Vector.hs:277:3-62                             2.4    0.0
newClauseFromStack.loop   SAT.Mios.Clause               src/SAT/Mios/Clause.hs:(99,5)-(100,58)              2.4    0.0
readByteArray#            Data.Primitive.Types          Data/Primitive/Types.hs:175:297-428                 2.3   10.7
newVec                    SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:(186,3)-(189,41)                2.2    6.0
swapBetween               SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:(180,3)-(183,72)                1.9    5.9
sortStack.sortOnRange     SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:(337,7)-(363,37)                1.8    2.2
pushTo                    SAT.Mios.ClauseManager        src/SAT/Mios/ClauseManager.hs:(116,3)-(131,27)      1.8    1.0
newClauseFromStack        SAT.Mios.Clause               src/SAT/Mios/Clause.hs:(95,1)-(102,55)              1.7    2.4
newManager                SAT.Mios.ClauseManager        src/SAT/Mios/ClauseManager.hs:(142,3)-(146,79)      1.6    2.4
get'                      SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:256:3-46                        1.4    2.8
new'                      SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:(267,3)-(269,40)                0.9    1.4
basicUnsafeWrite          Data.Vector.Mutable           Data/Vector/Mutable.hs:118:3-65                     0.8    3.9
basicUnsafeNew            Data.Vector.Primitive.Mutable Data/Vector/Primitive/Mutable.hs:(96,3)-(102,37)    0.5    1.4
shnarazk commented 6 years ago 
        Sun Apr  1 18:06 2018 Time and Allocation Profiling Report  (Final)

           mios-80.1 +RTS -p -RTS /home/narazaki/Documents/SAT-RACE/SC17main/g2-T75.2.0.cnf

        total time  =       34.20 secs   (34198 ticks @ 1000 us, 1 processor)
        total alloc = 21,317,890,528 bytes  (excludes profiling overheads)

COST CENTRE               MODULE                        SRC                                               %time %alloc

primitive                 Control.Monad.Primitive       Control/Monad/Primitive.hs:94:3-16                 35.9   11.5
injectClausesFromCNF.loop SAT.Mios                      src/SAT/Mios.hs:(280,7)-(281,57)                    7.5    5.3
clauseNew                 SAT.Mios.Criteria             src/SAT/Mios/Criteria.hs:(146,1)-(168,27)           6.0    2.8
pushClauseWithKey         SAT.Mios.ClauseManager        src/SAT/Mios/ClauseManager.hs:(237,1)-(252,25)      5.7    2.6
setNth                    SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:176:3-55                        3.5   11.6
modify'                   SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:260:3-81                        3.2    8.9
clauseNew.loop            SAT.Mios.Criteria             src/SAT/Mios/Criteria.hs:(150,7)-(155,61)           3.2    0.4
getNth                    SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:174:3-50                        3.1    8.2
newClauseFromStack.loop   SAT.Mios.Clause               src/SAT/Mios/Clause.hs:(98,7)-(99,60)               2.8    0.0
basicUnsafeIndexM         Data.Vector                   Data/Vector.hs:277:3-62                             2.5    0.0
readByteArray#            Data.Primitive.Types          Data/Primitive/Types.hs:175:297-428                 2.4   10.6
newVec                    SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:(186,3)-(189,41)                2.3    5.9
sortStack.sortOnRange     SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:(337,7)-(363,37)                2.1    2.1
swapBetween               SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:(180,3)-(183,72)                2.0    5.9
pushTo                    SAT.Mios.ClauseManager        src/SAT/Mios/ClauseManager.hs:(116,3)-(131,27)      2.0    1.0
newClauseFromStack        SAT.Mios.Clause               src/SAT/Mios/Clause.hs:(95,1)-(101,19)              1.9    4.7
newManager                SAT.Mios.ClauseManager        src/SAT/Mios/ClauseManager.hs:(142,3)-(146,79)      1.6    2.4
get'                      SAT.Mios.Vec                  src/SAT/Mios/Vec.hs:256:3-46                        1.5    2.8
basicUnsafeWrite          Data.Vector.Mutable           Data/Vector/Mutable.hs:118:3-65                     0.9    3.9
basicUnsafeNew            Data.Vector.Primitive.Mutable Data/Vector/Primitive/Mutable.hs:(96,3)-(102,37)    0.6    1.4
shnarazk commented 6 years ago 
        Sun Apr  1 20:33 2018 Time and Allocation Profiling Report  (Final)

           mios-80.1 +RTS -p -RTS /home/narazaki/Documents/SAT-RACE/SC17main/g2-T75.2.0.cnf

        total time  =       34.81 secs   (34806 ticks @ 1000 us, 1 processor)
        total alloc = 21,606,812,280 bytes  (excludes profiling overheads)

COST CENTRE               MODULE                           SRC                                                   %time %alloc

primitive                 Control.Monad.Primitive          Control/Monad/Primitive.hs:94:3-16                     36.0   11.4
injectClausesFromCNF.loop SAT.Mios                         src/SAT/Mios.hs:(280,7)-(281,57)                        7.9    5.3
clauseNew                 SAT.Mios.Criteria                src/SAT/Mios/Criteria.hs:(146,1)-(168,27)               6.7    5.8
pushClauseWithKey         SAT.Mios.ClauseManager           src/SAT/Mios/ClauseManager.hs:(237,1)-(252,25)          4.6    0.2
setNth                    SAT.Mios.Vec                     src/SAT/Mios/Vec.hs:176:3-55                            3.3   11.4
clauseNew.loop            SAT.Mios.Criteria                src/SAT/Mios/Criteria.hs:(150,7)-(155,61)               3.3    0.4
modify'                   SAT.Mios.Vec                     src/SAT/Mios/Vec.hs:260:3-81                            3.2    8.8
getNth                    SAT.Mios.Vec                     src/SAT/Mios/Vec.hs:174:3-50                            3.0    8.1
basicUnsafeIndexM         Data.Vector                      Data/Vector.hs:277:3-62                                 2.7    0.0
readByteArray#            Data.Primitive.Types             Data/Primitive/Types.hs:175:297-428                     2.7   10.4
newClauseFromStack.loop   SAT.Mios.Clause                  src/SAT/Mios/Clause.hs:(95,7)-(96,60)                   2.7    0.0
newVec                    SAT.Mios.Vec                     src/SAT/Mios/Vec.hs:(186,3)-(189,41)                    2.4    5.8
swapBetween               SAT.Mios.Vec                     src/SAT/Mios/Vec.hs:(180,3)-(183,72)                    2.0    5.8
sortStack.sortOnRange     SAT.Mios.Vec                     src/SAT/Mios/Vec.hs:(337,7)-(363,37)                    1.9    2.1
pushTo                    SAT.Mios.ClauseManager           src/SAT/Mios/ClauseManager.hs:(116,3)-(131,27)          1.8    0.0
newClauseFromStack        SAT.Mios.Clause                  src/SAT/Mios/Clause.hs:(92,1)-(98,19)                   1.8    4.3
newManager                SAT.Mios.ClauseManager           src/SAT/Mios/ClauseManager.hs:(142,3)-(146,79)          1.7    2.7
get'                      SAT.Mios.Vec                     src/SAT/Mios/Vec.hs:256:3-46                            1.3    2.7
addClause                 SAT.Mios.Criteria                src/SAT/Mios/Criteria.hs:(174,1)-(178,45)               0.9    1.4
basicUnsafeWrite          Data.Vector.Mutable              Data/Vector/Mutable.hs:118:3-65                         0.8    3.9
basicUnsafeNew            Data.Vector.Primitive.Mutable    Data/Vector/Primitive/Mutable.hs:(96,3)-(102,37)        0.6    1.3
basicSet                  Data.Vector.Generic.Mutable.Base Data/Vector/Generic/Mutable/Base.hs:(104,3)-(116,73)    0.4    1.0
shnarazk commented 6 years ago

no injection version

    Mon Apr  2 10:43 2018 Time and Allocation Profiling Report  (Final)

       mios-80.1 +RTS -p -RTS /home/narazaki/Documents/SAT-RACE/SC17main/g2-T75.2.0.cnf

    total time  =        7.10 secs   (7103 ticks @ 1000 us, 1 processor)
    total alloc = 5,342,896,568 bytes  (excludes profiling overheads)

COST CENTRE               MODULE                           SRC                                                   %time %alloc

injectClausesFromCNF.loop SAT.Mios                         src/SAT/Mios.hs:(280,7)-(281,57)                       30.1   21.3
primitive                 Control.Monad.Primitive          Control/Monad/Primitive.hs:94:3-16                     28.6   21.3
newManager                SAT.Mios.ClauseManager           src/SAT/Mios/ClauseManager.hs:(142,3)-(146,79)          6.3    6.8
newVec                    SAT.Mios.Vec                     src/SAT/Mios/Vec.hs:(186,3)-(189,41)                    4.1    8.6
setNth                    SAT.Mios.Vec                     src/SAT/Mios/Vec.hs:176:3-55                            3.4   11.9
basicUnsafeNew            Data.Vector.Primitive.Mutable    Data/Vector/Primitive/Mutable.hs:(96,3)-(102,37)        3.2    5.4
new'                      SAT.Mios.Vec                     src/SAT/Mios/Vec.hs:(236,3)-(238,22)                    2.9    0.9
basicSet.do_set           Data.Vector.Generic.Mutable.Base Data/Vector/Generic/Mutable/Base.hs:(112,7)-(116,73)    2.6    0.0
new'                      SAT.Mios.Vec                     src/SAT/Mios/Vec.hs:(252,3)-(254,37)                    2.3    3.2
basicSet                  Data.Vector.Generic.Mutable.Base Data/Vector/Generic/Mutable/Base.hs:(104,3)-(116,73)    2.2    3.6
newClauseVector           SAT.Mios.Clause                  src/SAT/Mios/Clause.hs:(142,1)-(145,10)                 2.0    1.8
setByteArray#             Data.Primitive.Types             Data/Primitive/Types.hs:175:506-860                     1.6    0.0
basicInitialize           Data.Vector.Primitive.Mutable    Data/Vector/Primitive/Mutable.hs:(105,3)-(108,36)       1.2    2.3
basicUnsafeNew            Data.Vector.Mutable              Data/Vector/Mutable.hs:(99,3)-(102,32)                  1.1    2.3
basicUnsafeWrite          Data.Vector.Mutable              Data/Vector/Mutable.hs:118:3-65                         1.0    3.6
basicUnsafeCopy           Data.Vector.Mutable              Data/Vector/Mutable.hs:(121,3)-(122,36)                 0.9    2.3
basicUnsafeWrite          Data.Vector.Primitive.Mutable    Data/Vector/Primitive/Mutable.hs:115:3-69               0.4    1.8
parseCNF                  SAT.Mios                         src/SAT/Mios.hs:(261,1)-(271,29)                        0.0    2.1
shnarazk commented 6 years ago 

$ sat-benchmark -3 250 -s mios-76 mios-80.1                                                         
solver, num, target, time                                                                           
# sat-benchmark 0.14.1, j=1, t=510, p='' on xingu @ 2018-04-02T17:18:18+09:00                       
# 2018-04-02T17:12 mios-76; # mios-1.6.1WIP#72#73#74#77#78 -- https://github.com/shnarazk/mios/commit/cb5e772087f573655ed1ab1560695b1cea8144e1
"mios-76", 1, 250,       167.50                                                                     
"mios-76", 2, "itox",    14.97                                                                      
"mios-76", 3, "m283",    70.00                                                                      
"mios-76", 4, "38b",     23.61                                                                      
"mios-76", 5, "44b",     120.82                                                                     
# 2018-04-02T16:53 mios-80.1; # mios-#80 -- https://github.com/shnarazk/mios/commit/9b25b16e15e848bd4dafc3a480de706028c3f23b
"mios-80.1", 1, 250,     186.84                                                                     
"mios-80.1", 2, "itox",  15.01                                                                      
"mios-80.1", 3, "m283",  88.00                                                                      
"mios-80.1", 4, "38b",   16.37                                                                      
"mios-80.1", 5, "44b",   505.79   ```
shnarazk commented 6 years ago

cherry picked -- clause parser -- tiny changes on 'Clause' layout -- comments -- internals of sort functions