view release on metacpan or  search on metacpan

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

            if $model
        and exists $model->{$literal}
        and $model->{$literal} == 0;    #avoid cycle if already set
        #remove the literal from the model (set to false)
    $model->{$literal} = 0;

    #remove the literal from the model (set to false) and delete it from index

    $self->_delete_from_index( $literal, $clauses );

    return 1;
}

sub _add_literal {
    my ( $self, $literal, $clauses, $model ) = @_;

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

sub _delete_from_index {
    my ( $self, $string, $list ) = @_;

    foreach my $c ( @{$list} ) {
        next if @{$c} <= 1;
        for ( my $index = scalar( @{$c} ); $index >= 0; --$index ) {
            do {
                splice( @{$c}, $index, 1 );
                $self->{_impurity}->{$string}--;
                }
                if $c->[$index]
                and $c->[$index] eq $string;    # remove certain elements
        }
    }
}

sub _remove_clause_if_contains {
    my ( $self, $literal, $list ) = @_;

    my $index = 0;
    while ( $index < scalar @{$list} ) {
        splice( @{$list}, $index, 1 )
            if grep { $_ eq $literal } @{ $list->[$index] };
        $index++;
    }

}

1;

=encoding utf-8

=head1 NAME

Algorithm::SAT::Backtracking::DPLL - A DPLL Backtracking SAT solver written in pure Perl

=head1 SYNOPSIS


    # You can use it with Algorithm::SAT::Expression
    use Algorithm::SAT::Expression;

    my $expr = Algorithm::SAT::Expression->new->with("Algorithm::SAT::Backtracking::DPLL");
    $expr->or( '-foo@2.1', 'bar@2.2' );
    $expr->or( '-foo@2.3', 'bar@2.2' );
    $expr->or( '-baz@2.3', 'bar@2.3' );
    $expr->or( '-baz@1.2', 'bar@2.2' );
    my $model = $exp->solve();

    # Or you can use it directly:
    use Algorithm::SAT::Backtracking;
    my $solver = Algorithm::SAT::Backtracking->new;
    my $variables = [ 'blue', 'green', 'yellow', 'pink', 'purple' ];
    my $clauses = [
        [ 'blue',  'green',  '-yellow' ],
        [ '-blue', '-green', 'yellow' ],
        [ 'pink', 'purple', 'green', 'blue', '-yellow' ]
    ];

    my $model = $solver->solve( $variables, $clauses );

=head1 DESCRIPTION

Algorithm::SAT::Backtracking::DPLL is a pure Perl implementation of a SAT Backtracking solver.

Look at L<Algorithm::SAT::Backtracking> for a theory description.

The DPLL variant applies the "unit propagation" and the "pure literal" technique to be faster.

Look also at the tests file for an example of usage.

L<Algorithm::SAT::Expression> use this module to solve Boolean expressions.

=head1 METHODS

Inherits all the methods from L<Algorithm::SAT::Backtracking> and implements new private methods to use the unit propagation and pure literal rule techniques.

=head1 LICENSE

Copyright (C) mudler.

This library is free software; you can redistribute it and/or modify
it under the same terms as Perl itself.

=head1 AUTHOR

mudler E<lt>mudler@dark-lab.netE<gt>

=head1 SEE ALSO

L<Algorithm::SAT::Expression>, L<Algorithm::SAT::Backtracking>, L<Algorithm::SAT::Backtracking::Ordered>, L<Algorithm::SAT::Backtracking::Ordered::DPLL>