【发布时间】：2014-04-28 01:12:16
【问题描述】：
这个真的让我很困惑，我不知道如何准确地命名它。
我正在编写一个程序，目的无关紧要，但你们中的一些人可能知道，因为我最近一直在问一些关于它的问题。
我将发布整个程序，但我认为没有必要。您需要查看的部分是嵌套循环，其中显示“开始搜索算法”。
程序需要很长时间才能完成，所以在最外层循环的每次迭代之后，我都会打印一个“.”。每 7 个点后打印一个新行。 由于某种原因，在打印换行符之前不会打印任何点。
代码如下：
#!/usr/bin/perl
use v5.14;
use warnings;
# this is a cgi implementation of a theorum proover.
# the program uses resolution refutation, using a breadth-first and set of support strategy
# to generate a proof(if possible) and relay the results to the user.
########################################################################################
#Algorithm:
#1.) Get size(i) of knowledge base
#2.) untill you have i clauses
# 3.) get the clause, add to knowledge base
#4.) get the conclusion variable(conjecture)
#5.) add the negation of the conjecture to the knowledge base
#6.) add the negation of the conjecture to the SOS set.
#7.) compare the SOS set to ever other clause
# 8.) if resolution is possible, add the new clause to the knowledge base if it does not already exist.
# 9.) add the new clause to the SOS set.
#10.) repeat 7-9 untill the null clause is generated or no more resolution is possible.
########################################################################################
my $conclusion;
my $conclusion2;
my @conclusion;
my @SOS;
my @clauses;
my $found=0;
#batch mode
if($ARGV[0])
{
my $filename = $ARGV[0];
open(IN, "<", $filename);
chomp(@clauses=<IN>);
close(IN);
for(@clauses)
{
$_ =~ s/[^A-Za-z~,]//g;
}
#negate the negation to get the desired conclusion for later
$conclusion2=$clauses[$#clauses];
print "$conclusion2";
@conclusion = split("", $conclusion2);
if($conclusion[0] eq '~')
{
splice(@conclusion, 0, 1);
$found=1;
}
if (!$found)
{
$conclusion = "~$conclusion2";
}
else
{
$conclusion = join("", @conclusion);
}
#now break up each line and make @clauses 2d
$_ = [split /,/ ] for @clauses;
}
#interactive mode
else
{
my $count=0;
say "Welcome to my Theorum Proover!";
say "How many clauses are in your knowledge base?";
say "(this does not include the conclusion)";
print "Amount: ";
my $amt = <>;
say "Enter your clauses: ";
say "Negations can be indicated with a '~'.";
say "Variable names must contain only letters.";
say "Separate each literal with a ','<br>";
my $clauses;
while($count < $amt)
{
print "clause $count:";
$clauses .= <>;
$clauses =~ s/[^A-Za-z~,]//g;
$clauses .= ";";
$count++;
print "\n";
}
print "\n \n \n Enter the conclusion, your conclusion should be a literal:";
$conclusion = <>;
$conclusion =~ s/[^A-Za-z~]//g;
print "\n";
#negate the conclusion and add it to the set of clauses.
@conclusion = split("", $conclusion);
if($conclusion[0] eq '~')
{
splice(@conclusion, 0, 1);
$found=1;
}
if (!$found)
{
$conclusion2 = "~$conclusion";
}
else
{
$conclusion2 = join("", @conclusion);
}
# split up the contents of the clause string and add them to a 2d array.
#then, add the negated conclusion to the list.
my @PartClauses= split(';', $clauses);
my $last=@PartClauses;
for my $i (0 .. $#PartClauses)
{
my @tmp=split(',', $PartClauses[$i]);
for my $j (0 .. @tmp)
{
$clauses[$i][$j] = $tmp[$j];
}
}
$clauses[$last][0] = $conclusion2;
}
open(RESULTS, ">", 'results.txt');
for my $i (0 .. $#clauses)
{
print RESULTS "clause $i: {";
for my $j (0 .. $#{ $clauses[$i] })
{
print RESULTS "$clauses[$i][$j]";
if($j != $#{ $clauses[$i] })
{
print RESULTS ",";
}
}
print RESULTS "}\n";
}
print RESULTS "_____________________________\n";
print "Beginning search ....";
##################################################
#begin breadthfirst/sos search/add algorithm
$SOS[0][0]=$conclusion2;
my $cSize=$#clauses;
say "\nworking......";
my $sAdd=0;
my $cAdd=0;
my $res=0;
my $flag=0;
my $dots=0;
SOSROW:
for (my $a=0; $a<=$#SOS; $a++)
{
&update;
CLAUSEROW:
for (my $i=0; $i<=$#clauses; $i++)
{
SOSCOL:
for (my $b=0; $b<=$#{ $SOS[$a] }; $b++)
{
CLAUSECOL:
for my $j (0 .. $#{ $clauses[$i] })
{
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
#start with the SOS literals(use a hash to keep track of duplicates)
my %seen;
for my $x (0 .. $#{ $SOS[$a] })
{
if($x != $b)
{
$seen{$SOS[$a][$x]}=1;
push @tmp, "$SOS[$a][$x]";
}
}
#now add the literals from the non-SOS clause
for my $y (0 .. $#{ $clauses[$i] })
{
if($y != $j)
{
if(! $seen{ $clauses[$i][$y] })
{
push(@tmp, "$clauses[$i][$y]");
}
}
}
#check to see if the clause is already listed
my $dupl = 0;
my @a1 = sort(@tmp);
my $s1 = join("", @a1);
MATCH:
for my $i (0 .. $#clauses)
{
my @a2= sort(@{ $clauses[$i] });
my $s2= join("", @a2);
if($s1 eq $s2 )
{
$dupl = 1;
last MATCH;
}
}
#if it isn't, go ahead and add it in
if(! $dupl)
{
$res++;
$sAdd++;
$cAdd++;
my $s = $cSize + $cAdd;
push(@SOS, \@tmp);
push(@clauses, \@tmp);
#print out the new clauses.
print RESULTS"clause $s: ";
my $clause = $cSize+$a;
print RESULTS "{";
if($SOS[$sAdd][0])
{
for my $j(0 .. $#{ $clauses[$s] })
{
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, so signal and break.
else
{
print RESULTS "} ($i,$clause)\n";
$flag=1;
last SOSROW;
}
}
}
}
}
}
}
close(RESULTS);
if($flag)
{
say "After $res resolutions, a resolvent was found and the empty set was generated.";
say "This indicates that when '$conclusion' is false, the entire knowledge base is false.";
say "Because we know that the clauses in the knowledge base are actually true, we can soundly conclude that '$conclusion must also be true.";
say "The clauses generated by each resolution can be found below.\n\n";
}
else
{
say "We were not able to generate the empty clause.";
say "this means that adding the negation of the desired conclusion does not render the theorum false.";
say "Therefore, we can not safely conclude that '$conclusion' is true.";
say "Any clauses that we were able to generate through a resoluton can be viewed below.\n\n";
}
print `more results.txt`;
sub update
{
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"
}
if($dots==210)
{
print "Like I said, VERY thorough\n";
}
if($dots==630)
{
print "My O is bigger than you can imagine\n"
}
$dots++;
print ".";
}
我不明白为什么会这样。它可能与缓冲有关吗？
如果不调用子程序，我只说 print ".";在 prog 完成执行之前不会打印任何内容。
【问题讨论】：