Alexey Ignatiev's home page
Research software tools
(Boolean simplifier for non-clausal formulae)
Bica is a Python prototype implementation of the formula simplification approach proposed in [1]. Given a Boolean formula in an arbitrary form, it is able to compute a smallest size prime cover of the formula, i.e. to construct a smallest CNF/DNF representation comprising the formula's prime implicates/implicants, which is equivalent to the original formula. Being inspired by the well-known Quine-McCluskey procedure, this entirely SAT-based approach can deal with arbitrary Boolean formulae whereas the Quine-McCluskey procedure can minimize only DNF formulae. The word "bica" is Portuguese and means extremely strong and high-quality coffee (a synonym of espresso).

[1] A. Ignatiev, A. Previti, and J. Marques-Silva (2015) SAT-Based Formula Simplification. In: Proc. SAT 2015, pp. 287–298.
Author(s):  Alexey Ignatiev
Contributor(s):  Joao Marques-Silva, Alessandro Previti

(Formula Quintessence extractor)
This tool is a result of the work on smallest MUS (SMUS) extraction. It is based on MinUC, which is the previous best SMUS extractor originally published at SAT 2013, as well as efficient minimal hitting set dualization approach proposed in our CP 2015 paper. Given a CNF formula, forqes is able to compute one of its smallest MUSes if the formula is unsatisfiable, or one of its smallest MESes (SMESes, smallest minimal equivalent subformulae) if the formula is satisfiable.
Author(s):  Alexey Ignatiev
Contributor(s):  Joao Marques-Silva

(Hypotheses finder)
Hyper is a solver for the propositional abduction problem based on implicit hitting set enumeration.
Author(s):  Alexey Ignatiev, Joao Marques-Silva, Antonio Morgado

(Minimum Satisfying Assignment extractor)
Mint is a Python prototype implementation of the minimum satisfying assignment solver proposed in [2]. Given an SMT formula in the SMTLIB format (version 2), it computes a model of the formula that assigns the smallest possible number of variables of the formula leaving all the other variables unassigned. The underlying algorithm is based on implicit hitting set approach and the minimal hitting set duality between "minimal existential subsets" and "minimal falsifying subsets" of a formula. The minimal hitting set engine is implemented as an incremental core-guided MaxSAT solver.

[2] A. Ignatiev, A. Previti, and J. Marques-Silva (2016) On Finding Minimum Satisfying Assignments. In: Proc. CP 2016, pp. 287–297.
Author(s):  Alexey Ignatiev, Alessandro Previti
Contributor(s):  Joao Marques-Silva

(Minimum Unsatisfiable Core finder)
This tool is intended for solving the Smallest Minimal Unsatisfiable Subset (smallest MUS, SMUS) problem. Given an unsatisfiable CNF formula in DIMACS, it finds a smallest unsatisfiable subset of clauses using the CEGAR-based 2QBF approach.
Author(s):  Alexey Ignatiev, Mikoláš Janota
Contributor(s):  Joao Marques-Silva

(a Python script to create cactus and scatter plots based on matplotlib)
The mkplot script is designed to automate the process of creating cactus and scatter plots with the use of the matplotlib plotting library.
Author(s):  Alexey Ignatiev

(Core-guided MaxSAT solver)
MSCG is a general-purpose MaxSAT solver participated in the Ninth and Tenth Evaluations of Max-SAT Solvers. Although it is mainly focused on core-guided MaxSAT solving, MSCG also incorporates some other MaxSAT algorithms based on iterative calls to a SAT oracle.
Author(s):  Alexey Ignatiev, Joao Marques-Silva, Antonio Morgado
Contributor(s):  Carmine Dodaro, Inês Lynce, Vasco Manquinho

(Hybrid Package Upgradability solver)
Given a CUDF package universe file and a MISC2012-compatible user request (see the MANCOOSI project website), this tool finds either an exact or an approximate solution to the package dependency problem. The solver is built on top of recent MaxSAT algorithms and MCS-based MaxSAT approximation. In order to use approximation, one needs to make sure "mcsls2" is available from the PATH environment variable.
Author(s):  Alexey Ignatiev, Mikoláš Janota
Contributor(s):  Joao Marques-Silva

(a toolkit for SAT-based prototyping in Python)
A Python library providing a simple interface to a number of state-of-art Boolean satisfiability (SAT) solvers and a few types of cardinality encodings. The purpose of PySAT is to enable researchers working on SAT and its applications and generalizations to easily prototype with SAT oracles in Python while exploiting incrementally the power of the original low-level implementations of modern SAT solvers.
Author(s):  Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva

Apr 19, 2017 16:11:54 WET