toysolver-0.6.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc

Copyright(c) Masahiro Sakai 2016
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

ToySolver.Combinatorial.HittingSet.MARCO

Contents

Description

Synopsis

Problem definition

Main functionality

run :: forall prob. IsProblem prob IO => prob -> Options IO -> IO (Set IntSet, Set IntSet) Source #

Given a problem and an option, it computes maximal interesting sets and minimal uninteresting sets.

Applications: monotone boolean functions

generateCNFAndDNF Source #

Arguments

:: IntSet

Set of variables V

-> (IntSet -> Bool)

A monotone boolean function f from {0,1}^|V| ≅ P(V) to Bool

-> Set IntSet

Subset C' of prime implicates C of f

-> Set IntSet

Subset D' of prime implicants D of f

-> (Set IntSet, Set IntSet) 

Compute the irredundant CNF representation and DNF representation.

Let f be a monotone boolean function over set of variables S. This function returns C and D where ∧_{I∈C} ∨_{i∈I} x_i and ∨_{I∈D} ∧_{i∈I} x_i are the irredundant CNF representation f and DNF representation of f respectively.

Applicaitons: minimal hitting sets