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.


use v5.14;
#use warnings;
use Getopt::Long; #use with options 

# 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. 

#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
    my $filename = $ARGV[0];

    open(IN, "<", $filename);

    #additional clean up
        $_ =~ s/[^A-Za-z~,]//g;

    #negate the negation to get the desired conclusion for later
    @conclusion = split("", $conclusion2);

    if($conclusion[0] eq '~')
            splice(@conclusion, 0, 1);

    if (!$found)
         $conclusion = "~$conclusion2";
        $conclusion = join("", @conclusion);

    #now break up each line and make @clauses 2d
    $_ = [split /,/ ] for @clauses;


#interactive mode
    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 "Enter your clauses: ";
    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;
        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);
    if (!$found)
         $conclusion2 = "~$conclusion";
        $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
for (my $sos_row = 0; $sos_row <=$#SOS; $sos_row++) 


    my $current_sos_row = $SOS[$sos_row];

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

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

        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
                $flag = 1;

            if($flag == 1)
                last SOS_ROW;
open(RESULTS, ">", 'results.txt');
say RESULTS "\n";
    say RESULTS "\n\n $subs subsumptions were made.";

    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"; 
    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`;


#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;
        $seen{$_}= 1;
    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;
        return 0;
    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


(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.

  • 1
    \$\begingroup\$ To help us understand what this code does, could you provide some sample inputs and outputs? \$\endgroup\$ – 200_success Apr 30 '14 at 19:21
  • \$\begingroup\$ Why is use warnings; commented out? You should also add use strict;. \$\endgroup\$ – Ingo Bürk Apr 30 '14 at 20:05
  • \$\begingroup\$ 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). \$\endgroup\$ – Ingo Bürk Apr 30 '14 at 20:06
  • \$\begingroup\$ 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. \$\endgroup\$ – Luke Apr 30 '14 at 20:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.