Your program has some mistakes about sat-solver-dpll HOT 7 CLOSED

Could you please share the input for which it fails? Thanks.

from sat-solver-dpll.

I haven't finished reading your code, but I think it has some logic mistakes. That's my test case.
c p cnf 200 320 46 72 115 0 -46 72 130 0 -46 72 -130 0 50 -72 115 0 -50 -72 115 0 92 -95 -115 0 -92 -95 -115 0 95 -115 -171 0 95 133 171 0 -52 -133 171 0 -133 171 175 0 171 -175 176 0 -21 -175 -176 0 21 63 111 0 21 63 -111 0 21 -63 103 0 -63 -94 -103 0 94 -103 -131 0 94 -103 200 0 28 -86 131 0 -28 -86 131 0 -87 131 -200 0 87 -93 131 0 53 87 93 0 -42 -53 93 0 42 -53 184 0 42 90 -184 0 -16 -90 -184 0 16 -90 138 0 -90 -138 187 0 -101 -138 -187 0 7 101 -187 0 -7 -62 101 0 -7 62 152 0 -7 142 -152 0 -49 -142 -152 0 49 -142 -153 0 49 153 -172 0 153 -159 172 0 123 159 172 0 -123 172 -188 0 -123 174 188 0 67 -174 188 0 -67 -89 -174 0 -67 80 89 0 -56 -67 -80 0 56 -80 -116 0 56 116 -186 0 1 116 186 0 -1 -14 186 0 -1 71 113 0 -71 113 186 0 14 -113 -193 0 -113 -160 193 0 100 -113 193 0 66 97 160 0 97 -100 160 0 -92 -97 -100 0 -97 -100 156 0 -40 92 -156 0 40 59 170 0 59 -156 -170 0 15 -59 -156 0 -15 -43 -59 0 43 145 159 0 -15 145 -159 0 43 -145 167 0 -48 -145 -167 0 34 48 -167 0 -34 54 -167 0 -34 -54 -130 0 -34 146 166 0 -54 146 -166 0 118 130 -146 0 -118 -146 165 0 64 -118 -146 0 -27 -64 -165 0 27 36 -64 0 27 -36 -99 0 3 -36 99 0 -3 77 110 0 -36 77 -110 0 -33 -77 107 0 -3 -33 -107 0 33 -77 148 0 -77 -104 -148 0 104 -148 164 0 23 -148 -164 0 -23 38 -164 0 -23 -38 45 0 -26 -38 -45 0 26 -45 -154 0 26 -73 154 0 -55 73 154 0 51 55 180 0 -51 144 180 0 73 -144 180 0 55 57 -180 0 11 -57 -180 0 -11 -57 -71 0 -11 71 81 0 58 -81 195 0 -58 71 195 0 -24 -81 -195 0 -81 179 -195 0 -10 -81 -179 0 10 52 -68 0 -52 -68 -179 0 10 68 -75 0 68 75 163 0 75 -163 -185 0 82 -163 185 0 -82 117 185 0 -82 85 -117 0 -85 -117 -126 0 -85 126 -157 0 -39 -85 126 0 -85 126 -192 0 39 157 173 0 39 -157 173 0 -79 -173 192 0 -5 79 -173 0 5 79 -136 0 5 -61 79 0 61 136 169 0 61 -169 182 0 -162 -169 -182 0 -134 162 -182 0 8 134 -182 0 -8 128 134 0 -8 -128 -178 0 -8 12 -128 0 -8 -12 60 0 -12 -60 132 0 -60 -132 -155 0 -98 -132 155 0 -31 89 155 0 -31 33 98 0 -31 -33 -89 0 22 31 98 0 -22 31 83 0 -22 41 -83 0 -25 -41 -83 0 -41 -83 -144 0 3 -4 25 0 -4 25 -83 0 4 144 196 0 -2 4 -196 0 2 -19 178 0 2 -19 46 0 2 -19 -196 0 19 114 -196 0 -72 -114 -196 0 72 -114 150 0 88 -114 -150 0 56 -150 -151 0 -56 -88 -151 0 -88 151 -199 0 -108 151 199 0 13 151 199 0 -13 -69 136 0 -69 -136 151 0 -13 65 69 0 18 -65 69 0 -18 -65 -197 0 -18 -102 197 0 -18 -32 197 0 32 102 -147 0 32 102 137 0 40 102 -154 0 -40 137 -154 0 32 48 -109 0 -48 -109 -137 0 109 -137 -141 0 -26 109 -141 0 76 109 141 0 76 109 -192 0 -46 -76 141 0 -76 109 -191 0 29 104 191 0 29 -104 191 0 -29 91 191 0 -29 -78 -91 0 78 -91 -194 0 -91 -139 194 0 78 -127 128 0 78 -127 194 0 -107 127 194 0 107 127 161 0 47 127 -161 0 -35 -47 -161 0 -47 96 -161 0 35 -96 -183 0 35 -89 -183 0 17 -96 183 0 -17 84 -96 0 -17 -96 110 0 -17 -84 -121 0 -84 -110 -111 0 -20 -110 121 0 111 -177 200 0 111 -177 -200 0 20 44 177 0 20 -44 -190 0 37 -44 99 0 37 84 190 0 37 -84 -99 0 -37 -140 190 0 108 124 140 0 -37 -108 140 0 -37 -124 125 0 -124 -125 -143 0 106 -125 143 0 -106 143 -170 0 105 -106 170 0 9 -105 170 0 -9 -28 -105 0 -9 -105 -149 0 28 74 149 0 6 11 149 0 6 -74 149 0 -6 -58 -74 0 -6 -74 120 0 -6 -120 129 0 -30 -120 -129 0 66 -120 -129 0 -66 -129 135 0 -66 -70 -135 0 70 -135 189 0 119 -135 -189 0 -119 122 -189 0 -50 -119 -122 0 -119 -122 198 0 50 168 -198 0 -166 -168 -198 0 24 -112 -198 0 -24 -112 -168 0 112 158 166 0 112 -158 -181 0 -51 -158 181 0 50 74 -171 0 45 147 -172 0 38 -93 124 0 13 17 62 0 -19 70 86 0 51 83 114 0 -2 -55 120 0 36 176 -190 0 -40 117 148 0 9 -20 139 0 1 -42 -94 0 -26 -75 93 0 82 -87 -101 0 34 119 140 0 22 125 163 0 -32 121 -178 0 18 50 -73 0 -102 119 -197 0 138 177 -177 0 123 142 183 0 -79 82 -160 0 86 96 157 0 7 16 100 0 -16 44 132 0 54 -62 -134 0 -25 90 122 0 -5 60 -61 0 23 -159 162 0 -33 117 133 0 88 168 179 0 9 -116 -121 0 -94 -149 161 0 53 64 105 0 -185 -194 196 0 38 52 -92 0 12 -98 113 0 41 85 147 0 -147 164 182 0 -131 168 169 0 -49 -143 -191 0 -43 48 -149 0 106 135 158 0 132 175 184 0 -10 -70 152 0 -30 82 118 0 58 130 -153 0 -35 -92 -134 0 6 8 90 0 103 -116 198 0 15 28 -39 0 19 -102 167 0 -33 -35 178 0 -10 -58 -162 0 -49 108 156 0 30 -35 -62 0 -35 -176 189 0 -43 -139 156 0 24 -27 -165 0 -140 -170 181 0 68 110 192 0 22 138 -193 0 -21 -126 150 0 65 91 165 0 -14 30 -155 0 20 81 -181 0 14 103 -197 0 -39 57 174 0 144 -164 -188 0 30 -78 161 0 14 80 -199 0 65 81 178 0 -43 80 133 0 24 103 187 0 -32 -58 0 57 67 139 0 -98 129 139 0 8 52 -170 0 23 -170 176 0 53 184 -186 0 17 -21 47 0

