2-sat 中文文档教程
2-sat
2SAT 是布尔可满足性问题的受限版本,其中每个子句的变量数最多为 2。两者都适用在 node.js 和浏览器中使用 browserify。
Example
var twoSat = require("2-sat")
//Solve problem:
//
// (x1 | !x2) & (x3 | x1) & (x3 | x2)
//
console.log(twoSat(3, [[1, -2], [3, 1], [3,2]]))
API
require("2-sat")(numVariables, clauses)
为以合取范式编写的 2SAT 问题找到令人满意的分配。 如果没有赋值是可能的返回 false
。
numVariables
is the number of variablesclauses
is a list of binary clauses. Variables are indexed in clauses starting at1
and negative values indicate negation.
返回 子句变量的赋值向量。 如果问题不可满足,则返回 false
Credits
(c) 2013 Mikola Lysenko。 麻省理工执照
2-sat
2SAT is a restricted version of the boolean satisfiability problem where the number of variables per clause is at most 2. Works both in node.js and in the browser using browserify.
Example
var twoSat = require("2-sat")
//Solve problem:
//
// (x1 | !x2) & (x3 | x1) & (x3 | x2)
//
console.log(twoSat(3, [[1, -2], [3, 1], [3,2]]))
API
require("2-sat")(numVariables, clauses)
Finds a satisfying assignment for a 2SAT problem written in conjunctive normal form. If no assignment is possible returns false
.
numVariables
is the number of variablesclauses
is a list of binary clauses. Variables are indexed in clauses starting at1
and negative values indicate negation.
Returns A vector of assignments to the variables of the clause. If problem is not satisfiable, returns false
Credits
(c) 2013 Mikola Lysenko. MIT License