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

test_ce_satA.m
%
%  Test  for the SAT solver by a Cross-Entropy (CE) optimization algorithm
%  see http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html for database



clear, clc, close all hidden

database          = {'uf20-01' , 'uf20-010' , 'uf20-0100' , 'uf50-01' ,'uf75-01', 'aim-50-1_6-yes1-1' , 'aim-50-1_6-yes1-2','aim-100-1_6-yes1-1'  , 'aim-100-2_0-yes1-1','aim-200-2_0-yes1-3','g125_17' , '2bitcomp_5' , '2bitmax_6'  };

numbase           = 5;

database{numbase}



load(database{numbase}); 
 
n                 = size(A , 2);
 
option.N          = 100000;
option.rho        = 0.1;
option.alpha      = 0.9;
option.d          = 50;
option.T_max      = 1000;
option.theta_min  = 0.05;
option.theta_max  = 0.99;

tic,out           = ce_satA(A , option);,toc

disp(sprintf('\n Pourcentage of Satisfied clauses = %5.2f%% (%d/%d), card(X) = %d' , 100*(out.S_opt/S_opt) , out.S_opt , S_opt , size(out.X , 2)))


figure(1)
plot(1:length(out.St) , out.St , 1:length(out.St) , repmat(size(A , 1) , 1 , length(out.St)) , 'r' , 'linewidth' , 2)
grid on
xlabel('Iterations')
title(sprintf('\n   Satisfied clauses = %5.2f%% (%d/%d), #(X) = %d' , 100*(out.S_opt/size(A , 1)) , out.S_opt , size(A , 1) ,size(out.X , 2)) , 'fontsize' , 13)

Contact us at files@mathworks.com