# Proving a conjecture given a set of clauses - calculating complexity

I have written this Perl program to prove a conjecture given a set of clauses. I've actually posted some code from it on here in another question.

This time its all done and I've made it as fast as I need to make it.

Now, I want to calculate the Big O notation of the program. It's something I want to get better at because I learned it in a class last year but I was never very good at it.

I believe the Big O to be $O(n^4)$, but like I said, I'm no expert so I'm asking you to help me out.

Also, feel free to criticize my code if you feel it's sub-par.

#!/usr/bin/perl

use v5.14;
#use warnings;
use Getopt::Long; #use with options
$|=1; # This 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. # Subsumption can be turned on with the --sub option. # This is recommended in most cases. #Algorithm: #1.) Add the negation of the conjecture to the SOS set. #2.) For each clause (S) is the SOS. # 3.)For each clause (C) in the knowledge base # 4.) Compare clause S to clause C # 5.) If subsumption is possible, perform subsumption. # 6.) If resolution is possible, perform the resolution. # 7.) If the newly generated clause is the null clause: Go to 13. # 8.) Otherwise, check to see if the newly generated clause is already in # the knowledge base: # 9.) If the clause is already in the knowledgebase: Go to 3. # 10.) Else (if the clause is not already in the knowledge base): # 11.)Add the clause to the SOS. # 12.)Add the clause to the knowledge base #13.) If the null clause was generated, you have proved the conjecture to be #true. If it was not generated, the conjecture was false. #14.) Inform the user accordingly my$conclusion;
my $conclusion2; my @conclusion; my @SOS; my @clauses; my$found=0;

my $subsumption=0; GetOptions( 'sub' => \$subsumption);

#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];
@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 Theorem Prover!"; say "How many clauses are in your knowledge base?"; say "(this does not include the conclusion)"; print "Amount: "; my$amt = <>;

say "Negations can be indicated with a '~'.";
say "Variable names must contain only letters.";
say "Separate each literal with a ',' and be sure not to use the same";
say "variable twice in the same clause\n";

while($count <$amt)
{
print "clause $count:";$clauses[$count] .= <>;$clauses[$count] =~ s/[^A-Za-z~,]//g;$count++;
print "\n";
}

