Satisfiability solver

Version 1.0.0.1 (2.8 KB) by Zhi Han
A satisfiability solver using the classical Davis-Putnam algorithm.
2.4
(5)
1.4K Downloads
Updated 1 Sep 2016

View License

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).

Cite As

Zhi Han (2024). Satisfiability solver (https://www.mathworks.com/matlabcentral/fileexchange/22284-satisfiability-solver), MATLAB Central File Exchange. Retrieved .

MATLAB Release Compatibility
Created with R2007a
Compatible with any release
Platform Compatibility
Windows macOS Linux

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!

Version Published Release Notes
1.0.0.1

Updated license
1.0.0.0