I'm writing a Perl program to take a set of clauses and a conclusion literal and produce a resolution-refutation proof (if possible) using a breadth-first set of support (SOS) search algorithm.
The actual searching part of the program runs extremely slow, because I have many nested loops. I imagine it may also have to do with the system calls for the I/O taking place, but I'm not sure.
Here is the code for the searching part of the program.
@clauses
and @SOS
are both 2D arrays. The @clauses
contain all of the clauses including the negated conclusion. In the beginning of the algorithm you see @SOS
gets initialized with the negated conclusion as its only value. It then grows with clauses as resolutions are found.
#Begin breadth-first/SOS search/add algorithm
$SOS[0][0]=$conclusion2;
my $cSize=@clauses;
say "\nworking......";
my $dots=0;
SOSROW:
for(my $a; $a<@SOS; $a++)
{
if((($dots % 7) ==0))
{
print "\n";
}
if($dots==14)
{
print "You might want to get some coffee.\n";
}
if($dots==35)
{
print "I'm being VERY Thorough.\n";
}
if($dots==63 || $dots==140)
{
print "Hows that coffee?\n";
}
if($dots==105)
{
print "I think it might be time for a second cup of coffee\n"
}
print ".";
$dots++;
#Iterate through each clause on tier i
CLAUSEROW:
for(my $i=0; $i<@clauses; $i++)
{
SOSCOL:
for(my $b; $b<=$#{@SOS[$a]};$b++)
{
CLAUSECOL:
for(my $j=0; $j<=$#{@clauses[$i]}; $j++)
{
if($SOS[$a][$b] eq "~$clauses[$i][$j]"
|| $clauses[$i][$j] eq "~$SOS[$a][$b]")
{
my @tmp;
#Found a resolution, so add all other literals from
#both clauses to each set as a single clause
##*Algorith improvement**##
# First add them to a temporary array, then add them to the actual lists,
# only if the clause does not already appear.
#Start with the SOS literals (use a hash to keep track of duplicates)
my %seen;
for(my $c=0; $c<$#{@SOS[$a]}+1; $c++)
{
if($c != $b)
{
$seen{$SOS[$a][$c]}=1;
push @tmp, "$SOS[$a][$c]";
}
}
#Now add the literals from the non-SOS clause
for(my $k=0; $k<$#{@clauses[$i]}+1; $k++)
{
if($k != $j)
{
if(!$seen{$clauses[$i][$k]})
{
push @tmp,"$clauses[$i][$k]";
}
}
}
#Check to see if the clause is already listed
my $dupl='not';
my @a1=Unicode::Collate->new->sort(@tmp);
my $s1= join(undef, @a1);
for(my $i=0; $i<@clauses; $i++)
{
my @a2= Unicode::Collate->new->sort(@{@clauses[$i]});
my $s2= join(undef,@a2);
if($s1 eq $s2 )
{
$dupl ='did';
}
}
if($dupl eq 'not')
{
my $s=$cSize+$cAdd;
$res++;
$sAdd++;
$cAdd++;
push @{$SOS[$sAdd]}, @tmp;
push @{$clauses[$s]}, @tmp;
#Print out the new clauses.
print RESULTS"clause $s: ";
my $clause = $cSize+$a-1;
if($SOS[$sAdd][0])
{
print RESULTS "{";
for(my $j=0; $j<$#{@clauses[$s]}+1; $j++)
{
if($clauses[$s][$j])
{
print RESULTS "$clauses[$s][$j]";
}
if($j!=$#{@clauses[$s]})
{
print RESULTS ",";
}
}
print RESULTS "} ($i,$clause)\n";
}
#If you found a new res, but there was nothing to push, you found
# the contradiction, add {} as a clause, signal that you're done and break.
else
{
print RESULTS "{} ($i, $clause)\n";
$flag=1;
last SOSROW;
}
}
}
}
}
}
}
close(RESULTS);
I am interested in ways to possibly improve this code without changing the searching method (that is, breadth-first SOS).
As it stands, it works okay for small sets, but with sets with a lot of clauses, or rather, a lot of literals in the clauses, it takes a really long time to complete. For example, I just ran it on a file containing 16 clauses. The largest clause had 16 literals. It took about 24 hours to complete.
I also welcome any and all criticism of my code, no matter how harsh (as long as it's constructive).
EDIT: I feel that multi-threading would be a good solution, but now I'm trying to figure out the best place to use threads. I've decided to use two threads because, I'm not sure what machine will be running this program, but I can be fairly certain it will have at least two cores.
Actually, is there an environment variable that could tell me how many cores the CPU has, or that I could parse the number from? That way I could dynamically determine the thread amount.
Either way, I have two ideas so far
I am thinking I could break up the second loop into multiple concurrent threads so each time the outer-most loop finished, the second loop (checking the SOS clause against all other clauses) could be broken up into x groups that are executed concurrently.
Or, because on each pass of the outer loop, multiple clauses could be added to the SOS set, I could break that group up and check them against the other clauses concurrently, instead of sequentially.
Is there any reason one solution would be better than the other?