print "\n \n \n Enter the conjecture, the conjecture 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); } #add the new conclusion and make @clauses 2d$_ = [split /,/ ] for @clauses;
$clauses[$count][0] = $conclusion2; } #sort all clauses for my$unsorted (0 .. $#clauses) { @{$clauses[$unsorted] } = sort ( @{$clauses[$unsorted] }); } print "Beginning search ...."; ################################################## #Begin search algorithm$SOS[0][0] = $conclusion2; my$initial = $#clauses; my$offset = 1;
my %known_clauses;
for my $i (0 ..$#clauses)
{
my $key = join ( '', sort(@{$clauses[$i]}));$known_clauses{$key} =$i;
}

my $subs = 0; say "\nworking......"; my %generated_with; #for use when printing my$flag = 0; #for use when printing
SOS_ROW:
for (my $sos_row = 0;$sos_row <=$#SOS;$sos_row++)
{

&display_status($sos_row); my$current_sos_row = $SOS[$sos_row];

CLAUSE_ROW:
for (my $clause_row = 0;$clause_row <= $#clauses ;$clause_row++)
{

if($subsumption) { my$matches = 0;
for (@{$SOS[$sos_row]})
{
if ($_ ~~ @{$clauses[$clause_row]}) {$matches++;
}
}
my $size = @{$clauses[$clause_row]}; if ($matches == $size) { splice (@clauses,$clause_row, 1);
$clause_row--;$subs++;
}
}

my $current_clause_row =$clauses[$clause_row]; my @new_clause = sort (&resolves($current_sos_row,$current_clause_row)); my$new_clause = join ('', @new_clause);
if(!($new_clause eq '0')) { #resolution occurred, so check to see if #the clause already exists before adding it in. if( exists$known_clauses{$new_clause}) { next CLAUSE_ROW; } #okay its new, so add it to the sets push(@SOS, \@new_clause); push(@clauses, \@new_clause); my$current_clause = $initial +$offset;
$known_clauses{$new_clause} = $current_clause; #also, remember which clauses generated this one my$g1 = $known_clauses{join ('', @{$current_clause_row})};
my $g2 =$initial + $sos_row;$generated_with{$current_clause} = "($g1,$g2)"; #if resolution occurred, but$new_clause is empty
$offset++; if(!$new_clause)
{
$flag = 1; } if($flag == 1)
{
last SOS_ROW;
}
}
}
}
open(RESULTS, ">", 'results.txt');
say RESULTS "\n";
&printClauses;
if($subsumption) { say RESULTS "\n\n$subs subsumptions were made.";
}

if($flag) { say RESULTS "\n\nGood news! A resolvent was found and the empty set was generated."; say RESULTS "This means that when the negation of '$conclusion' is added to the knowledge base, a contradiction renders the knowledge base false.";
say RESULTS "Because we know that the clauses in the knowledge base are actually true, we can soundly conclude that '$conclusion' must also be true."; say RESULTS "The clauses generated by each resolution can be found above.\n\n\n"; } else { say RESULTS "\n\nUnfortunately, we were not able to generate the empty clause."; say RESULTS "This means that adding the negation of the desired conclusion does not create a contradiction in our knowledge base."; say RESULTS "Therefore, we can not safely conclude that '$conclusion' is true.";
say RESULTS "Any clauses that we were able to generate through a resolution can be viewed above\n\n\n";
}
print more results.txt;

close(RESULTS);

#if a resolution is possible, return the new clause as an array
#if not, return 0.
sub resolves
{
my $removed; my @sosR = @{$_[0]};
my @clauseR = @{$_[1]}; my %seen; for(@sosR) {$seen{$_}= 1; } SOS: for my$i (0 .. $#sosR) { for my$j (0 .. $#clauseR) { if("$sosR[$i]" eq "~$clauseR[$j]" || "$clauseR[$j]" eq "~$sosR[$i]") { splice(@sosR,$i, 1);
splice(@clauseR, $j, 1);$removed = 1;
last SOS;
}
}
}
if(!$removed) { return 0; } for(@clauseR) { if(!$seen{$_} ) { push(@sosR, "$_");
}
}

return @sosR;

}

sub display_status
{
my ($round) = @_; print "\n" if$round % 35 == 0;
print ".";
}

sub printClauses
{
foreach my $name (sort {$known_clauses{$a} <=>$known_clauses{$b} } keys %known_clauses) { my$indx = $known_clauses{$name};
my $clause = "clause$indx:\t";
$clause .= "{"; my @name = split ('',$name);
for my $i (0 ..$#name)
{
$clause.=$name[$i]; unless ($i == $#name ||$name[$i] eq "~") {$clause .= ",";
}
}
$clause .= "}"; #will generate some warnings (because the initial clauses have no parents to print) printf RESULTS ("%-25s\t%15s\n",$clause, $generated_with{$known_clauses{$name}}); if($indx == $initial) { say RESULTS "____________________________________________________________________"; } } }  EDIT: Some sample input-output to help you understand: Command line usage: perl ResRef.perl clauses.txt Input file: clauses.txt a,b,c ~b,c ~c ~a  (The clauses in the knowledge base are the first 3 lines and the last line is the negated conjecture, so we are trying to prove a is true.) Output would be something like this: clause 0: {a,b,c} clause 1: {~b,c} clause 2: {~c} clause 3: {~a} ________________________ clause 4: {b,c} (0,3) clause 5: {c} (1,4) clause 6: {b} (2,4) clause 7: {} (2,5)  Good news! We found the empty clause. • To help us understand what this code does, could you provide some sample inputs and outputs? – 200_success Apr 30 '14 at 19:21 • Why is use warnings; commented out? You should also add use strict;. – Ingo Bürk Apr 30 '14 at 20:05 • Also, Perl has cool things like $flag = 1 unless \$new_clause. Not sure if you purposely avoided it – I'm actually not sure if this could be considered bad practice (I'm not that proficient in Perl). – Ingo Bürk Apr 30 '14 at 20:06
• use 5.14 takes care of use strict and I turned off the warnings after I was done writing the program because It always produces some annoying warnings in the beginning. I know why they appear and it doesn't effect the program. – Luke Apr 30 '14 at 20:12