This zip file contains satisfy.m: a very simple implementation of the classical Davis-Putnam algorithm for solving satisfiability (SAT) problems.
[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 (2021). Satisfiability solver (https://www.mathworks.com/matlabcentral/fileexchange/22284-satisfiability-solver), MATLAB Central File Exchange. Retrieved .
Find the treasures in MATLAB Central and discover how the community can help you!Start Hunting!