GPT-Academic Report
SAT解算器练习I
2025年1月6日
SAT解算是一个非常大的话题，一篇文章难以涵盖。以下是一些讨论、程序和链接。
SAT解算器的能力在1990年代经历了爆炸性的性能提升，并且自那以后每年都有相当不错的进步。
下面是一张图表，比较了过去25年的SAT竞赛冠军的表现。提升显著！
可满足性问题从表面上看是一个极其简单的问题。粗略地说，它是在问是否有一个输入可以使电路的输出为真，即反向运行电路。更准确的描述是，它在寻找一个满足的赋值（每个变量为true或false），这是一个由“或”组成的巨大“与”的逻辑范式，称为合取范式。这种范式在某些方面类似于多项式的标准展开形式。这也使它成为处理其他组合问题时的一个很好中间表示形式。
示例的SAT解算器大致分为两种类型：
- 简单的功能编程风格，可能是递归等
- 低级语言实现。你需要显式地管理堆栈，并且可能使用低级语言编写。
我并不反对第一种方法。我写了大量的Python代码。Python的一个好处是你知道无论写什么性能都不会太好。所以你可以写得清晰或有趣。另一方面，Python缺乏了一种来自性能考虑的表达和乐趣。
“LISP程序员知道一切的价值，却不知道任何成本。”——Alan Perlis
无论如何，下文内容并不代表我的建议。有关如何编写SAT解算器，可以参考MiniSAT、Cadical、Kissat以及CrueSAT论文。也许下一篇会提到。
暴力解算器
编写一个暴力解算器总是一个有趣的练习。有时，它甚至有用。如果你的SAT问题变量很少，或者你进入了“终结阶段”，这可能是你能编写的最快的SAT解算器。
一种不错的方法是用整数作为位矢量。然后可以通过递增整数来枚举模型。
一个烦人的设计选择是如何表示你的问题本身。条款列表是一个合理的选择。
# 问题以整数列表的列表表示。
# 外层列表表示隐式的与
# 内层列表（条款）表示隐式的或
# -1表示`¬v1`，1表示`v1`
# 反转变量等同于反转整数，这很巧妙。（会不会太巧妙了？）
CNF = list[list[int]]
def nv(cnf):
"""获取最大变量编号"""
return max((max(map(abs,c),default=0) for c in cnf), default=0)
def bits(i,n):
"""将整数转换成布尔值列表"""
return [bool(i & (1 << j)) for j in range(n)]
def satisfies(model,cnf):
"""赋值的验证。M |= C"""
return all(any(model[abs(l)] if l > 0 else not model[abs(l)] for l in c) for c in cnf)
def brute(cnf):
n = nv(cnf) + 1
for i in range(2**n):
model = bits(i,n)
if satisfies(model, cnf):
yield model
return "unsat"
list(brute([[0],[1,2],[-1,-2]]))
def brute_sat(cnf):
return next(brute(cnf), None) is not None
生成随机的SAT问题可以有一些帮助。但是，随机生成的SAT问题可能不会探索所有感兴趣的现象，因为实际的SAT问题有很多结构。
import random
def rand_cnf():
lits = 9
clauses = 7
return [[random.randint(-lits, lits) for _ in range(random.randint(0,6))] for _ in range(random.randint(0,clauses))]
rand_cnf()
for i in range(10):
print(brute_sat(rand_cnf()))
True
False
False
True
True
True
True
False
True
True
但是这种方法有许多令人不满的地方（哈哈）。它并不容易扩展为更复杂的SAT求解器。此外，使用整数来标识变量意味着你需要在其他地方记录这些整数对应的含义。
Davis Putnam
另一种方法是使用Davis Putnam过程。这基本上是一个消解过程，用来饱和子句集。消解找到两个具有互补文字的子句并将它们合在一起，删除该文字。你可以通过指出无论l还是not l为真，在这两个子句中的其他内容也必须为真来为这种推理增加尊严。通过这种方式，你可以开始从子句中消除变量，类似于通过消除变量解决线性方程组的方法。
以下代码是基于Harrison的代码https://www.cl.cam.ac.uk/~jrh13/atp/OCaml/dp.ml
def resolve_on(p : int, cnf):
"""
通过消解消除文字 p。
"""
assert isinstance(p, int)
pos_p = [c - {p} for c in cnf if p in c]
neg_p = [c - {-p} for c in cnf if -p in c]
no_p = [c for c in cnf if p not in c and -p not in c]
return set(no_p + [c1 | c2 for c1 in pos_p for c2 in neg_p])
def one_literal(cnf):
"""
找到只有一个文字的子句，删除包含它的子句或移除其否定。
"""
p = next((c for c in cnf if len(c) == 1), None)
if p is None:
return None
p, = p
return set([c - {-p} for c in cnf if p not in c])
def affirm_negative(cnf):
lits = set(l for c in cnf for l in c)
pure_lits = [l for l in lits if -l not in lits]
if len(pure_lits) == 0:
return None
return set([c for c in cnf if all(l not in pure_lits for l in c)])
def remove_pos_neg(cnf):
# 删除同时包含 p 和 not p 的所有子句
if any(any(-l in c for l in c) for c in cnf):
return set([c for c in cnf if not any(-l in c for l in c)])
else:
return None
def dp(cnf):
cnf = set([frozenset(c) for c in cnf])
while cnf:
if frozenset() in cnf:
# 不可满足
return False
cnf1 = remove_pos_neg(cnf)
if cnf1 is not None:
cnf = cnf1
continue
cnf1 = one_literal(cnf)
if cnf1 is not None:
cnf = cnf1
continue
cnf2 = affirm_negative(cnf)
if cnf2 is not None:
cnf = cnf2
continue
print(cnf)
p = next(iter(next(iter(cnf))))
cnf = resolve_on(p,cnf)
return True
dp([[0],[1,2],[-1,-2]])
{frozenset({-1, -2}), frozenset({1, 2})}
True
为了验证我们的算法有一定道理，可以将其结果与暴力求解器进行比较。
for i in range(100):
cnf = rand_cnf()
assert brute_sat(cnf) == dp(cnf)
另一种风格的消解求解器使用给定子句循环。给定子句循环是典型的一阶饱和型自动定理证明器的核心部分。这是它的基础版本。这有点像从 datalog 中的半朴素评估，总是在新旧内容之间进行匹配。
def negate_clause(clause : frozenset[int]):
return frozenset([-l for l in clause])
def saturate(cnf):
processed = set()
unprocessed = [frozenset(c) for c in cnf]
while unprocessed:
#print("unprocessed", unprocessed)
given = unprocessed.pop()
if given == frozenset():
return False
if any(-l in given for l in given):
continue
for c2 in processed:
res_lits = given & negate_clause(c2)
#print("given", given, "c2", c2, res_lits)
if len(res_lits) != 0:
res = (given | c2) - res_lits - negate_clause(res_lits)
if res not in processed:
unprocessed.append(res)
processed.add(given)
#print(processed)
return True #processed
#given([[0],[1,2,3],[-1,-2]])
#saturate([[1,2], [2,3], [3,-1], [1]])
#saturate([[6], [-3, 0, 4], [-6, 5, -8, 8, -5]])
#brute_sat([[6], [-3, 0, 4], [-6, 5, -8, 8, -5]])
for i in range(100):
cnf = rand_cnf()
if brute_sat(cnf) != saturate(cnf):
print(cnf)
assert False
# 琐事和点滴
对于给定的子句风格，基于子句长度的 `unprocessed` 队列将为你提供一种单位传播。基于最大文字的未处理队列可能会给你类似递归消除变量的东西。
你可以重新组织（向量化？）给定的子句算法，使其更类似于半朴素Datalog。
以标准形式存储子句或进行子句包含（Subsumption）几乎是为了实现饱和度所必需的。
while len(new) > 0:
d = resolve(new, old)
old = new + old
new = d - old
from z3 import *
使用z3expr作为我的命题
def negate(p : z3.BoolRef):
if z3.is_not(p):
return p.arg(0)
return z3.Not(p)
#bool(BoolVal(True) == BoolVal(True))
x,y = Ints("x y")
x in [y]
x + y in {x, y}
False
### SAT 求解器的部分求值
在深入通用求解器之前考虑具体问题是有启发性的。此外，如果你实际上只需要解决一两个特定的问题，构建通用系统可能是徒劳且昂贵的。你通常可以回顾这些专用求解器作为针对特定问题数据的通用求解器部分求值的实例。我不清楚是否有人真正致力于SAT求解器的部分求值。肯定应该已经被研究过。
import itertools
#list(brute([[0],[1,2],[-1,-2]]))
这些都是 eval_clause(clause, m) 的部分求值：
def clause1(m):
return m[0]
def clause2(m):
return m[1] or m[2]
def clause3(m):
return not m[1] or not m[2]
for m in itertools.product([True,False], repeat=3):
if clause1(m) and clause2(m) and clause3(m): # partial eval of satisfies(cnf, m)
print(m)
(True, True, False)
(True, False, True)
# SAT
sympy.logic.algorithms 中有 dpll1 和 dpll2 [https://github.com/sympy/sympy/blob/master/sympy/logic/algorithms/dpll2.py](https://github.com/sympy/sympy/blob/master/sympy/logic/algorithms/dpll2.py)，还有 LRA，甚至还有与 z3 的接口（！）
cadical 2023 - SBVA 结构化阻塞子句添加 [https://cca.informatik.uni-freiburg.de/papers/BiereFallerFazekasFleuryFroleyksPollitt-SAT-Competition-2024-solvers.pdf](https://cca.informatik.uni-freiburg.de/papers/BiereFallerFazekasFleuryFroleyksPollitt-SAT-Competition-2024-solvers.pdf) kissat
kissat 2024 - 子句一致性闭包 [https://github.com/arminbiere/kissat/blob/master/src/congruence.c](https://github.com/arminbiere/kissat/blob/master/src/congruence.c) [https://cca.informatik.uni-freiburg.de/papers/BiereFazekasFleuryFroleyks-SAT24-preprint.pdf](https://cca.informatik.uni-freiburg.de/papers/BiereFazekasFleuryFroleyks-SAT24-preprint.pdf)
“使用嵌入式SAT求解器Kitten的SAT清理技术” Kitten是kissat内部的一个较小的SAT求解器？
[https://m-fleury.github.io/](https://m-fleury.github.io/)
[https://github.com/IsaFoL/IsaFoL/](https://github.com/IsaFoL/IsaFoL/)
SAT竞赛基准描述
* 替代riscv
* 电路等价性检查
avatar
快速重启可能实现简单。每次冲突后完全重启，不需要清理追踪或模型。
如果我编写了一个SAT求解器，并且使用我的egraph，我可以在SAT竞赛中获得一个迷你奖项吗？
[沉默的SAT革命](https://news.ycombinator.com/item?id=36079115#36081904)
[creusat](https://sarsko.github.io/_pages/SarekSkot%C3%A5m_thesis.pdf) [https://github.com/sarsko/CreuSAT](https://github.com/sarsko/CreuSAT)
[https://fmv.jku.at/fleury/papers/Fleury-thesis.pdf](https://fmv.jku.at/fleury/papers/Fleury-thesis.pdf)
[https://github.com/marijnheule/microsat](https://github.com/marijnheule/microsat)
[https://github.com/msoos/minisat-v1.14](https://github.com/msoos/minisat-v1.14)
[https://x.com/SoosMate/status/1760817528236818456?s=20](https://x.com/SoosMate/status/1760817528236818456?s=20) phind了解SAT求解器 “是的（关于Kitten在Kissat中的角色），但解释仍然有问题。听起来像是一个不明白任何东西的学生试图通过随机讨论这些上下文中的概念来通过考试。我可能会让它勉强通过。”
[https://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html](https://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html) 这个博客很好看
[https://easychair.org/publications/open/b7Cr](https://easychair.org/publications/open/b7Cr) CDCL作为重写系统，
[https://x.com/krismicinski/status/1856341897331003842](https://x.com/krismicinski/status/1856341897331003842) “尝试将我的课堂材料转化为一些关于CDCL的录制讲座。我见过一些关于CDCL历史的好谈话（例如Armin Biere在Simmons研究所的演讲），但我认为还有更多空间可以从尽可能功能化的风格开始讨论。”
两个观察字面值与单纯形表法有关吗？ [https://types.pl/@krismicinski/113470474347084554](https://types.pl/@krismicinski/113470474347084554)
Jules Jacobs - 重构出DPLL并从一开始就将其视为迭代子句学习？
我们可以枚举所有模型。当每个模型失败时，我们可以确定一种回溯跳过而不是仅仅进入下一个模型。或者我们可以进行子句学习。这在我们尝试根据变量顺序获取最小模型时特别有用。
有序解析和CDCL 给定一个解析状态，我们可以开始构建部分模型。字面值排序意味着“Datalog”规则是单元传播，我们在考虑每个规则之前已经分配了所有其他位。轨迹是当前的部分模型。
决策子句与传播子句……
冲突子句应该与之前的子句解决。
CDCL是在有用的字面值排序上做调整。当前的排序*是*轨迹。但是即使我们有最佳的先验排序，它也不会那么好，因为它是
avatar。也许一个智能的avatar循环会更聪明
[https://github.com/NikolajBjorner/ShonanArtOfSAT](https://github.com/NikolajBjorner/ShonanArtOfSAT) 可满足性模重写
[https://www-cs-faculty.stanford.edu/~knuth/programs.html](https://www-cs-faculty.stanford.edu/~knuth/programs.html) Knuth 的 SAT 求解器和其他工具
[https://www.labri.fr/perso/lsimon/research/glucose/](https://www.labri.fr/perso/lsimon/research/glucose/) glucose [https://github.com/audemard/glucose](https://github.com/audemard/glucose) 原来 glucose 是 minisat 的一个分支。我之前不知道这一点
lingeling [https://github.com/arminbiere/lingeling](https://github.com/arminbiere/lingeling)
trail 是当前文字排序。在不同排序之间进行转换。嗯。
## DPLL
[https://en.wikipedia.org/wiki/DPLL_algorithm](https://en.wikipedia.org/wiki/DPLL_algorithm) DP
纯文字消除
* [https://github.com/safwankdb/SAT-Solver-using-DPLL/blob/master/SATSolver.py](https://github.com/safwankdb/SAT-Solver-using-DPLL/blob/master/SATSolver.py)
* [https://github.com/charliermarsh/OCaml-SAT-Solvers/blob/master/dpll.ml](https://github.com/charliermarsh/OCaml-SAT-Solvers/blob/master/dpll.ml)
* [https://github.com/baptiste-fourmont/dpll/blob/main/dpll.ml](https://github.com/baptiste-fourmont/dpll/blob/main/dpll.ml)
* [https://simon.cedeela.fr/sat.html](https://simon.cedeela.fr/sat.html)
* [https://github.com/Gbury/mSAT](https://github.com/Gbury/mSAT)
* [https://github.com/qnighy/ratsat](https://github.com/qnighy/ratsat) 使用 Rust 重新实现的 minisat
* [https://github.com/imandra-ai/minisat-ml](https://github.com/imandra-ai/minisat-ml) [https://github.com/imandra-ai/minisat-ml/blob/master/docs/tech_report.md](https://github.com/imandra-ai/minisat-ml/blob/master/docs/tech_report.md) 技术报告。使用 OCaml 而不是 C++ 的成本对 minisat 的精确复制
Harrison 处理方法 [https://matryoshka-project.github.io/pubs/splitting_paper.pdf](https://matryoshka-project.github.io/pubs/splitting_paper.pdf) 统一划分框架
划分规则。另一种方法是拆分某些子句。嗯。将子句中的析取符号转换为元析取符号。
最简单的方法。使用整数作为模型。遍历它们。我们仍然需要表示子句的能力。我们需要重新评估子句的能力。
使用向量作为模型。
将 trail 与模型分开。它同时承担着两个职责。
单元传播
三值逻辑：真、假、未知。或者重构为真、假，假、真，假、假。真、真表示矛盾。
trues = [] #
falses = []
trues = set()
falses = set()
设计选择：递归、循环、修改、纯 Trail、模型、子句。
简化子句与非子句表示：vecvec，模型表示：vec，在 trail 中隐式表示，集合，其他？文字表示：+- 文字 或 struct bool 文字，整数作为原子。对象作为原子。
学习到的子句和初始子句。
查看这些低级别的最快版本可能不是最启发性的
def simplify(cs):
units 是赋值
units = []
for i in range(4):
units.extend([c[0] for c in cs if len(c) == 1])
cs = [[l for l in c if l not in units] for c in cs if len(c) != 1]
split 应该放在哪里。例如，进入宇宙分支？
def split(c):
return c[0], c[1:]
3-SAT 或 N-SAT 可能通过对 3-SAT 的限制简化甚至提高性能。1-SAT # 模型 2-SAT # 监视列表 3-SAT # 子句
3-SAT 或 N-SAT
## 翻译 private_upload/18682424545/2025-01-08-16-24-42/1.md.part-5.md
# 简化子句和递归简化模型风格
```markdown
def replace(c, n):
if n in c:
return True
else:
return c.remove(-n)
def units(cs):
return {c[0] for c in cs if len(c) == 1}
def search(cs, vs):
# 选择文字 nvar
if any(len(c) == 0 for c in cs): # 空子句无法被满足
return False
v = vs.pop()
for decide in [v, -v]:
todo = {decide}
vs1 = vs.copy()
cs1 = cs.copy()
while todo:
lit = todo.pop()
vs1.remove(abs(lit))
cs1 = [replace(c, lit) for c in cs1] # 简化子句
todo |= units(cs1) # 单元传播
if search(cs1, vs1):
return True
return False
# 替换并简化
# 传播单元
# 递归调用自身 nvar-1
def search_rec(cs):
model = []
def lit_sat(l):
neg = l < 0
v = model.get(abs(l))
if v is None:
return None
return v if not neg else not v
def is_sat():
return all(any(lit_sat(l) for l in c) for c in cs)
def decide():
model.append(True)
"""for l in cs[0]:
if model.get(abs(l)) is None:
model[abs(l)] = l > 0
return True
return False"""
def backtrack():
while model[-1]:
model.pop()
model.append(False)
"""
if model[-1]:
model[-1] = False
else:
model.pop()
backtrack()
"""
def propagate():
pass
model.append(True)
while model:
status = is_sat()
if status is None:
decide()
elif status is False:
backtrack()
elif status is True:
return model
return "unsat"
暴力方法
CNF 应该采取什么形式
---------------------------------------------------------------------------
ModuleNotFoundError Traceback (most recent call last)
Cell In[6], line 2
1 import pysat
----> 2 import pysat.formula
ModuleNotFoundError: No module named 'pysat.formula'
from pysat.formula import CNF
from pysat.solvers import Solver
# 创建一个可满足的 CNF 公式 "(-x1 ∨ x2) ∧ (-x1 ∨ -x2)":
cnf = CNF(from_clauses=[[-1, 2], [-1, -2]])
# 创建这个公式的 SAT 求解器：
with Solver(bootstrap_with=cnf) as solver:
# 1.1 调用求解器处理这个公式：
print('公式是', f'{"可" if solver.solve() else "不可"}满足')
# 1.2 公式是可满足的，因此存在一个模型：
print('并且模型是:', solver.get_model())
# 2.1 使用类似 MiniSat 的假设接口：
print('公式是',
f'{"可" if solver.solve(assumptions=[1, 2]) else "不可"}满足',
'假设 x1 和 x2')
# 2.2 公式是不可满足的，
# 即可以提取一个不可满足的核心：
print('并且不可满足的核心是:', solver.get_core())
公式是可满足
并且模型是: [-1, -2]
公式是在假设 x1 和 x2 下不可满足
并且不可满足的核心是: [1]
cnf = CNF(from_clauses=[[-1, 2], [-1, -2], [14]])
cnf.clauses
cnf.nv
dir(cnf)
['__and__',
'__class__',
'__deepcopy__',
'__delattr__',
'__dict__',
'__dir__',
'__doc__',
'__eq__',
'__format__',
'__ge__',
'__getattribute__',
'__gt__',
'__hash__',
'__iand__',
'__ilshift__',
'__imatmul__',
'__init__',
'__init_subclass__',
'__invert__',
'__ior__',
'__irshift__',
'__iter__',
'__ixor__',
'__le__',
'__lshift__',
'__lt__',
'__matmul__',
'__module__',
'__ne__',
'__new__',
'__or__',
'__reduce__',
'__reduce_ex__',
'__repr__',
'__rshift__',
'__setattr__',
'__sizeof__',
'__str__',
'__subclasshook__',
'__weakref__',
'__xor__',
'_clausify',
'_compute_nv',
'_context',
'_get_key',
'_instances',
'_iter',
'_merge_suboperands',
'_vpool',
'append',
'attach_vpool',
'clauses',
'clausify',
'cleanup',
'comments',
'copy',
'export_vpool',
'extend',
'formulas',
'from_aiger',
'from_clauses',
'from_file',
'from_fp',
'from_string',
'literals',
'name',
'negate',
'nv',
'satisfied',
'set_context',
'simplified',
'to_alien',
'to_dimacs',
'to_file',
'to_fp',
'type',
'weighted']
def nv(cnf):
return max(max(map(abs, c)) for c in cnf)
def bits(i, n):
return [bool(i & (1 << j)) for j in range(n)]
def satisfies(model, cnf):
return all(any(model[abs(l)] if l > 0 else not model[abs(l)] for l in c) for c in cnf)
def brute(cnf):
n = nv(cnf) + 1
for i in range(2**n):
model = bits(i, n)
if satisfies(model, cnf):
yield model
return "unsat"
list(brute([[0], [1, 2], [-1, -2]]))
[[False, True, False], [False, False, True]]
def brute_rec(pmodel, cnf):
n = nv(cnf)
if len(pmodel) == n + 1:
if satisfies(pmodel, cnf):
yield pmodel
else:
yield from brute_rec(pmodel + [False], cnf)
yield from brute_rec(pmodel + [True], cnf)
list(brute_rec([], [[0], [1, 2], [-1, -2]]))
[[False, False, True], [False, True, False]]
def psatisfies(model,cnf):
return all(any(False if len(model) < abs(l) else model[abs(l)] if l > 0 else not model[abs(l)] for l in c) for c in cnf)
def brute_cps(cnf, fail, succ):
pass
def brute_cps(succ, backtracklist):
pass
def decide(model):
model.append(False)
def backtrack(model):
while model[-1]:
model.pop()
model[-1] = True
def brute_loop(cnf): # 暴力循环？
n = nv(cnf) + 1
model = []
while model != [True] * n:
print(model)
if len(model) != n:
decide(model)
else:
if satisfies(model,cnf):
yield model.copy()
backtrack(model)
return "unsat"
list(brute_loop([[0],[1,2],[-1,-2]]))
[]
[False]
[False, False]
[False, False, False]
[False, False, True]
[False, True]
[False, True, False]
[False, True, True]
[True]
[True, False]
[True, False, False]
[True, False, True]
[True, True]
[True, True, False]
[[False, False, True], [False, True, False]]
技术
有界变量消去 - 非常重要的预处理。也许是最重要的？https://fmv.jku.at/papers/EenBiere-SAT05.pdf
阶段保存 - 实现简单，性能提升显著。记录变量的旧值并优先选择？
平均胶水LBD。葡萄糖
“活化”实例化
二元原因跳跃、幸运阶段检测、SLUR前瞻
阻塞子句 https://fmv.jku.at/papers/JarvisaloBiereHeule-TACAS10.pdf
VMTF（Variable Move to Front）变量移动到前面 - 验证的SAT求解器似乎使用这种方式，因为不需要像VSIDS那样使用浮点数。VSIDS。EVSIDS？
Luby重启
- https://www.msoos.org/2023/10/the-inprocessing-api-of-cryptominisat/
- https://fmv.jku.at/biere/talks/Biere-POS14-talk.pdf 三元解析
- 主干简化 https://wenxiwang.github.io/papers/cadiback.pdf
- 蒸馏 https://dl.acm.org/doi/10.1145/1278480.1278628
- 使用Korhonen和Jarvisalo的Oracle工具对从句进行活化 https://arxiv.org/pdf/2308.15819.pdf
%%file /tmp/sat.c
#define VAR(n) ((1 << n) & model)
//bool var(int model, int i){
//
//}
bool clause1(int model){
return VAR(3) | VAR(4) | VAR(5);
}
#define VNUM 4
int main(){
for(int model = 0; model < 2**VNUM; model++){
if(clause1(model) && clause2(model) && clause3(model)){
printf("%d\n", model);
return 0;
}
}
printf("unsat");
return 1;
}
子句学习
https://en.wikipedia.org/wiki/Conflict-driven_clause_learning
如何实际执行它？蕴含图（不好的视角？）
遍历追踪。
单冲突子句或多个？我们在单位传播队列中可能会有多个“原因”。类似于生成证明的一致性闭包？每个单位传播可以标记为原因子句或决定。
https://sarsko.github.io/_pages/SarekSkot%C3%A5m_thesis.pdf 第5节
子句学习和解析。
双观测文字
翻译 private_upload/18682424545/2025-01-08-16-24-42/1.md.part-8.md
将 2-SAT 与 2-sat ~ 同余闭包进行比较。
tw 观察到的自由变量 ~ 并查集自由
b | a b = ite(a, b, true) a = ite(b, a, true) ite(false,b,true) = true iter(false,b,true) = true
实际上不需要 ite……但是，如果两个东西在 a 上被冻结呢？好吧，也许我们需要它
b = freeze(clause7, a, true) freeze(clause7,false)
# 两个观察到的自由变量
Lit = int
clauses = []
from collections import defaultdict
vmap = defaultdict(list)
def unit(cnum):
for lit in clauses[cnum]:
v = model[lit]
if v is None:
def propagate(lit):
queue = [lit]
while queue:
lit = queue.pop()
for cid in vmap[lit]:
#cls = clauses[cid]
for l2 in cid:
v2 = model[l2]
if v2 is True:
break # 子句为真
elif v2 is None:
if cid in vmap[l2]: # 其他观察到的自由变量
continue
else:
vmap[l2].append(cid)
break
l2 = unit(cid)
if l2 is not None:
queue.append(l2)
def solve():
trail = []
clauses = []
def clause(n):
c = clauses[n]
for lit in c:
while True:
# 传播
# 决策
# 回跳
# 学习
# 忘记
class Solver():
model : dict[int, bool]
trail : list[tuple[bool, int, int]]
twl : dict[int, list[int]]
def eval_clause(self, nc):
c = self.clauses[c]
done = True
for l in c:
v = self.model.get(l)
if v is True:
return True
if v is None:
done = False
continue
if done:
return False # 冲突
else:
return None # 未决定
def decide(self, l):
self.trail.append((True, l))
self.model[l] = True
def backjump(self, n):
for i in range(n):
l = self.trail.pop()
del self.model[l]
求解器
Cadical
- Chu、Harwood 和 Stuckey 在 2008 年 JSAT 论文中的阻塞文字
- 最后，在长子句中，我们将最后一个观察替换的位置保存在 'pos' 中，从而减少了某些二次累积传播成本（Ian Gent 的 2013 年 JAIR 文章）
https://cca.informatik.uni-freiburg.de/papers/BiereFallerFazekasFleuryFroleyksPollitt-CAV24.pdf cadical 2
cdcl_loop_with_inrpcoessing是内部的核心 https://github.com/arminbiere/cadical/blob/31f9aae44947c673dc6190c9beb399acb9ffec6a/src/internal.cpp#L246
mode = PROPAGATE
def analyze():
def propagate():
def decide():
while True:
match mode:
case PROPAGATE:
case DECIDE:
