坐着¶

SAGE支持合取范式的解析子句(参见 :wikipedia:`Conjunctive_normal_form` )，即SAT求解，通过受SAT求解中使用的常用DIMACS格式启发的接口 [SG09]. 例如，要表示：：

x1 OR x2 OR (NOT x3)

如果是真的，我们写道：：

(1, 2, -3)

警告

可变指数 must 从一点开始。

解算器¶

默认情况下，Sage将SAT实例作为整数线性规划进行求解(请参见 sage.numerical.mip )，但任何支持DIMACS输入格式的SAT解算器都可以使用 sage.sat.solvers.dimacs.DIMACS 蓝图。Sage附带预写的接口，用于 RSat [RS] 和 Glucose [GL]. 此外，Sage还提供了到 CryptoMiniSat [CMS] SAT求解器，可与基于DIMACS的求解器互换使用。对于最后一个求解器，必须安装可选的CryptoMiniSat程序包，这可以通过在Shell中键入以下命令来完成：

sage -i cryptominisat sagelib

我们现在展示如何解决一个简单的SAT问题。**

(x1 OR x2 OR x3) AND (x1 OR x2 OR (NOT x3))

在Sage的符号中：：

sage: solver = SAT()
sage: solver.add_clause( ( 1,  2,  3) )
sage: solver.add_clause( ( 1,  2, -3) )
sage: solver()       # random
(None, True, True, False)

备注

add_clause() 在必要时创建新变量。当使用CryptoMiniSat时，它创建 all 直到给定索引的变量。因此，添加涉及变量1000的文字将创建多达1000个内部变量。

基于DIMACS的求解器也可用于写入DIMACS文件：：

sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: solver.add_clause( ( 1,  2,  3) )
sage: solver.add_clause( ( 1,  2, -3) )
sage: _ = solver.write()
sage: for line in open(fn).readlines():
....:    print(line)
p cnf 3 2
1 2 3 0
1 2 -3 0

或者，还有 sage.sat.solvers.dimacs.DIMACS.clauses() **

sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS()
sage: solver.add_clause( ( 1,  2,  3) )
sage: solver.add_clause( ( 1,  2, -3) )
sage: solver.clauses(fn)
sage: for line in open(fn).readlines():
....:    print(line)
p cnf 3 2
1 2 3 0
1 2 -3 0

然后可以将这些文件传递给外部SAT解算器。

有关特定求解器的详细信息¶

转换器¶

SAGE支持从布尔多项式(也称为代数范式)到合取范式的转换：：

sage: B.<a,b,c> = BooleanPolynomialRing()
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: e = CNFEncoder(solver, B)
sage: e.clauses_sparse(a*b + a + 1)
sage: _ = solver.write()
sage: print(open(fn).read())
p cnf 3 2
-2 0
1 0
<BLANKLINE>

有关特定转换器的详细信息¶

高级接口¶

SAGE提供了各种高级函数，使得使用布尔多项式变得更容易。我们构建一个非常小规模的AES方程系统，并将其传递给SAT解算器：

sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True)
sage: while True:
....:     try:
....:         F,s = sr.polynomial_system()
....:         break
....:     except ZeroDivisionError:
....:         pass
sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - pycryptosat
sage: s = solve_sat(F)                                            # optional - pycryptosat
sage: F.subs(s[0])                                                # optional - pycryptosat
Polynomial Sequence with 36 Polynomials in 0 Variables