view release on metacpan or  search on metacpan

README.md  view on Meta::CPAN

        [ '-blue', '-green', 'yellow' ],
        [ 'pink', 'purple', 'green', 'blue', '-yellow' ]
    ];

    my $model = $solver->solve( $variables, $clauses );

# DESCRIPTION

Algorithm::SAT::Backtracking is a pure Perl implementation of a simple SAT Backtracking solver.

In computer science, the Boolean Satisfiability Problem (sometimes called Propositional Satisfiability Problem and abbreviated as _SATISFIABILITY_ or _SAT_) is the problem of determining if there exists an interpretation that satisfies a given Boolea...

For example, the formula "a AND NOT b" is satisfiable because one can find the values a = **TRUE** and b = **FALSE**, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable. More: [https://en.wikipedia.org/wiki/Boolean\_satisfia...

Have a look also at the tests file for an example of usage.

[Algorithm::SAT::Expression](https://metacpan.org/pod/Algorithm::SAT::Expression) use this module to solve Boolean expressions.

# METHODS

## solve()

The input consists of a boolean expression in Conjunctive Normal Form.

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

        [ '-blue', '-green', 'yellow' ],
        [ 'pink', 'purple', 'green', 'blue', '-yellow' ]
    ];

    my $model = $solver->solve( $variables, $clauses );

=head1 DESCRIPTION

Algorithm::SAT::Backtracking is a pure Perl implementation of a simple SAT Backtracking solver.

In computer science, the Boolean Satisfiability Problem (sometimes called Propositional Satisfiability Problem and abbreviated as I<SATISFIABILITY> or I<SAT>) is the problem of determining if there exists an interpretation that satisfies a given Bool...

For example, the formula "a AND NOT b" is satisfiable because one can find the values a = B<TRUE> and b = B<FALSE>, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable. More: L<https://en.wikipedia.org/wiki/Boolean_satisfiabi...

Have a look also at the tests file for an example of usage.

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

=head1 METHODS

=head2 solve()

The input consists of a boolean expression in Conjunctive Normal Form.

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

        );
    return 1;

}

sub _pure {
    my ( $self, $literal ) = @_;

    #     Pure literal rule

    # if a variable only occurs positively in a formula, set it to true
    # if a variable only occurs negated in a formula, set it to false

    my $opposite
        = substr( $literal, 0, 1 ) eq "-"
        ? substr( $literal, 1 )
        : "-" . $literal;
    return 1
        if (
        (   exists $self->{_impurity}->{$literal}
            and $self->{_impurity}->{$literal} != 0
        )