toysolver-0.8.1: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2012-2014
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

ToySolver.SAT.MUS.Types

Description

In this module, we assume each soft constraint C_i is represented as a literal. If a constraint C_i is not a literal, we can represent it as a fresh variable v together with a hard constraint v ⇒ C_i.

References:

Synopsis

Documentation

type US = LitSet Source #

Unsatisfiable Subset of constraints (US).

A subset U ⊆ C is an US if U is unsatisfiable.

type MUS = LitSet Source #

Minimal Unsatisfiable Subset of constraints (MUS).

A subset U ⊆ C is an MUS if U is unsatisfiable and ∀C_i ∈ U, U\{C_i} is satisfiable [CAMUS].

type CS = LitSet Source #

Correction Subset of constraints (CS).

A subset M ⊆ C is a CS if C\M is satisfiable. A CS is the complement of a SS.

type MCS = LitSet Source #

Minimal Correction Subset of constraints (MCS).

A subset M ⊆ C is an MCS if C\M is satisfiable and ∀C_i ∈ M, C\(M\{C_i}) is unsatisfiable [CAMUS]. A MCS is the complement of an MSS and also known as a CoMSS.

type SS = LitSet Source #

Satisfiable Subset (SS).

A subset S ⊆ C is a SS if S is satisfiable. A SS is the complement of a CS.

type MSS = LitSet Source #

Maximal Satisfiable Subset (MSS).

A subset S ⊆ C is an MSS if S is satisfiable and ∀C_i ∈ U\S, S∪{C_i} is unsatisfiable [CAMUS]. A MSS is the complement of an MCS.