view release on metacpan or  search on metacpan

lib/Algorithm/SAT/Backtracking/Ordered/DPLL.pm  view on Meta::CPAN

package Algorithm::SAT::Backtracking::Ordered::DPLL;
use Hash::Ordered;
use base "Algorithm::SAT::Backtracking::DPLL";
use Algorithm::SAT::Backtracking::DPLL
    "Algorithm::SAT::Backtracking::Ordered";
use strict;
use warnings;
our $VERSION = "0.13";

##Ordered implementation, of course has its costs
sub solve {
    my ( $self, $variables, $clauses, $model ) = @_;
    $model = Hash::Ordered->new if !defined $model;
    return $self->SUPER::solve( $variables, $clauses, $model );
}

sub _up {
    my ( $self, $variables, $clauses, $model ) = @_;
    $model = Hash::Ordered->new if !defined $model;

    #Finding single clauses that must be true, and updating the model
    ( @{$_} != 1 )
        ? ()
        : ( substr( $_->[0], 0, 1 ) eq "-" ) ? (
        do {
            my $literal = substr( $_->[0], 1 );
            $model->set( $literal => 0 );
            $self->_delete_from_index( $literal, $clauses );
            }

#remove the positive clause form OR's and add it to the model with a false value
        )
        : (
                $self->_add_literal( "-" . $_->[0], $clauses )
            and $model->set( $_->[0] => 1 )

        ) # if the literal is present, remove it from SINGLE ARRAYS in $clauses and add it to the model with a true value
        for ( @{$clauses} );
    return $model;
}

sub _add_literal {
    my ( $self, $literal, $clauses, $model ) = @_;
    $literal
        = ( substr( $literal, 0, 1 ) eq "-" )
        ? $literal
        : substr( $literal, 1 );
    return
            if $model
        and $model->exists($literal)
        and $model->set( $literal, 1 );    #avoid cycle if already set
         #remove the literal from the model (set to false)
    $model->set( $literal, 1 );
    $self->_delete_from_index( $literal, $clauses );
    return 1;
}

sub _choice {
    my ( $self, $variables, $model ) = @_;
    my $choice;
    foreach my $variable ( @{$variables} ) {
        $choice = $variable and last if ( !$model->exists($variable) );
    }
    return $choice;
}

1;

=encoding utf-8

=head1 NAME

Algorithm::SAT::Backtracking::Ordered::DPLL - A DPLL Backtracking SAT ordered implementation