Satisfiability solver

A satisfiability solver using the classical Davis-Putnam algorithm.

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