PAKCS
Exported names: Imported modules:

Module Dimacs.Solver

This module defines an operation to solve a Boolean formula with some SAT solver supporting the DIMACS format. It also defines configuration for various solvers.

Author: Michael Hanus

Version: September 2017

Summary of exported operations:

z3Dimacs :: SolverConfig   
The configuration of the Z3 solver for DIMACS.
lingeling :: SolverConfig   
The configuration of the lingeling solver.
solveWithDimacs :: SolverConfig -> Boolean -> IO [(Int,Bool)]   
Checks the satisfiability of a Boolean formula with a SAT solver supporting DIMACS format.
boolVars2AssocList :: [Boolean] -> [(Int,Bool)]   
Translates a list of Boolean variables into a list associating the variable indices to Boolean values.

Exported datatypes:

SolverConfig

Type of solvers configuration with fields for the name of the executable and command line flags.

Constructors:

  • Config :: String -> [String] -> SolverConfig

    Fields:

    • executable :: String
    • flags :: [String]

Exported operations:

z3Dimacs :: SolverConfig   

The configuration of the Z3 solver for DIMACS.

Further infos:
  • solution complete, i.e., able to compute all solutions

lingeling :: SolverConfig   

The configuration of the lingeling solver.

Further infos:
  • solution complete, i.e., able to compute all solutions

solveWithDimacs :: SolverConfig -> Boolean -> IO [(Int,Bool)]   

Checks the satisfiability of a Boolean formula with a SAT solver supporting DIMACS format. A list associating the variable indices to Boolean values so that the formula is satisfied is returned. If the formula is unsatisfiable, the returned list is empty.

boolVars2AssocList :: [Boolean] -> [(Int,Bool)]   

Translates a list of Boolean variables into a list associating the variable indices to Boolean values.