# The SAT Problem

{% hint style="success" %}
SMT2 follows a parenthesized "Prefix Notation", very similar to LISP. This means that the operators are set before the operands, in the format (+ 1 2) instead of (1 + 2), where the parentheses mark the calculation steps. If you are unfamiliar with this notation, please have a quick look at the contents linked here.
{% endhint %}

```armasm
; add eax, ecx
; shl eax, 0xc
; mul ecx
; mov edx, eax
; xor edx, ecx
```

Ta cần tạo các mục theo một khung gồm đầy đủ cá phần như sau: [Link](https://compsys-tools.ens-lyon.fr/z3/index.php)

```
;set the logic type (đây là set kiểu logic muốn sử dụng)
(set-logic QF_BV)
(set-info :smt-lib-version 2.0)

; declare the variables needed
; you are going to need to add some (khai báo định nghĩa các thanh ghi, hằng, hàm)
; on the go
(declare-fun eax_in () (_ BitVec 32))
(declare-fun ecx_in () (_ BitVec 32))

; 1 encode CPU indtructions and machine code (câu lệnh thao tác)

; check for satisfiability (check kiểm tra trạng thái bằng check-sat)

; 02 Retieve a model (nhận kết quả model bằng lệnh get-model)

; 03 constraining the input values (thêm values vào biến bằng push, assert)

; 04 contraining even more
```

Và đây là slove của bài:

```
;set the logic type
(set-logic QF_BV)
(set-info :smt-lib-version 2.0)

; declare the variables needed
; you are going to need to add some
; on the go
(declare-fun eax_in () (_ BitVec 32))
(declare-fun ecx_in () (_ BitVec 32))

(declare-fun eax1 () (_ BitVec 32))
(declare-fun eax2 () (_ BitVec 32))
(declare-fun eax3 () (_ BitVec 32))
(declare-fun edx1 () (_ BitVec 32))
(declare-fun edx2 () (_ BitVec 32))

; 1 encode CPU indtructions and machine code
(assert (and
  (= eax1 (bvadd eax_in ecx_in))
  (= eax2 (bvshl eax1 (_ bv12 32)))
  (= eax3 (bvmul eax2 ecx_in))
  (= edx1 eax3)
  (= edx2 (bvxor edx1 ecx_in))
))

; check for satisfiability
(check-sat)

; 02 Retieve a model
(get-model)

; 03 constraining the input values
(push)
(assert (= eax_in #xffffffff))
(check-sat)
(get-model)

; 04 contraining even more
(push)
(assert (= ecx_in  #xeeeeeee))
(check-sat)
(get-model)
```


---

# 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-and-constraints/the-sat-problem.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.