[Formulas] = loadSAT(n, mum_i) loadMaxSAT: This function loads SAT instances from the SATLIB- benchmark problems site (http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html). It is only valid for the set of instances called Uniform Random-3-SAT. In 'functions/sat/sat_instances' there are some examples. INPUT n: number of variables num_i: instance identifier Formula{i,j}: Global variable that contains j clauses for the i formula (instance). A clause is a six component vector. The first three components are the numbers of the variables in the clause. The rest three component indicate whether the literal is negated (0) or not (1). OUTPUT Formula{i,j} Last version 2/17/2009. Carlos Echegoyen (carlos.echegoyen@ehu.es)
0001 function [Formulas] = loadSAT(n, num_i, Formulas) 0002 % [Formulas] = loadSAT(n, mum_i) 0003 % loadMaxSAT: This function loads SAT instances from the SATLIB- benchmark 0004 % problems site (http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html). 0005 % It is only valid for the set of instances called Uniform 0006 % Random-3-SAT. In 'functions/sat/sat_instances' there are some examples. 0007 % 0008 % INPUT 0009 % n: number of variables 0010 % num_i: instance identifier 0011 % Formula{i,j}: Global variable that contains j clauses for the i formula (instance). A clause is a six 0012 % component vector. The first three components are the numbers of the 0013 % variables in the clause. The rest three component indicate whether the 0014 % literal is negated (0) or not (1). 0015 % 0016 % OUTPUT 0017 % Formula{i,j} 0018 % 0019 % Last version 2/17/2009. Carlos Echegoyen (carlos.echegoyen@ehu.es) 0020 0021 file = ['uf', num2str(n), '-0',num2str(num_i),'.cnf']; 0022 0023 f = fopen(file, 'r'); 0024 0025 for i=1:8 0026 Text{i} = fgetl(f); 0027 end 0028 0029 % Obtaining data form the text 0030 aux_s = size(Text{6}, 2); 0031 aux_cl = strcat(Text{6}(aux_s-2), Text{6}(aux_s-1), Text{6}(aux_s)); 0032 cl = str2num(aux_cl); % Clause length. (Max two digits for the length) 0033 0034 aux_s = size(Text{8},2); 0035 aux_nc = strcat(Text{8}(aux_s-4), Text{8}(aux_s-3), Text{8}(aux_s-2), Text{8}(aux_s-1), Text{8}(aux_s)); 0036 nc = str2num(aux_nc); % Number of clauses (Max four digits and min two digits for the number of clauses) 0037 0038 nf = size(Formulas,1); % number of formulas 0039 0040 % Obtaining the clauses. 0041 for j=1:nc 0042 aux = fgetl(f); 0043 aux = str2num(aux); 0044 Formulas{nf+1,j}(1:3) = abs(aux(1:cl)); 0045 Formulas{nf+1,j}(4:6) = aux(1:cl) > 0; 0046 end 0047 0048 fclose(f); 0049