Portability  portable 

Stability  provisional 
Maintainer  Richard Senington <sc06r2s@leeds.ac.uk> 
A library for the representation and manipulation of satisfiability problems. Currently this is expected to only be 3SAT however I do not think the code is particularly limited to 3SAT. 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.
 data SATProblem = SATProblem {
 numClauses :: Int
 numSATEDClauses :: Int
 numVariables :: Int
 variableLookUp :: Int > ([Int], [Int])
 clauseLookUp :: Int > ([Int], [Int])
 variablePosition :: Map Int Bool
 clausePosition :: Map Int Int
 numUnSATEDClauses :: SATProblem > Int
 getTrueFalseCount :: SATProblem > (Int, Int)
 summariseSAT :: SATProblem > String
 makeRandomSATProblem :: RandomGen g => g > Int > Int > SATProblem
 flipVariable :: Int > SATProblem > (SATProblem, Int)
 satproblem :: Int > Int > (Int > ([Int], [Int])) > (Int > ([Int], [Int])) > Map Int Bool > SATProblem
 setAllVars :: Bool > SATProblem > SATProblem
 randomiseVariables :: RandomGen g => g > SATProblem > SATProblem
Documentation
data SATProblem Source
SATProblem  

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 3SAT 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 metaheuristic.