File Coverage

blib/lib/Algorithm/SAT/Backtracking/Ordered/DPLL.pm

Criterion	Covered	Total	%
statement	39	48	81.2
branch	8	14	57.1
condition	1	11	9.0
subroutine	8	9	88.8
pod	1	1	100.0
total	57	83	68.6

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

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

sub _up {
    my $self      = shift;
    my $variables = shift;
    my $clauses   = shift;
    my $model     = defined $_[0] ? shift : Hash::Ordered->new;

    #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    = shift;
    my $literal = shift;
    my $clauses = shift;
    my $model   = shift;
    $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      = shift;
    my $variables = shift;
    my $model     = shift;
    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

=head1 SYNOPSIS


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

    my $expr = Algorithm::SAT::Expression->new->with("Algorithm::SAT::Backtracking::Ordered::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::Ordered::DPLL;
    my $solver = Algorithm::SAT::Backtracking::Ordered::DPLL->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::Ordered::DPLL is a pure Perl implementation of a DPLL SAT Backtracking solver, in this variant of L we keep the order of the model updates and return a L as result.

Look at L for a theory description.

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

L use this module to solve Boolean expressions.

=head1 METHODS

Inherits all the methods from L and override/implements the following:

=head2 SOLVE

    $expr->solve();

in this case returns a L.

=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-mail]

=head1 SEE ALSO

L, L, L, L

=cut