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: July 2021

Summary of exported operations:

z3Dimacs :: SolverConfig  Deterministic 
The configuration of the Z3 solver for DIMACS.
lingeling :: SolverConfig  Deterministic 
The configuration of the lingeling solver.
solveWithDimacs :: SolverConfig -> Boolean -> IO [(Int,Bool)]  Deterministic 
Checks the satisfiability of a Boolean formula with a SAT solver supporting DIMACS format.
boolVars2AssocList :: [Boolean] -> [(Int,Bool)]  Deterministic 
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  Deterministic 

The configuration of the Z3 solver for DIMACS.

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

lingeling :: SolverConfig  Deterministic 

The configuration of the lingeling solver.

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

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

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)]  Deterministic 

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