view release on metacpan or  search on metacpan

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

package Algorithm::SAT::Backtracking::DPLL;
use Storable qw(dclone);
use Data::Dumper;
use strict;
use warnings;
our $VERSION = "0.13";

# this allow to switch the parent implementation (needed for the Ordered alternative)
sub import {
    my ( $class, $flag ) = @_;
    if ($flag) {
        eval "use base '$flag'";
    }
    else {
        eval "use base 'Algorithm::SAT::Backtracking'";
    }
}

sub solve {

    # ### solve
    #
    # * `variables` is the list of all variables
    # * `clauses` is an array of clauses.
    # * `model` is a set of variable assignments.
    my ( $self, $variables, $clauses, $model ) = @_;
    $model = {} if !defined $model;
    my $impurity = dclone($clauses);

    if ( !exists $self->{_impurity} ) {
        $self->{_impurity}->{$_}++ for ( map { @{$_} } @{$impurity} );
    }

    # If every clause is satisfiable, return the model which worked.
    return $model
        if (
        (   grep {
                ( defined $self->satisfiable( $_, $model )
                        and $self->satisfiable( $_, $model ) == 1 )
                    ? 0
                    : 1
            } @{$clauses}
        ) == 0
        );

    # If any clause is **exactly** false, return `false`; this model will not
    # work.
    return 0 if !$self->_consistency_check( $clauses, $model );

    $model = $self->_up( $variables, $clauses, $model )
        ;    # find unit clauses and sets them

    return 0 if !$self->_consistency_check( $clauses, $model );

    # TODO: pure unit optimization
    # XXX: not working

#   $self->_pure($_)
#     ? ( $model->{$_} = 1 and $self->_remove_clause_if_contains( $_, $clauses ) )
#     : $self->_pure( "-" . $_ )
#     ? ( $model->{$_} = 0 and $self->_remove_clause_if_contains( $_, $clauses ) )
#    : ()
#     for @{$variables};