Be the first to rate this file! 11 downloads (last 30 days) File Size: 3.92 KB File ID: #22284

Satisfiability solver

01 Dec 2008

A satisfiability solver using the classical Davis-Putnam algorithm.

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)
Zip File Content
Other Files	example1.m, example2.m, example3.m, example4.m, example5.m, sat_cnf.m, satisfy.m

Tags for This File
Everyone's Tags	algorithm, discrete, logic, satisfiability
Tags I've Applied
Add New Tags	Please login to tag files.

Please login to add a comment or rating.

Tag Activity for this File
Tag	Applied By	Date/Time
satisfiability	Zhi Han	01 Dec 2008 15:51:18
algorithm	Zhi Han	01 Dec 2008 15:51:18
discrete	Zhi Han	18 Dec 2008 09:44:22
logic	Zhi Han	18 Dec 2008 09:44:27

MATLAB Central Terms of Use

NOTICE: Any content you submit to MATLAB Central, including personal information, is not subject to the protections which may be afforded information collected under other sections of The MathWorks, Inc. Web site. You are entirely responsible for all content that you upload, post, e-mail, transmit or otherwise make available via MATLAB Central. The MathWorks does not control the content posted by visitors to MATLAB Central and, does not guarantee the accuracy, integrity, or quality of such content. Under no circumstances will The MathWorks be liable in any way for any content not authored by The MathWorks, or any loss or damage of any kind incurred as a result of the use of any content posted, e-mailed, transmitted or otherwise made available via MATLAB Central. Read the complete Terms prior to use.