3
\$\begingroup\$

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?

\$\endgroup\$
4
  • \$\begingroup\$ would using multiple threads help at all? \$\endgroup\$
    – user3002620
    Commented Apr 27, 2014 at 16:31
  • \$\begingroup\$ if you can split your job into chunks, why not? \$\endgroup\$
    – mpapec
    Commented Apr 27, 2014 at 16:54
  • \$\begingroup\$ the thing is I've never used multi threading before, so I'm not sure how I would go about implementing it. could I divide the clauses to be compared into x separate groups and have them compared in parallel. But then, how would I decide how many groups. It depends on the machine and how many processors it has, right? \$\endgroup\$
    – user3002620
    Commented Apr 27, 2014 at 17:21
  • \$\begingroup\$ think of threading like running your script multiple times, but on separate data sets. If you can make separate data sets, you can also run them in parallel. \$\endgroup\$
    – mpapec
    Commented Apr 27, 2014 at 18:36

4 Answers 4

4
\$\begingroup\$

I found the general style of your program hard to read. You use 8-space indentation but have so many levels that the most of your code isn't visible without scrolling. Other for indentation, you use very little spaces in your code, for example around operators. This line:

for(my $j=0; $j<=$#{@clauses[$i]}; $j++) {

Could be made more readable as

for(my $j = 0; $j <= $#{ @clauses[$i] }; $j++) {

I used the automatic Perl code formatter “Perl::Tidy” with a configuration I use, which produced the more readable below output. All I did manually was to reflow the comments and remove empty lines.

# begin breadthfirst/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 tmp 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);

The most crucial issues with this code besides formatting are mentioned by Borodin in his answer.

Beyond those issues, I made the following observations:

  • you did join(undef, @a1). This makes very little sense, if you want to join strings without a delimiter, use the empty string: join('', @a1).

  • You perform an Unicode sort Unicode::Collate->new->sort(@tmp), and that multiple times. Unless there is a real need for this, I'd recommend to use the faster builtin sort: sort @tmp. Here there is no need, and you just need the sorting to be consistent.

  • You use the variable $dup as a boolean flag with values "not" or "dup". Instead, choose a proper variable name and use values that are boolean on their own:

    my $found_duplicates = 0;
    ...
        $found_duplicates = 1;
    ...
    if (not $found_duplicates) {
       ...
    
  • The provided code snippet refers to many variables that are declared outside of this snippet (if they are declared at all). These have very broad scopes, which is a bad sign.

  • You regularly output some status (usually a period, every seven periods a line, and sometimes a quip). I'd suggest moving this code into a separate subroutine so the actual algorithm is less cluttered. Your loop would then only contain a simple display_status($dots++).

    my %quips = (
        14 => "You might want to get some coffe",
        35 => "I'm being VERY thorough",
        ...
    );
    
    sub display_status {
        my ($round) = @_;
        print "\n" if $round % 7 == 0;
        print "$quips{$round}\n" if exists $quips{$round};
        print ".";
    }
    
  • Initialize all your variables. All of them, without excuse. use warnings if you need a friendly reminder.

  • Some of your search loops can be terminated early when you've found something. E.g.

    # 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';
        }
    }
    

    could be improved to

    # check to see if the clause is already listed
    my $found_duplicates = 0;
    my $s1 = join '', sort @tmp;
    
    CLAUSE:
    for my $clause (@clauses) {
        my $s2 = join '', sort @$clause;
        if ($s1 eq $s2) {
            $found_duplicates = 1;
            last CLAUSE;
        }
    }
    
  • Use foreach loops wherever you can, e.g. for my $clause (@clauses) rather than using indices.

  • This code is basically replicating join:

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

    It can be simplified to

    my $list_of_clauses = join ',', map { $_ || '' } @{ $clauses[$s] };
    say RESULTS "{$list_of_clauses} ($i, $clause)";
    

    This needs a bit of explanation. map is a function that takes a block and a list. It sets $_ to each element of the input list in turn and then evaluates the block. The result of the block is added to the output list:

    my @output;
    for (@input) {
        push @output, the_block($_);
    }
    

    So for each element map { $_ || '' } @list returns the list element if it's true-ish, or the empty string otherwise.

Edit: comprehensive refactoring

I went through the code and gradually improved it. There are many optimizations that can be employed, such as calculating data structures in the outermost possible loop, or using hashes for linear-time lookup. I also tried to rename most variables to something sensible. This should have lowered the algorithmic complexity of the outer loops from \$O(n^2 \cdot m^2)\$ to \$O(n^2 \cdot m)\$ (which isn't much in the grand scheme of things, but might still be a 16× speedup under some input). More importantly, in many parts my refactoring should have a far lower constant factor.

I could have employed further optimizations if I'd known the exact initial makeup of @SOS and @clauses. For example certain checks have to added when elements can be undef, or when the input clauses might contain duplicate elements. Furthermore the input is currently treated as strings. If they are actually numbers or can be mapped to numbers, certain simplifications could be employed.

After having spent a lot of time with this code, I've come to the conclusion that this problem is not easily parallelizable. Certainly, it would be possible to run the MATCH loop inside worker threads which get passed a pair of rows and return a bunch of new clauses. A main thread would then aggregate the new clauses and extend your data structures, then dispatch new jobs. However, the speedup obtainable in this way is likely to be small compared with other optimizations you could take (such as rewriting part of the program in C, or doing more caching of data structures that get recalculated).

# begin breadthfirst/sos search/add algorithm
$SOS[0][0] = $conclusion2;

my $initial_clause_offset = $#clauses;

my %known_clauses;
for my $clause (@clauses) {
    my $key = join '', sort @$clause;
    $known_clauses{$key} = 1;
}

say "";
say "working......";

SOS_ROW:
for (my $sos_row = 0 ; $sos_row < @SOS ; $sos_row++) {
    my $the_sos_row = $SOS[$sos_row];

    display_status($sos_row);

    # build the hash of seen elements for this row
    my %seen;
    $seen{$_}++ for @$the_sos_row;

    CLAUSE_ROW:
    for (my $clause_row = 0 ; $clause_row < @clauses ; $clause_row++) {
        my $the_clause_row = $clauses[$clause_row];

        MATCH:
        for my $match (find_matches($the_sos_row, $the_clause_row)) {
            my ($sos_col, $clause_col) = @$match;

            # We found a resolution, so we combine all other literals from
            # both clauses to each a single new clause.
            # We add the new clause only if it isn't already known

            # make a copy of the SOS clause
            # and remove the $sos_col-th element
            my @sos_literals = @$the_sos_row;
            my $removed = splice @sos_literals, $sos_col, 1;

            # shadow-delete the $removed element from the hash
            # but only if it was seen once. It will be there again in the next
            # loop iteration. This is admittedly a bit arcane.
            local $seen{$removed} = $seen{$removed};
            delete $seen{$removed} if $seen{$removed} == 1;

            # copy the literals from the non-SOS clause
            # and remove $clause_col-th element
            # and remove seen elements
            my @non_sos_literals = @$the_clause_row;
            splice @non_sos_literals, $clause_col, 1;
            @non_sos_literals = grep { not $seen{$_} } @non_sos_literals;

            my @new_clause = sort(@sos_literals, @non_sos_literals);
            my $new_clause_key = join '', @new_clause;

            # skip this new clause if the clause is already known
            next MATCH if $known_clauses{$new_clause_key};

            # else add this clause to the known clauses etc.
            push @SOS,     \@new_clause;
            push @clauses, \@new_clause;
            $known_clauses{$new_clause_key} = 1;
            $res++;

            # print out the new clauses.
            my $clause = $initial_clause_offset + $sos_row;
            my $list_of_clauses = join ',', map { $_ || '' } @new_clause;
            say RESULTS
                "clause $#clauses: {$list_of_clauses} ($clause_row, $clause)";

            # 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.
            if (not @new_clause) {
                $flag = 1;
                last SOS_ROW;
            }
        }
    }
}

close(RESULTS);

# Return pairs of indices for all matching elements between the two arrays.
# Only uses O(n + m) complexity!
sub find_matches {
    my ($sos_row, $clause_row) = @_;

    # build a hash of clause items that map to their columns
    # in principle, this could be cached.
    my %clause_col;
    for my $i (0 .. $#$clause_row) {
        $clause_col{ $clause_row->[$i] } = $i;
        $clause_col{ '~' . $clause_row->[$i] } = $i;
    }

    # we now look up possible matching items,
    # and add the indices to the matches
    my @matches;
    for my $sos_col (0 .. $#$sos_row) {
        my $item = $sos_row->[$i];
        my $clause_col = $clause_col{$item} // $clause_col{"~$item"};
        push @matches, [ $sos_col, $clause_col ] if defined $clause_col;
    }

    return @matches;
}

my %quips;

BEGIN {
    %quips = (
        14  => "You might want to get some coffe",
        35  => "I'm being VERY thorough",
        63  => "How's that coffee?",
        105 => "I think it might be time for a second cup of coffee",
        140 => "How's that coffee?",
    );
}

sub display_status {
    my ($round) = @_;
    print "\n" if $round % 7 == 0;
    print "$quips{$round}\n" if exists $quips{$round};
    print ".";
}
\$\endgroup\$
1
  • \$\begingroup\$ added a fairly comprehensive refactoring that should result in much faster run time. \$\endgroup\$
    – amon
    Commented Apr 27, 2014 at 21:51
7
\$\begingroup\$

You seem to have taken away little from my efforts to help you write good Perl code. In particular you must add

use warnings

to the top of every Perl program, which in this case would have resulted in line after line of errors like

Scalar value @clauses[$s] better written as $clauses[$s]

You also should use Perl's range iterator. The C-style for loop is a clumsy tool, and you are also mixing together $#array, $#array + 1, @array, and @array - 1 in your loop limits.

To iterate over the indices of a Perl array you should write

for my $i (0 .. $#array) {
  ...
}

unless you have a strange and unusual requirement. It is also best to keep to $i, $j, $k etc. for array indices as everyone knows what they mean. $s is usually a string, and $a and $b are fobidden because they are used by the Perl sort engine.

So your loops

for (my $i = 0; $i < @clauses; $i++) { ... }

for (my $j = 0; $j < $#{ @clauses[$s] } + 1; $j++) { ... }

should be

for my $i (0 .. $#clauses) { ... }

for my $j (0 .. $#{ $clauses[$i] }) { ... }

which I hope you will agree is much more readable.

If you make at least these changes then you will get a lot more help from people who will then be able to understand your code better.

\$\endgroup\$
7
  • \$\begingroup\$ again, Borodin, I have use v5.14. this is only a segment as I said. I meant to ask you, if use 5.14 only turns on strict and not warnings, because I get no such errors. yes that does appear more readable, i suppose. I am used to the c style and thats what i was using, so in my error checking I could be sure that my syntax wasn't causing an error. I will get to changing that. Also, is using a/b actually affecting my program? or just bad practice. finally, any input on the multi-threading thing? \$\endgroup\$ Commented Apr 27, 2014 at 19:04
  • \$\begingroup\$ never mind obviously i doesn't i just tried it. I could have sworn i remember reading in the orielly book that it does, that would have helped me out a lot \$\endgroup\$ Commented Apr 27, 2014 at 19:06
  • 1
    \$\begingroup\$ @user3002620: You did ask me and I answered you here \$\endgroup\$
    – Borodin
    Commented Apr 27, 2014 at 19:07
  • 1
    \$\begingroup\$ @user3002620: I can't tell whether your misuse of $a and $b is affecting anything because I can't see your full program, but it is a far better solution just to avoid them, then I can be certain that you aren't causing a problem; that is why good practice is good practice. I can't make a recommendation on how to optimise your code until you have written it so that I can see what it is doing. That is why I am offering you advice to improve the legibility of your code. It should need no comments, or very few, to make it comprehensible. \$\endgroup\$
    – Borodin
    Commented Apr 27, 2014 at 19:12
  • \$\begingroup\$ oh yep, i skipped right over that last sentence. I should have just tried it immediately. But my program was running while I was talking to you and I was running it over a remote connection in which i couldn't open another window or tab to check. \$\endgroup\$ Commented Apr 27, 2014 at 19:12
1
\$\begingroup\$

These answers are great, but they're all missing one simple thing.

I know you said you want to stick with the breadth-first SOS algorithm.

and you can/should, but have you considered adding subsumption capabilities to your code?

It would only take a couple of lines above that first inner loop.

My bet is that it's the large amount of values in the arrays that's causing the slowdown and not the actual amount of arrays.

Best case scenario, jobs that take hours now, only take seconds with subsumption.

\$\endgroup\$
0
\$\begingroup\$

There is unlikely to be any benefit from multithreading your application until you have identified a section of code that is most responsible for any delay.

In general, a program that could benefit from multithreading will divide its time between CPU-intensive and IO-intensive sections.

If your program does little or no IO and just uses the CPU sequentially until it finds a result (think of something like calculating π to many decimal places) then there is no benefit in multithreading.

Likewise, if the CPU has very little to do except wait until comparatively snail-paced IO to complete (suppose the task is to copy one disk file to another) then again there is no purpose in multithreading.

Where multithreading can give huge benefits is if the amount of processing is more or less equal to the time taken communicating with external devices. In that case a process can prepare the contents of the next output during the time taken to deliver the previous set of data.

Ideal balances like that are rare, and it is much more common that the overheads of multi-threading outweigh the benefits. In particular it is left to the operating system to divide the CPU workload between the available processors, and since you have no control over that decision it may well be that a single-threaded solution is the optimal one.

In the end there is a limit to how fast any given machine can execute the algorithm that you have coded. Unless there are obvious places in your program where useful processing could be done while waiting for IO to complete, it is unlikely that clever coding can compete with what the operating system already does.

\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.