++ed by:
FUKAI

1 PAUSE user
1 non-PAUSE user.

Ettore Di Giacinto
and 1 contributors

NAME

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

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 );

DESCRIPTION

Algorithm::SAT::Backtracking::Ordered::DPLL is a pure Perl implementation of a DPLL SAT Backtracking solver, in this variant of Algorithm::SAT::Backtracking::DPLL we keep the order of the model updates and return a Hash::Ordered as result.

Look at Algorithm::SAT::Backtracking::DPLL for a theory description.

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

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

METHODS

Inherits all the methods from Algorithm::SAT::Backtracking::DPLL and override/implements the following:

SOLVE

    $expr->solve();

in this case returns a Hash::Ordered.

LICENSE

Copyright (C) mudler.

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

AUTHOR

mudler <mudler@dark-lab.net>

SEE ALSO

Algorithm::SAT::Expression, Algorithm::SAT::Backtracking, Algorithm::SAT::Backtracking::Ordered, Algorithm::SAT::Backtracking::DPLL