input을 x, 21BD60을 b로 생각해서 Ax=b를 만들 수 있을 것 같아서, 38*38 A 행렬을 만들어 아래와 같이 z3로 풀었습니다 그런데 model이 없다고 하네요..ㅠㅠ이 방법이 아닌 건가요? 아니면 제가 A를 잘못 구한 건가요? from z3 import * #A 행렬(38 * 38, 직접 구함) value_str = "239 117 113 160 175 170 73 59 28 178 206 64 95 109 249 193 184 0 165 42 223 8 117 205 145 54 75 152 189 73 127 237 200 136 200 150 178 9 \ 97 108 72 187 37 34 232 185 210 217 16 85 155 136 152 241 2 184 92 15 142 51 128 102 225 239 73 70 230 0 229 177 204 37 103 238 88 110 \ 74 80 83 141 35 126 180 99 241 64 127 144 24 122 132 36 107 2 12 176 210 158 34 36 141 82 138 126 197 125 3 201 75 225 186 152 92 106 \ 108 232 209 239 92 138 216 43 51 151 177 89 17 124 233 88 115 107 6 191 224 17 65 77 146 156 61 236 53 36 230 27 145 57 169 144 62 220 \ 214 186 140 232 21 38 103 88 229 86 121 136 236 6 39 27 127 115 217 34 5 62 95 118 90 182 206 246 111 18 37 137 244 152 23 18 179 68 \ 196 150 210 134 147 46 189 60 225 78 72 219 54 97 50 60 246 127 250 46 148 80 249 103 191 157 38 125 104 11 236 94 4 13 19 237 118 232 \ 194 60 201 9 173 106 210 129 6 61 111 92 233 41 65 126 243 246 6 169 100 25 195 15 164 51 102 211 137 17 35 12 31 172 201 160 73 11 \ 101 70 232 158 111 143 226 111 65 137 128 144 90 199 189 90 64 243 84 161 233 10 152 85 78 184 23 149 30 6 157 67 21 7 181 145 40 160 \ 210 184 133 28 29 208 6 19 0 202 163 197 117 133 189 150 6 64 64 43 21 22 93 173 57 97 57 30 90 144 139 87 63 199 3 178 31 85 \ 28 130 214 0 110 123 83 15 2 125 59 160 220 6 188 27 110 6 170 164 60 52 193 103 76 78 168 144 229 216 40 22 109 88 221 145 52 160 \ 196 2 77 39 240 128 51 42 204 74 135 240 111 140 118 173 14 110 53 77 226 114 26 8 15 64 145 190 102 157 132 71 117 23 183 104 217 50 \ 210 81 202 27 0 30 215 111 96 117 41 115 226 124 172 42 241 14 231 134 23 98 250 9 198 155 119 223 178 189 133 105 134 200 86 42 17 73 \ 11 82 129 190 108 50 81 129 134 45 89 237 202 199 212 214 229 241 33 140 111 173 221 15 155 81 118 208 190 229 123 247 90 174 185 12 242 123 \ 155 211 7 85 236 124 237 184 46 198 26 222 54 103 187 115 63 229 227 34 223 159 122 196 132 228 29 26 87 126 238 39 192 153 119 81 76 45 \ 96 106 198 73 16 212 220 208 183 201 101 203 120 77 121 207 216 63 250 100 35 151 110 34 146 148 55 167 82 183 238 113 247 223 110 24 236 246 \ 76 226 120 69 128 177 70 174 16 74 151 200 197 18 19 196 21 216 79 213 41 16 30 31 223 206 64 196 126 191 101 83 140 175 250 193 166 246 \ 234 115 180 6 211 101 34 6 16 159 59 5 148 66 101 167 90 21 20 93 120 211 55 182 163 241 231 31 8 234 66 180 66 18 158 49 85 169 \ 218 205 220 91 42 38 40 191 72 77 35 174 211 136 133 36 27 90 141 119 27 103 182 90 219 111 113 159 100 198 121 33 6 28 95 153 110 160 \ 216 59 45 9 72 210 119 243 198 242 3 51 135 50 10 244 82 27 194 26 112 29 195 45 189 107 67 151 18 181 167 243 83 40 78 7 72 175 \ 184 104 101 160 174 53 35 232 169 122 92 49 33 80 127 235 188 82 75 83 100 55 168 209 110 118 106 239 28 94 186 204 73 118 121 76 182 102 \ 47 55 121 34 173 244 24 15 214 198 133 15 221 196 153 236 45 188 209 48 101 59 177 90 62 147 16 80 243 250 102 195 183 129 97 168 105 230 \ 173 96 68 55 103 197 148 53 16 59 44 207 117 198 178 133 135 45 167 85 47 173 108 14 140 46 69 129 24 147 138 227 238 152 172 192 13 186 \ 186 231 137 246 234 198 68 85 172 145 56 65 46 141 64 57 162 135 56 220 217 81 231 38 191 244 51 213 242 146 122 204 73 63 249 182 70 114 \ 25 219 250 195 231 76 77 149 183 42 113 29 21 51 134 112 199 162 85 203 122 245 114 70 169 129 130 81 247 121 214 73 151 47 10 21 52 227 \ 130 247 73 161 231 58 15 234 215 244 169 228 235 9 118 69 223 199 31 184 137 105 216 149 107 117 1 58 150 186 8 181 150 113 124 5 82 127 \ 237 219 245 199 189 208 150 165 118 123 36 119 193 142 89 179 239 223 125 108 49 68 194 48 122 206 129 196 28 242 126 66 213 232 145 148 164 224 \ 244 202 138 77 78 136 169 201 236 157 233 19 82 66 119 175 36 239 238 106 37 141 33 167 84 241 190 120 236 240 71 216 107 20 22 113 187 142 \ 180 89 166 147 79 166 35 108 121 86 178 86 142 165 0 213 223 36 162 118 186 50 237 21 183 109 206 186 82 135 164 111 39 77 94 203 214 233 \ 216 4 155 24 227 85 142 105 171 145 173 71 237 199 35 246 125 223 219 131 55 204 125 8 159 179 215 46 172 58 107 7 59 94 25 55 227 46 \ 217 229 156 117 155 218 121 37 136 135 140 208 221 26 143 168 127 125 74 140 100 28 217 92 52 165 20 204 67 208 100 217 85 102 172 209 19 228 \ 162 133 135 54 178 78 24 143 107 79 148 49 69 117 21 249 126 127 161 179 70 120 195 102 78 187 227 149 49 124 149 65 215 174 100 45 152 167 \ 149 24 122 75 208 177 82 96 7 103 190 124 233 185 55 231 180 126 222 208 64 67 233 24 79 246 2 170 235 53 45 217 241 164 99 232 41 180 \ 234 46 94 230 99 9 220 103 140 215 104 183 94 225 146 179 54 180 206 37 164 220 215 89 216 128 77 205 216 27 145 23 101 132 48 12 189 91 \ 91 224 238 46 52 48 213 127 195 187 103 135 29 237 75 63 174 54 5 93 196 11 210 28 171 250 231 182 73 169 14 99 214 10 72 3 59 111 \ 137 241 105 205 206 64 0 102 2 243 110 140 186 143 228 65 138 174 169 194 218 232 161 3 53 163 211 162 154 25 113 202 246 73 157 245 51 225 \ 188 105 2 102 37 93 14 104 45 52 236 159 99 242 165 113 49 138 116 209 0 130 200 165 165 212 91 45 91 104 134 16 10 5 132 13 44 203 \ 102 248 208 39 166 92 124 70 54 14 222 50 79 245 138 161 143 49 184 41 8 165 190 67 175 212 96 214 84 122 182 159 125 54 114 151 233 10 \ 1 31 55 68 231 80 185 41 171 212 22 166 61 15 184 126 0 143 187 210 191 1 94 42 97 65 115 214 80 177 105 6 235 6 130 171 58 131".split( " " ) value = list() for i in range(38): value.append(value_str[i].split("\t")) bytes_21BD60 = "141 19 175 235 67 221 136 245 242 163 220 204 13 60 76 235 82 200 153 127 132 244 84 57 77 201 232 24 122 148 224 158 80 162 197 193 170 177".split( " " ) s = Solver() arr = [BitVec("%d" % i, 8) for i in range(38)] for i in range(38): s.add(32 <= arr[i], arr[i] <= 126) for i in range(38): tmp = 0 for j in range(38): tmp += int(valuei) * arr[j] tmp %= 251 s.add(tmp == bytes_21BD60[i]) s.check() print(s.model())