[![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. # 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. Will follow a package to help to define proper expressions soon. ## 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