view release on metacpan or  search on metacpan

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

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

    # 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 (
        (   grep {
                ( defined $self->satisfiable( $_, $model )
                        and $self->satisfiable( $_, $model ) == 0 )
                    ? 1
                    : 0
            } @{$clauses}
        ) > 0
        );

    # Choose a new value to test by simply looping over the possible variables
    # and checking to see if the variable has been given a value yet.

    my $choice = $self->_choice( $variables, $model );

    # If there are no more variables to try, return false.

    return 0 if ( !$choice );

    # Recurse into two cases. The variable we chose will need to be either
    # true or false for the expression to be satisfied.
    return $self->solve( $variables, $clauses,
        $self->update( $model, $choice, 1 ) )    #true
        || $self->solve( $variables, $clauses,
        $self->update( $model, $choice, 0 ) );    #false
}

sub _choice {
    my ( undef, $variables, $model ) = @_;

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

# ### update
# Copies the model, then sets `choice` = `value` in the model, and returns it.
sub update {
    my ( $self, $copy, $choice, $value ) = @_;
    $copy = dclone($copy);

    $copy->{$choice} = $value;
    return $copy;
}

# ### resolve
# Resolve some variable to its actual value, or undefined.
sub resolve {
    my ( undef, $var, $model ) = @_;

    if ( substr( $var, 0, 1 ) eq "-" ) {
        my $value = $model->{ substr( $var, 1 ) };
        return !defined $value ? undef : $value == 0 ? 1 : 0;
    }
    else {
        return $model->{$var};
    }
}

# ### satisfiable
# Determines whether a clause is satisfiable given a certain model.
sub satisfiable {
    my ( $self, $clauses, $model ) = @_;

    my @clause = @{$clauses};

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

    #If any variable is true, then the clause is true.
    return 1
        if (
        (   grep {
                ( defined $self->resolve( $_, $model )
                        and $self->resolve( $_, $model ) == 1 )
                    ? 1
                    : 0
            } @{$clauses}
        ) > 0
        );

    # Otherwise, we don't know what the clause is.
    return undef;
}

1;
__END__

=encoding utf-8