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:

- EBNA_MultiObj_SAT % EXAMPLE 2: MULTIO-OBJECTIVE MAXSAT

## 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