from
Satisfiability solver
by Zhi Han
A satisfiability solver using the classical Davis-Putnam algorithm.
|
| example5.m |
% Example 5 from slides
% A a1 a2 B b G g1 I H
exp=[0 0 0 0 0 0 0 1 0; %I
0 0 0 0 0 0 0 0 1; %H
0 0 0 0 0 0 1 -1 0; %~I||g1
0 0 0 0 0 1 -1 0 0; %~g1||G
0 1 0 0 0 -1 0 0 0; %~G||a1
0 0 0 0 1 -1 0 0 0; %~G||b
1 -1 0 0 0 0 0 0 0; %~a1||A
1 0 -1 0 0 0 0 0 0; %~a2||A
0 -1 -1 0 0 0 0 0 0; %~a1||a2
0 0 1 0 0 0 0 0 -1; %~H||a2
0 0 0 0 1 0 0 0 -1; %~H||a2
0 0 0 1 -1 0 0 0 0];%~b||B
[sat, sol]=sl('SATSolver', exp')
[sat, sol]=satisfy(exp)
|
|
Contact us at files@mathworks.com
