Browsing LERO - Project partner authors by Author "Belov, Anton"

Now showing items 1-4 of 4

MUSer2: an efficient MUS extractor, system description

Belov, Anton; Marques-Silva, Joao (IOS Press, 2012)

Algorithms for extraction of Minimally Unsatisfiable Subformulas (MUSes) of CNF formulas find a wide range of practical applications, including product configuration, knowledge-based validation, hardware and software ...
On computing minimal equivalent subformulas

Belov, Anton; Janota, Mikolas; Lynce, Inês; Marques-Silva, Joao (Springer, 2012)

A propositional formula in Conjunctive Normal Form (CNF) may contain redundant clauses | clauses whose removal from the for- mula does not a ect the set of its models. Identi cation of redundant clauses is important ...
On efficient computation of variable MUSes

Belov, Anton; Ivrii, Alexander; Matsliah, Arie; Marques-Silva, Joao (Springer-Verlag, 2012)

In this paper we address the following problem: given an unsatisfiable CNF formula F, find a minimal subset of variables of F that constitutes the set of variables in some unsatisfiable core of F. This problem, known as ...
Towards efficient MUS extraction

Belov, Anton; Lynce, Inês; Marques-Silva, Joao (IOS Press, 2012)

Minimally Unsatisfiable Subformulas (MUS) find a wide range of practical applications, including product configuration, knowledge-based validation, and hardware and software design and verification. MUSes also find ...

DSpace Repository