# Introduction

{% hint style="success" %}
The SAT problem is <mark style="color:blue;">evidently</mark> (rõ ràng) killer app, because it is key to the solution of so many other problems.
{% endhint %}

{% hint style="info" %}
SAT/SMT solvers có thể được coi là bộ giải của các hệ phương trình khổng lồ. Sự khác biệt là các bộ giải SMT lấy các hệ thống ở định dạng tùy ý, trong khi các bộ giải SAT bị giới hạn ở các phương trình Boolean ở dạng CNF.

Rất nhiều bài toán thực tế có thể được biểu diễn dưới dạng bài toán giải hệ phương trình.
{% endhint %}

{% hint style="success" %}
CNF (Conjunctive Normal Form) - là dạng chuẩn hội là một cách tiếp cận để Boolean logic diễn tả công thức như liên từ các điều khoản với and hoặc or.
{% endhint %}

{% hint style="info" %}
SMT (SAT Module Theories) Solver - những công cụ tự động minh chứng sự thảo mãn hay không thỏa mãn (sat/unsat).

* Bài toán SAT là bài toán có độ phức tạp NP và các kỹ thuật SAT solving đã được nghiên cứu và phát triển lâu.
* Satisfiability - thỏa mãn
  {% endhint %}

{% file src="/files/v8wFcdCtxejqlfDMjDx7" %}


---

# 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/introduction.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.