Algorithm::SAT::Backtracking::DPLL - A DPLL Backtracking SAT solver written in pure Perl
# 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 );
Algorithm::SAT::Backtracking::DPLL is a pure Perl implementation of a SAT Backtracking solver.
Look at 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.
Algorithm::SAT::Expression use this module to solve Boolean expressions.
Inherits all the methods from Algorithm::SAT::Backtracking and implements new private methods to use the unit propagation and pure literal rule techniques.
Copyright (C) mudler.
This library is free software; you can redistribute it and/or modify it under the same terms as Perl itself.
mudler <mudler@dark-lab.net>
Algorithm::SAT::Expression, Algorithm::SAT::Backtracking, Algorithm::SAT::Backtracking::Ordered, Algorithm::SAT::Backtracking::Ordered::DPLL
To install Algorithm::SAT::Backtracking, copy and paste the appropriate command in to your terminal.
cpanm
cpanm Algorithm::SAT::Backtracking
CPAN shell
perl -MCPAN -e shell install Algorithm::SAT::Backtracking
For more information on module installation, please visit the detailed CPAN module installation guide.