combinatorial-problems-0.0.4: A number of data structures to represent and allow the manipulation of standard combinatorial problems, used as test problems in computer science.

Portabilityportable
Stabilityprovisional
MaintainerRichard Senington <sc06r2s@leeds.ac.uk>

CombinatorialOptimisation.SAT

Description

A library for the representation and manipulation of satisfiability problems. Currently this is expected to only be 3-SAT however I do not think the code is particularly limited to 3-SAT. The approach taken is that there is a complex data structure called SATProblem, which contains both the problem and the solution (settings of variables). In addition it contains a number additional fields that allow for making changes quickly, such as a table of clause positions. This is a Map from clause index to the number of variable terms that are currently set to true.

Currently the only function for quickly changing a problem is the flipping of a single variable. I think some other low level operations for finding clauses not currently evaluating to true and so on would be useful.

Synopsis

Documentation

numUnSATEDClauses :: SATProblem -> IntSource

The number of unsatisfied clauses in the problem, the inverse of numSATEDClauses

getTrueFalseCount :: SATProblem -> (Int, Int)Source

For the purposes of getting a general impression of the state of the system, it returns the number of variables in the True, and False positions.

summariseSAT :: SATProblem -> StringSource

Partial display function, for usage in show, displays some general statistics about the solution status.

makeRandomSATProblem :: RandomGen g => g -> Int -> Int -> SATProblemSource

I am not sure how often this will be used in practice, as randomly created problems often seem to be quite easy to solve. Requires a source of random numbers, the number of variables and the number of clauses to create, in that order. It is assumed that 3-SAT problems are the type wanted.

flipVariable :: Int -> SATProblem -> (SATProblem, Int)Source

The first low level operation. Takes a problem and changes the setting of the indexed variable from true to false. This is expected to be used in conjunction with other program logic to select which index to flip.

satproblem :: Int -> Int -> (Int -> ([Int], [Int])) -> (Int -> ([Int], [Int])) -> Map Int Bool -> SATProblemSource

Alternative constructor for the data structure. Takes only those elements that can not be derived and correctly initialises the other components, such as calculating how many clauses are currently evaluating to true. Requires the number of clauses, the number of variables, the lookup function for variables (variable index returning two lists, the first is the indexes of clauses in which this variable is present, the second list the indexes of clauses in which the inverse of this variable is present), the lookup table for clauses (clause index to lists of variable indexes) and the current settings of each variable.

setAllVars :: Bool -> SATProblem -> SATProblemSource

For rapid initialisation of problem instances. This fixes the setting of all variables to either true or false. The effect this has on the number of clauses that evaluate to true is unknown until it is carried out.

randomiseVariables :: RandomGen g => g -> SATProblem -> SATProblemSource

For rapid initialisation of problem instances for usage in stochastic algorithms. Specifically expected to be used for genetic algorithms and other forms of stochastic meta-heuristic.