Multi-objective satisfiability problem

In the multi-objective version of the satisfiability (SAT) problem, there are m formulas, each representing a different objective. The goal is to satisfy the maximum number of clauses in each formula. The code below implements a Bayesian network based EDA for multi-objective 3-SAT.

The global variable Formulas stores the formulas that are read from the file. In this example, there are 20 binary variables, 10 formulas and 20 clauses in each formula. ParetoRank_ordering is used as the ordering criterion and truncation selection is applied.

MATEDA-2.0 includes the method EvaluateSAT which evaluates a solution on a set of 3-SAT formulas contained in the global variable Formulas. The output is a multi-objective solution, one component corresponds to the evaluation of one formula. The method MakeRandomFormulas can be used to generate random instances of the multi-objective SAT problem and a number of these instances can be found in the folder ../MATEDA/functions/SAT/instances.

 %Bayesian network based EDA  for multi-objective 3-SAT
 %For details on the EDA application to the multi-objective 3-SAT problem, see (Santana_et_al:2009) 
 
 global Formulas;   % Global variable for SAT function
 load TypeForm_1_Form_1.mat; % Multi-objective SAT instance
 n = 20;  % Number of variables
 m = 10;  % Number of objectives
 c = 20;  % Number of clauses
 PopSize = 500;
 NumbVar = n;
 cache  = [1,1,1,1,1];
 Card = 2*ones(1,NumbVar);
 maxgen = 50;
 F = 'EvaluateSAT'; % 3-SAT function
 selparams(1:2) = {0.5,'ParetoRank_ordering'};
 sampling_params(1:3) = {PopSize,m,Obj_Card};
 BN_params(1:7) = {'k2',5,0.05,'pearson','bayesian','no'};
 edaparams{1} = {'learning_method','LearnBN',BN_params};
 edaparams{2} = {'sampling_method','SampleBN',sampling_params};
 edaparams{3} = {'selection_method','truncation_selection',selparams};
 edaparams{4} = {'replacement_method','best_elitism',{'ParetoRank_ordering'}};
 edaparams{5} = {'stop_cond_method','max_gen',{maxgen}};
 [AllStat,Cache]=RunEDA(PopSize,NumbVar,F,Card,cache,edaparams)