[![Build Status](https://travis-ci.org/mudler/Algorithm-Sat-Backtracking.png?branch=master)](https://travis-ci.org/mudler/Algorithm-Sat-Backtracking)
# NAME

Algorithm::SAT::Backtracking - A simple Backtracking SAT solver written in pure Perl

# SYNOPSIS

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

    $model = {
          'green' => 1,
          'yellow' => 1,
          'blue' => 1
    }

# 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 Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values **TRUE** or **FALSE** in such a way that the formula evaluates to **TRUE**.

If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is identically **FALSE** for all possible variable assignments and the formula is unsatisfiable.

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\_satisfiability\_problem](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem) .

Look also at the test 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.
This means it looks something like this:

    `(blue OR green) AND (green OR NOT yellow)`

    We encode this as an array of strings with a `-` in front for negation:

       `[['blue', 'green'], ['green', '-yellow']]`

Hence, each row means an **AND**, while a list groups two or more **OR** clauses.

Returns 0 if the expression can't be solved with the given clauses, the model otherwise.

Have a look at [Algorithm::SAT::Expression](https://metacpan.org/pod/Algorithm::SAT::Expression) to see how to use it in a less painful way.

## resolve()

Uses the model to resolve some variable to its actual value, or undefined if not present.

    my $model = { blue => 1, red => 0 };
    my $a=$solver->resolve( "blue", $model );
    #$a = 1

## satisfiable()

Determines whether a clause is satisfiable given a certain model.

    my $model
        = { pink => 1, purple => 0, green => 0, yellow => 1, red => 0 };
    my $a=$solver->satisfiable( [ 'purple', '-pink' ], $model );
    #$a = 0

## update()

Copies the model, then sets \`choice\` = \`value\` in the model, and returns it.

    my $model
        = { pink => 1, red => 0, purple => 0, green => 0, yellow => 1 };
    my $new_model = $solver->update( $model, 'foobar', 1 );
    # now $new_model->{foobar} is 1

# 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>