坐

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] 和 葡萄糖 [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: F,s = sr.polynomial_system()
sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - cryptominisat
sage: s = solve_sat(F)                                            # optional - cryptominisat
sage: F.subs(s[0])                                                # optional - cryptominisat
Polynomial Sequence with 36 Polynomials in 0 Variables