# koengit/satplus

No description, website, or topics provided.
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.

# SAT+

This is a Haskell library for constraint programming using a SAT-solver, in particular MiniSAT.

The names and types of these functions may change at any moment!

## Basic MiniSAT

The basic MiniSAT functions are:

```newSolver  :: IO Solver
newLit     :: Solver -> IO Lit
addClause  :: Solver -> [Lit] -> IO ()
solve      :: Solver -> [Lit] -> IO Bool
modelValue :: Solver -> Lit -> IO Bool
conflict   :: Solver -> IO [Lit]

valueMaybe      :: Solver -> Lit -> IO (Maybe Bool)
modelValueMaybe :: Solver -> Lit -> IO (Maybe Bool)```

## Boolean functions

This library also supports boolean operators:

`andl, orl, xorl :: Solver -> [Lit] -> IO Lit`

And binary operators:

```implies :: Solver -> Lit -> Lit -> IO Lit
equiv   :: Solver -> Lit -> Lit -> IO Lit```

## Values

We also have implemented a convenient type that links Haskell values with the SAT-solver:

```type Val a

newVal :: Ord a => Solver -> [a] -> IO (Val a)
val    ::          a -> Val a
(.=)   :: Ord a => Val a -> a -> Lit
domain ::          Val a -> [a]```

We also provide:

`modelValue :: Solver -> Val a -> IO a`

## Equality

We often want to add constraints that say that two things are equal, or not equal, to each other.

```class Equal a where
equal    :: Solver -> a -> a -> IO ()
notEqual :: Solver -> a -> a -> IO ()
...```

Instances of this class are:

```instance Equal ()
instance Equal Lit
instance (Equal a, Equal b) => Equal (a,b)
instance (Equal a, Equal b) => Equal (Either a b)
instance Equal a => Equal [a]
instance Equal a => Equal (Maybe a)
instance Ord a => Equal (Val a)
instance Equal Unary
instance Equal Binary```

## Order

We often want to add constraints that say that one thing is smaller than another.

```class Order a where
lessThan         :: Solver -> a -> a -> IO ()
lessThanEqual    :: Solver -> a -> a -> IO ()
greaterThan      :: Solver -> a -> a -> IO ()
greaterThanEqual :: Solver -> a -> a -> IO ()
...```

Instances of this class are:

```instance Order ()
instance Order Lit
instance (Order a, Order b) => Equal (a,b)
instance (Order a, Order b) => Equal (Either a b)
instance Order a => Order [a]
instance Order a => Order (Maybe a)
instance Ord a => Order (Val a)
instance Order Unary
instance Order Binary```

## Unary numbers

We have support for unary numbers (represented as sorted lists of Lits). These are handy when you want to count number of literals in a set being true, for example.

```type Unary

zero   :: Unary
digit  :: Lit -> Unary
number :: Int -> Unary

count    :: Solver ->        [Lit] -> IO Unary
countMax :: Solver -> Int -> [Lit] -> IO Unary

add     :: Solver -> Unary -> Unary -> IO Unary
addList :: Solver -> [Unary] -> IO Unary

(.<=), (.<), (.>=), (.>) :: Unary -> Int -> Lit```

We also provide:

`modelValue :: Solver -> Unary -> IO Int`

## Binary numbers

We have support for binary numbers (represented as lists of Lits). These are handy when you want to represent numbers that are large.

```type Binary

zero   :: Binary
digit  :: Lit -> Binary
number :: Integer -> Binary

count    :: Solver ->        [Lit] -> IO Binary
countMax :: Solver -> Int -> [Lit] -> IO Binary

add     :: Solver -> Binary -> Binary -> IO Binary
addList :: Solver -> [Binary] -> IO Binary```

We also provide:

`modelValue :: Solver -> Binary -> IO Integer`

## Terms

We also support linear arithmetic terms over a base type of variables (for example Lit, Unary, or Binary).

(not done yet)

## Minimization / Maximization

We also support finding solutions that are minimized or maximized w.r.t. a particular argument.

```solveMinimize :: Order a => Solver -> [Lit] -> Unary -> IO Bool
solveMaximize :: Order a => Solver -> [Lit] -> Unary -> IO Bool```

TODO: add optimization over binary numbers.