from sat-solver-dpll.

    c
p cnf 200 320
46 72 115 0
-46 72 130 0
-46 72 -130 0
50 -72 115 0
-50 -72 115 0
92 -95 -115 0
-92 -95 -115 0
95 -115 -171 0
95 133 171 0
-52 -133 171 0
-133 171 175 0
171 -175 176 0
-21 -175 -176 0
21 63 111 0
21 63 -111 0
21 -63 103 0
-63 -94 -103 0
94 -103 -131 0
94 -103 200 0
28 -86 131 0
-28 -86 131 0
-87 131 -200 0
87 -93 131 0
53 87 93 0
-42 -53 93 0
42 -53 184 0
42 90 -184 0
-16 -90 -184 0
16 -90 138 0
-90 -138 187 0
-101 -138 -187 0
7 101 -187 0
-7 -62 101 0
-7 62 152 0
-7 142 -152 0
-49 -142 -152 0
49 -142 -153 0
49 153 -172 0
153 -159 172 0
123 159 172 0
-123 172 -188 0
-123 174 188 0
67 -174 188 0
-67 -89 -174 0
-67 80 89 0
-56 -67 -80 0
56 -80 -116 0
56 116 -186 0
1 116 186 0
-1 -14 186 0
-1 71 113 0
-71 113 186 0
14 -113 -193 0
-113 -160 193 0
100 -113 193 0
66 97 160 0
97 -100 160 0
-92 -97 -100 0
-97 -100 156 0
-40 92 -156 0
40 59 170 0
59 -156 -170 0
15 -59 -156 0
-15 -43 -59 0
43 145 159 0
-15 145 -159 0
43 -145 167 0
-48 -145 -167 0
34 48 -167 0
-34 54 -167 0
-34 -54 -130 0
-34 146 166 0
-54 146 -166 0
118 130 -146 0
-118 -146 165 0
64 -118 -146 0
-27 -64 -165 0
27 36 -64 0
27 -36 -99 0
3 -36 99 0
-3 77 110 0
-36 77 -110 0
-33 -77 107 0
-3 -33 -107 0
33 -77 148 0
-77 -104 -148 0
104 -148 164 0
23 -148 -164 0
-23 38 -164 0
-23 -38 45 0
-26 -38 -45 0
26 -45 -154 0
26 -73 154 0
-55 73 154 0
51 55 180 0
-51 144 180 0
73 -144 180 0
55 57 -180 0
11 -57 -180 0
-11 -57 -71 0
-11 71 81 0
58 -81 195 0
-58 71 195 0
-24 -81 -195 0
-81 179 -195 0
-10 -81 -179 0
10 52 -68 0
-52 -68 -179 0
10 68 -75 0
68 75 163 0
75 -163 -185 0
82 -163 185 0
-82 117 185 0
-82 85 -117 0
-85 -117 -126 0
-85 126 -157 0
-39 -85 126 0
-85 126 -192 0
39 157 173 0
39 -157 173 0
-79 -173 192 0
-5 79 -173 0
5 79 -136 0
5 -61 79 0
61 136 169 0
61 -169 182 0
-162 -169 -182 0
-134 162 -182 0
8 134 -182 0
-8 128 134 0
-8 -128 -178 0
-8 12 -128 0
-8 -12 60 0
-12 -60 132 0
-60 -132 -155 0
-98 -132 155 0
-31 89 155 0
-31 33 98 0
-31 -33 -89 0
22 31 98 0
-22 31 83 0
-22 41 -83 0
-25 -41 -83 0
-41 -83 -144 0
3 -4 25 0
-4 25 -83 0
4 144 196 0
-2 4 -196 0
2 -19 178 0
2 -19 46 0
2 -19 -196 0
19 114 -196 0
-72 -114 -196 0
72 -114 150 0
88 -114 -150 0
56 -150 -151 0
-56 -88 -151 0
-88 151 -199 0
-108 151 199 0
13 151 199 0
-13 -69 136 0
-69 -136 151 0
-13 65 69 0
18 -65 69 0
-18 -65 -197 0
-18 -102 197 0
-18 -32 197 0
32 102 -147 0
32 102 137 0
40 102 -154 0
-40 137 -154 0
32 48 -109 0
-48 -109 -137 0
109 -137 -141 0
-26 109 -141 0
76 109 141 0
76 109 -192 0
-46 -76 141 0
-76 109 -191 0
29 104 191 0
29 -104 191 0
-29 91 191 0
-29 -78 -91 0
78 -91 -194 0
-91 -139 194 0
78 -127 128 0
78 -127 194 0
-107 127 194 0
107 127 161 0
47 127 -161 0
-35 -47 -161 0
-47 96 -161 0
35 -96 -183 0
35 -89 -183 0
17 -96 183 0
-17 84 -96 0
-17 -96 110 0
-17 -84 -121 0
-84 -110 -111 0
-20 -110 121 0
111 -177 200 0
111 -177 -200 0
20 44 177 0
20 -44 -190 0
37 -44 99 0
37 84 190 0
37 -84 -99 0
-37 -140 190 0
108 124 140 0
-37 -108 140 0
-37 -124 125 0
-124 -125 -143 0
106 -125 143 0
-106 143 -170 0
105 -106 170 0
9 -105 170 0
-9 -28 -105 0
-9 -105 -149 0
28 74 149 0
6 11 149 0
6 -74 149 0
-6 -58 -74 0
-6 -74 120 0
-6 -120 129 0
-30 -120 -129 0
66 -120 -129 0
-66 -129 135 0
-66 -70 -135 0
70 -135 189 0
119 -135 -189 0
-119 122 -189 0
-50 -119 -122 0
-119 -122 198 0
50 168 -198 0
-166 -168 -198 0
24 -112 -198 0
-24 -112 -168 0
112 158 166 0
112 -158 -181 0
-51 -158 181 0
50 74 -171 0
45 147 -172 0
38 -93 124 0
13 17 62 0
-19 70 86 0
51 83 114 0
-2 -55 120 0
36 176 -190 0
-40 117 148 0
9 -20 139 0
1 -42 -94 0
-26 -75 93 0
82 -87 -101 0
34 119 140 0
22 125 163 0
-32 121 -178 0
18 50 -73 0
-102 119 -197 0
138 177 -177 0
123 142 183 0
-79 82 -160 0
86 96 157 0
7 16 100 0
-16 44 132 0
54 -62 -134 0
-25 90 122 0
-5 60 -61 0
23 -159 162 0
-33 117 133 0
88 168 179 0
9 -116 -121 0
-94 -149 161 0
53 64 105 0
-185 -194 196 0
38 52 -92 0
12 -98 113 0
41 85 147 0
-147 164 182 0
-131 168 169 0
-49 -143 -191 0
-43 48 -149 0
106 135 158 0
132 175 184 0
-10 -70 152 0
-30 82 118 0
58 130 -153 0
-35 -92 -134 0
6 8 90 0
103 -116 198 0
15 28 -39 0
19 -102 167 0
-33 -35 178 0
-10 -58 -162 0
-49 108 156 0
30 -35 -62 0
-35 -176 189 0
-43 -139 156 0
24 -27 -165 0
-140 -170 181 0
68 110 192 0
22 138 -193 0
-21 -126 150 0
65 91 165 0
-14 30 -155 0
20 81 -181 0
14 103 -197 0
-39 57 174 0
144 -164 -188 0
30 -78 161 0
14 80 -199 0
65 81 178 0
-43 80 133 0
24 103 187 0
-32 -58 0
57 67 139 0
-98 129 139 0
8 52 -170 0
23 -170 176 0
53 184 -186 0
17 -21 47 0

from sat-solver-dpll.

But some files can be completed. I don't know if it's a program problem or if the test file I'm using is wrong.

from sat-solver-dpll.

The most likely reason is that the solver takes a very long time to find a solution. The DPLL algorithm is not very efficient in its traversal of the search space (as compared to newer algorithms such as CDCL). Moreover, this is a very simple implementation without any of the common techniques that speedup the search.

You could consider using state-of-the-art SAT solvers, such as from here.

However, in case you find any bug in the code in this repository, please feel free to report it. Thanks.

from sat-solver-dpll.

How can we optimize your code, still using DPLL.

from sat-solver-dpll.

Unfortunately, I am unable to provide any additional support for this right now. For efficiency, it would be best to use state-of-the-art solvers. This code does not focus on that, even in terms of use of efficient data structures and good variable selection heuristics.

from sat-solver-dpll.