BCP的基本实现演示

$ ./MapleLCMDistChronoBT-DL-v2_scavel.exe 10.48.640112774.cnf outu1.out
0
c This is MapleLCMDistChronoBT.
c ============================[ Problem Statistics ]=============================
c |                                                                             |
c |  Number of variables:  {          10}                                       |
c |  Number of clauses:    {          48}                                       |
c |  Parse time:                   0.00 s                                       |
c Reduced to 10 vars, 43 cls (grow=0)
c No iterative elimination performed. (vars=10, c/v ratio=4.3)
c |  Simplification time:          0.00 s                                       |
c |                                                                             |
c ============================[ Search Statistics ]==============================
c | Conflicts |          ORIGINAL         |          LEARNT          | Progress |
c |           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
c ===============================================================================
decisions: 1;  decision var: -1
the size of trail is 3. : -1 -7 3
the size of trail_lim is 1 : 0
the implied lit is : -7
the implied clause is: [-7 1 ]
the implied lit is : 3
the implied clause is: [3 7 ]

decisions: 2;  decision var: -10
the size of trail is 10. : -1 -7 3 -10 -6 -4 9 -2 8 5
the size of trail_lim is 2 : 0 3
the implied lit is : -6
the implied clause is: [-6 10 -3 ]
the implied lit is : -4
the implied clause is: [-4 6 1 ]
the implied lit is : 9
the implied clause is: [9 6 -3 ]
the implied lit is : -2
the implied clause is: [-2 4 6 ]
the implied lit is : 8
the implied clause is: [8 -9 1 ]
the implied lit is : 5
the implied clause is: [5 -8 6 ]

the conflict index of trail is : 8
the conflict liter is : 8
the tow clauses get confliction each other-----
the conflict reason clause is: [8 -9 1 ]
the confl clause is: [-5 -8 2 ]

the learnt clause is : [ 6  1 ]

backtrack_level:1

decisions: 3;  decision var: -1
the size of trail is 7. : -1 -7 3 6 2 10 4
the size of trail_lim is 1 : 0
the implied lit is : -7
the implied clause is: [-7 1 ]
the implied lit is : 3
the implied clause is: [3 7 ]
the implied lit is : 6
the implied clause is: [6 1 ]
the implied lit is : 2
the implied clause is: [2 -6 -3 ]
the implied lit is : 10
the implied clause is: [10 -6 -3 ]
the implied lit is : 4
the implied clause is: [4 -6 -3 ]

the conflict index of trail is : 3
the conflict liter is : 6
the tow clauses get confliction each other-----
the conflict reason clause is: [6 1 ]
the confl clause is: [-4 -6 -2 ]

the learnt clause is : [ 1 ]

backtrack_level:0

decisions: 3;  decision var: 1
the size of trail is 1. : 1
the size of trail_lim is 0 :

decisions: 4;  decision var: -7
the size of trail is 9. : 1 -7 3 9 -4 8 -6 5 -2
the size of trail_lim is 1 : 1
the implied lit is : 3
the implied clause is: [3 7 ]
the implied lit is : 9
the implied clause is: [9 -3 -1 ]
the implied lit is : -4
the implied clause is: [-4 -9 -3 ]
the implied lit is : 8
the implied clause is: [8 4 -1 ]
the implied lit is : -6
the implied clause is: [-6 4 -3 ]
the implied lit is : 5
the implied clause is: [5 -8 6 ]
the implied lit is : -2
the implied clause is: [-2 6 4 ]

the conflict index of trail is : 7
the conflict liter is : 5
the tow clauses get confliction each other-----
the conflict reason clause is: [5 -8 6 ]
the confl clause is: [2 -5 -8 ]

the learnt clause is : [ -3 ]

backtrack_level:0

decisions: 4;  decision var: 1
the size of trail is 4. : 1 -3 7 -10
the size of trail_lim is 0 :
the implied lit is : 7
the implied clause is: [3 7 ]
the implied lit is : -10
the implied clause is: [-10 3 -1 ]

decisions: 5;  decision var: 9
the size of trail is 9. : 1 -3 7 -10 9 -2 5 8 -6
the size of trail_lim is 1 : 4
the implied lit is : -2
the implied clause is: [-2 -9 -7 ]
the implied lit is : 5
the implied clause is: [5 -9 -7 ]
the implied lit is : 8
the implied clause is: [8 2 3 ]
the implied lit is : -6
the implied clause is: [-6 -5 2 ]

the conflict index of trail is : 6
the conflict liter is : 5
the tow clauses get confliction each other-----
the conflict reason clause is: [5 -9 -7 ]
the confl clause is: [-8 -5 2 ]

the learnt clause is : [ -9 ]

backtrack_level:0

decisions: 5;  decision var: 1
the size of trail is 9. : 1 -3 7 -10 -9 2 5 8 6
the size of trail_lim is 0 :
the implied lit is : 7
the implied clause is: [3 7 ]
the implied lit is : -10
the implied clause is: [-10 3 -1 ]
the implied lit is : 2
the implied clause is: [2 9 -7 ]
the implied lit is : 5
the implied clause is: [5 9 -6 ]
the implied lit is : 8
the implied clause is: [8 9 3 ]
the implied lit is : 6
the implied clause is: [6 9 -1 ]

the conflict index of trail is : 4
the conflict liter is : -9
the tow clauses get confliction each other-----
the pre conflict clause in level 0! not put out!]
the confl clause is: [-6 9 3 ]

the conflict index of trail is : 4
the conflict liter is : -9
the tow clauses get confliction each other-----
the pre conflict clause in level 0! not put out!]
the confl clause is: [-6 9 3 ]

c ===============================================================================
c restarts              : {1}
c conflicts             : {5           }   (inf /sec)
c decisions             : {5           }   (0.00 % random) (inf /sec)
c propagations          : {25          }   (inf /sec)
c conflict literals     : {5           }   (16.67 % deleted)
c backtracks            : {4           }   (NCB 100% , CB 0%)
c Memory used           : 1.00 MB
c CPU time              : {0} s

s {UNSATISFIABLE}