現在この提出コンテンツをフォロー中です。
- フォローしているコンテンツ フィードに更新が表示されます。
- コミュニケーション基本設定に応じて電子メールを受け取ることができます
This zip file contains satisfy.m: a very simple implementation of the classical Davis-Putnam algorithm for solving satisfiability (SAT) problems.
Example
[S, a] = satisfy(A)
The input argument A is a (sparse) matrix representation of the conjunctive normal form (CNF) of the boolean formula to solver. Each row of A is a clause and the sign of the entry represents the polarity of the literal. For example, [1 0 -1] represents (x1 or not x3). The return arguments are
- S: whether the formula is satisfiable.
- a: an assignment to satisfy the Boolean formula.
See the examples for more detail.
[sat, sol, X] = sat_cnf(cnf_file)
solves a SAT problem given in the DIMACS CNF file format (.cnf).
引用
Zhi Han (2026). Satisfiability solver (https://jp.mathworks.com/matlabcentral/fileexchange/22284-satisfiability-solver), MATLAB Central File Exchange. に取得済み.
