跳转至主要内容
回到顶部
Ctrl
+
K
思考的代码 ― 约束与优化的冒险
搜索
Ctrl
+
K
Z3
约束满足问题(CSP)：给每个变量定一个值，让全部条件都满足
Z3的用法：用五个步骤解约束，从建立变量到取出全部解
用尽量少的硬币付款：借助 Optimize 直接求出最优解
扫雷：根据已翻开格中的数字推断出哪些格是安全的
运动会得分谜题：竞赛数目未知时如何求解
10 个问题的谜题：用 Implies 解自指的选择题
24 点：寻找四个数与三个运算符的组合
插入运算符凑出 99：让 Z3 决定括号的位置
骑士巡游：找出把每一格都访问一次的路线
数回：用线把相同的数字连起来
预测伪随机数：用 Z3 反算
rand()
的种子
格雷码：构造每步只变一位的数列
攻破 CRC32：从哈希值造出原始数据
Z3 的数据类型：式、类型与函数声明的关系
Fixedpoint：用递归的规则推导可达性
PySat
用 SAT 解数独：把恰好一个写成 CNF
解数织：用位置变量把 CNF 变小
解四角分割：用布尔变量把格与数字连起来
OrTools
CP-SAT 简介：用 SAT 的技术做约束编程
CP-SAT 的基本 API：构造约束所用的函数与写法
解数织：把每个数字的起始位置设为整数变量
装箱谜题：把 12 种五格骨牌装进箱子
巡回路约束：用一条闭合回路来决定访问顺序
数墙：把谜题当作格点上的回路来解
珍珠 Masyu：用边写出圆圈的约束
阴阳谜题：用整数编号来表达同色格的连通性
数回：用回路把数字的对连起来
旅行商问题：寻找一条总距离最短的巡回路线
Repository
Open issue
索引