Navegación

Búsqueda

Búsqueda avanzada

Resultados de búsqueda para SAT solvers

Satisfiability Solvers based on Resolution and Cutting Planes Proof Systems

Satisfiability (SAT) is the canonical NP-Complete problem. Many other interesting and practical problems can be encoded into SAT. This is why it is important from a theoretical and practical point of view. Nowadays there are very good algorithms to solve SAT, the best from the point of view of industrial instances can be shown equivalent to the proof system Resolution. We will present the algorithm, and the equivalence to Resolution. Other proof systems are more powerful than Resolution, and still might be amenable to finding refutation algorithms, like Cutting Planes. We will talk about posible ways to automatize Cutting Planes. Also we will present the dual-rail encoding of formulas, to be then refuted using MaxSAT algorithms, as another methodology for SAT more powerful than Resolution.

Autores: Maria Luisa Bonet / 
Palabras Clave: Cutting Planes - Proof Complexity - Resolution - SAT solvers - Satisfiability

Modelling and Specifying Software Systems with Alloy (tutorial)

Alloy is both a modelling and specifying language of software systems, and a tool to automatically check the consistency of descriptions. Alloy uses sets and set relations to describe the high-level structure of systems, and a first-order relational logic to enrich models with more specific properties. A similar methodology is followed by software engineers when using OCL to complete the UML descriptions with more detailed features that improve the specifications. Alloy is able to construct and analyze the consistency of static specifications of complex systems, producing snapshots of possible model instances. In addition,Alloy can also describe dynamic specifications that show how the system may evolve over time when executing transitions. In this tutorial, we present the main features of the language and illustrate them by means of an example consisting in the specification and modelling of Software-Defined Networks. The example is sufficiently complex to permit the use of the most significant Alloy constructors.

Autores: María-Del-Mar Gallardo / Laura Panizo / 
Palabras Clave: Modelling language Alloy - SAT solvers - Software defined networks

No encuentra los resultados que busca? Prueba nuestra Búsqueda avanzada