-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | High-level Haskell bindings for the MiniSat SAT solver.
--   
--   This package provides high-level Haskell bindings for the well-known
--   MiniSat satisfiability solver. It solves the boolean satisfiability
--   problem, i.e., the input is a boolean formula, and the output is a
--   list of all satisfying assignments. MiniSat is a fully automated,
--   well-optimized general-purpose SAT solver written by Niklas Een and
--   Niklas Sorensson, and further modified by Takahisa Toda. Unlike other
--   similar Haskell packages, we provide a convenient high-level interface
--   to the SAT solver, hiding the complexity of the underlying C
--   implementation. It can be easily integrated into other programs as an
--   efficient turn-key solution to many search problems. To illustrate the
--   use of the library, two example programs are included in the
--   "examples" directory; one program solves Sudoku puzzles, and the other
--   solves a 3-dimensional block packing problem. These programs can be
--   built manually, or by invoking Cabal with the '--enable-benchmarks'
--   option.
@package minisat-solver
@version 0.1


-- | This module provides high-level Haskell bindings for the well-known
--   MiniSat satisfiability solver. It solves the boolean satisfiability
--   problem, i.e., the input is a boolean formula, and the output is a
--   list of all satisfying assignments. MiniSat is a fully automated,
--   well-optimized general-purpose SAT solver written by Niklas Een and
--   Niklas Sorensson, and further modified by Takahisa Toda.
--   
--   Unlike other similar Haskell packages, the purpose of this library is
--   not to provide access to low-level C functions, to give the user
--   fine-grained interactive control over the SAT solver, or to provide
--   building blocks for developing new SAT solvers. Rather, we package the
--   SAT solver as a general-purpose tool that can easily be integrated
--   into other programs as a turn-key solution to many search problems.
--   
--   It is well-known that the boolean satisfiability problem is
--   NP-complete, and therefore, no SAT solver can be efficient for all
--   inputs. However, there are many search problems that can be naturally
--   expressed as satisfiability problems and are nevertheless tractable.
--   Writing custom code to traverse the search space is tedious and rarely
--   efficient, especially in cases where the size of the search space is
--   sensitive to the order of traversal. This is where using a
--   general-purpose SAT solver can often be a time saver.
--   
--   We provide a convenient high-level interface to the SAT solver, hiding
--   the complexity of the underlying C implementation. The main API
--   function is <a>solve_all</a>, which inputs a boolean formula, and
--   outputs a list of all satisfying assignments (which are modelled as
--   maps from variables to truth values). The list is generated lazily, so
--   that the underlying low-level C code only does as much work as
--   necessary.
--   
--   Two example programs illustrating the use of this library can be found
--   in the "examples" directory of the Cabal package.
module SAT.MiniSat

-- | The type of boolean formulas. It is parametric over a set of variables
--   <i>v</i>. We provide the usual boolean operators, including
--   implications and exclusive or. For convenience, we also provide the
--   list quantifiers <a>All</a>, <a>Some</a>, <a>None</a>,
--   <a>ExactlyOne</a>, and <a>AtMostOne</a>, as well as a general
--   <a>Let</a> operator that can be used to reduce the size of repetitive
--   formulas.
data Formula v

-- | A variable.
Var :: v -> Formula v

-- | The formula <i>true</i>.
Yes :: Formula v

-- | The formula <i>false</i>.
No :: Formula v

-- | Negation.
Not :: (Formula v) -> Formula v

-- | Conjunction.
(:&&:) :: Formula v -> Formula v -> Formula v

-- | Disjunction.
(:||:) :: Formula v -> Formula v -> Formula v

-- | Exclusive or.
(:++:) :: Formula v -> Formula v -> Formula v

-- | Implication.
(:->:) :: Formula v -> Formula v -> Formula v

-- | If and only if.
(:<->:) :: Formula v -> Formula v -> Formula v

-- | All are true.
All :: [Formula v] -> Formula v

-- | At least one is true.
Some :: [Formula v] -> Formula v

-- | None are true.
None :: [Formula v] -> Formula v

-- | Exactly one is true.
ExactlyOne :: [Formula v] -> Formula v

-- | At most one is true.
AtMostOne :: [Formula v] -> Formula v

-- | <a>Let</a> <i>a</i> <i>f</i> is the formula "let <i>x</i>=<i>a</i> in
--   <i>fx</i>", which permits the subexpression <i>a</i> to be re-used. It
--   is logically equivalent to <i>fa</i>, but typically smaller.
Let :: (Formula v) -> (Formula v -> Formula v) -> Formula v

-- | For internal use only.
Bound :: Integer -> Formula v

-- | Check whether a boolean formula is satisfiable.
satisfiable :: (Ord v) => Formula v -> Bool

-- | Return a satisfying assignment for the boolean formula, if any.
solve :: (Ord v) => Formula v -> Maybe (Map v Bool)

-- | Lazily enumerate all satisfying assignments for the boolean formula.
solve_all :: (Ord v) => Formula v -> [Map v Bool]
