Home > Mateda2.0 > functions > sat > LoadRandom3SAT.m

LoadRandom3SAT

PURPOSE ^

[Formulas] = loadSAT(n, mum_i)

SYNOPSIS ^

function [Formulas] = loadSAT(n, num_i, Formulas)

DESCRIPTION ^

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

CROSS-REFERENCE INFORMATION ^

This function calls: This function is called by:

SOURCE CODE ^

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

Generated on Fri 04-Dec-2009 13:38:29 by m2html © 2003