Búsqueda avanzada

Resultados de búsqueda para Resolution

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

Invariant-Free Clausal Temporal Resolution

We provide an extended abstract of the paper with the same title and authors that is going to appear in Journal of Automated Reasoning (Online from December 2th, 2011).

Autores: J. Gaintzarain / M. Hermo / P. Lucio / M. Navarro / F. Orejas / 
Palabras Clave: Clausal Normal Form - Invariant-free - Resolution - Temporal Logic

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