Satisfiability solver
by Zhi Han
01 Dec 2008
A satisfiability solver using the classical Davis-Putnam algorithm.
|
Watch this File
|
| File Information |
| Description |
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).
|
| MATLAB release |
MATLAB 7.4 (R2007a)
|
|
Tags for This File
|
| Everyone's Tags |
|
| Tags I've Applied |
|
| Add New Tags |
Please login to tag files.
|
|
Contact us at files@mathworks.com
