Code covered by the BSD License  

Highlights from
SAT solver by CE & BK algorithms

image thumbnail
from SAT solver by CE & BK algorithms by Sebastien PARIS
Solve SAT problems with 2 stochastic solvers : CE & BK algorithms

readsatA(name)
function A = readsatA(name)

%
% Read a sparse clause matrix A associated with the CNF file 'name'
%
%
% Usage
% -----
% 
% A = readsatA(['name']);
%
% 
% Example
% -------
%
% A = readsat;
% spy(A)
% axis square
%

if(nargin < 1)

    [name, pathname] = uigetfile('*.cnf', 'Select CNF file');

    if (isequal(name , 0) || isequal(pathname , 0))

        disp('Pressed cancel');
        
        A = [];
       
        return

    end
    
end


if(isempty(name))

    A = [];
       
    return

end


fid = fopen(name , 'r');

line = fgetl(fid);

while(line(1) ~= 'p')

    line = fgetl(fid);

end


[T , D] = strtok(strtrim(line));

[T , D] = strtok(D);

data    = str2num(D);

n       = data(1);

m       = data(2);

A       = sparse([] , [] , [] , m , n , 0); 

for i = 1 : m

    line             = fgetl(fid);

    ind              = str2num(line);
    
    ind1             = ind(1:end-1);
    
    A(i , abs(ind1)) = sign(ind1);

end

%%% To be sure that nzmax = nnz, otherwise, sparse transposition in
%%% cost_satA is buggy


[i,j,s] = find(A);

[m,n]   = size(A);

A       = sparse(i,j,s,m,n);

fclose(fid);

Contact us at files@mathworks.com