# 2. Solving XKCD 287

<figure><img src="/files/sZHgFlDzyrhe95SMpdMp" alt=""><figcaption></figcaption></figure>

Mô tả bài toán như sau: 1 người có số tiền 15.05 đô la để gọi món. Hãy giúp cho anh ta chọn số lượng của món này để thanh toán đúng số tiền 15.05 đô la.

Vấn đề này là giải phương trình sau: 2.15a + 2.75b + 3.35c + 3.55d + 4.20e + 5.80f == 15.05, khi a...f là các số nguyên. Vì vậy, đây là một phương trình diophanitine (là phương trình trong đó tổng của 2 hay nhiều hơn đơn thức bằng với một hằng số nào đó, và mỗi đơn thức có bậc một.

Dưới đây là cách giải z3:

{% code overflow="wrap" %}

```python
#!/usr/bin/python3

from z3 import *

a,b,c,d,e,f = Ints('a b c d e f')
s = Solver()
s.add(215*a + 275*b + 335*c + 355*d + 420*e + 580*f == 1505, a>=0, b>=0, c>=0, d>=0, e>=0, f>=0)

results=[]

# enumerate all possible solutions: (liệt kê tất cả các giải pháp có thể)
while True:
    if s.check() == sat:
        m = s.model()
        print (m)
        results.append(m)
        block = []
        for d in m:
            c=d()
            block.append(c != m[d])
        s.add(Or(block))
    else:
        print ("results total=", len(results))
        break
```

{% endcode %}

Và đây là SMT-LIB 2.x format:

```
(set-logic QF-BV)
(set-info :smt-lib-version 2.0)

(declare-fun a () (_ BitVec 16))
(declare-fun b () (_ BitVec 16))
(declare-fun c () (_ BitVec 16))
(declare-fun d () (_ BitVec 16))
(declare-fun e () (_ BitVec 16))
(declare-fun f () (_ BitVec 16))

(assert (bvult a #x0010)) #ult có thể được hiểu until less to 
(assert (bvult b #x0010))
(assert (bvult c #x0010))
(assert (bvult d #x0010))
(assert (bvult e #x0010))
(assert (bvult f #x0010))

(assert
        (=         
                (bvadd 
                        (bvmul (_ bv215 16) a)
                        (bvmul (_ bv275 16) b)
                        (bvmul (_ bv335 16) c)
                        (bvmul (_ bv355 16) d)
                        (bvmul (_ bv420 16) e)
                        (bvmul (_ bv580 16) f)
                 )
                 (_ bv1505 16)
         )
 )
 
;(check-sat)
;(get-model)

(get-all-models)
; correct answer:
;(model
; (define-fun a () (_ BitVec 16) (_ bv7 16)) ; 0x7
; (define-fun b () (_ BitVec 16) (_ bv0 16)) ; 0x0
; (define-fun c () (_ BitVec 16) (_ bv0 16)) ; 0x0
; (define-fun d () (_ BitVec 16) (_ bv0 16)) ; 0x0
; (define-fun e () (_ BitVec 16) (_ bv0 16)) ; 0x0
; (define-fun f () (_ BitVec 16) (_ bv0 16)) ; 0x0
;)
;(model
; (define-fun a () (_ BitVec 16) (_ bv1 16)) ; 0x1
; (define-fun b () (_ BitVec 16) (_ bv0 16)) ; 0x0
; (define-fun c () (_ BitVec 16) (_ bv0 16)) ; 0x0
; (define-fun d () (_ BitVec 16) (_ bv2 16)) ; 0x2
; (define-fun e () (_ BitVec 16) (_ bv0 16)) ; 0x0
; (define-fun f () (_ BitVec 16) (_ bv1 16)) ; 0x1
;)
;Model count: 2
```


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://viettaliii.gitbook.io/home/education/reverse-engineering/symbolic-analysis/sat-smt-by-example/equations/2.-solving-xkcd-287.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.