update

content/posts/2024-4-22.md

@@ -0,0 +1,31 @@
+---
+title: "ArchLinux 使用备忘"
+date: 2024-04-22T17:38:11+08:00
+author: "Shaka"
+slug: 
+---
+
+### 连接无线网络
+
+使用 iwctl 连接
+
+```
+iwctl 
+device list
+station wlan0 scan
+station wlan0 get-networks
+station wlan0 connect wifi-name
+exit
+```
+
+检查内核是否加载无线网卡驱动
+
+```
+lspci -k | grep Network
+```
+
+开启无线网卡开关
+
+```
+rfkill list
+```

content/posts/2024-4-26.md

@@ -0,0 +1,30 @@
+---
+title: "SAT求解教程"
+date: 2024-04-26T10:11:29+08:00
+author: "Shaka"
+slug: 
+draft: true
+---
+
+
+### 1. 计算机求解的两种方法
+
+- 问题可以形式化陈述
+
+用户陈述问题，计算机通过解决数学问题来解决它。典型场景：定理证明。
+
+- 问题无法形式化陈述
+
+用户提供示例，计算机学习如何解决它。典型场景：人脸识别。
+
+### 2. 约束求解
+
+问题 -> 建模 -> 数学子句 Φ -> 求解 -> 结果
+
+- 布尔代数（SAT）
+
+逻辑结构：`𝜑 = (𝑥1 ∨ ¬𝑥2) ∧ (𝑥2 ∨ 𝑥3) ∧ (¬𝑥1 ∨ ¬𝑥3 ∨ 𝑥4)`
+
+- 约束编程（CSP）
+
+各种约束：`𝜓 = 𝐴𝑙𝑙𝐷𝑖𝑓𝑓𝑒𝑟𝑒𝑛𝑡(𝑥𝑖, 𝑥𝑗) ∧ |𝑥𝑖 − 𝑥𝑗| ≠ |𝑖 − 𝑗|`