Satisfiability via Smooth Pictures

DOI10.1007/978-3-319-40970-2_2zbMath1475.68137OpenAlexW2484413349MaRDI QIDQ2817998

Mateus de Oliveira Oliveira

Publication date: 5 September 2016

Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-40970-2_2

zbMATH Keywords

pigeonhole principlebounded Frege proof systemssmooth pictures

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Complexity of proofs (03F20) Computational aspects of satisfiability (68R07)

Uses Software

• MiniSat
• Chaff

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the power of clause-learning SAT solvers as resolution engines
• Exponential lower bounds for the pigeonhole principle
• Resolution proofs of generalized pigeonhole principles
• The intractability of resolution
• The membership and equivalence problems for picture languages
• Minimisation of acyclic deterministic automata in linear time
• A characterization of recognizable picture languages by tilings by finite sets
• Recognizable picture languages and domino tiling
• Picture languages: tiling systems versus tile rewriting grammars.
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Using string languages to describe picture languages
• The relative efficiency of propositional proof systems
• Lower bounds to the size of constant-depth propositional proofs
• An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
• Theory and Applications of Satisfiability Testing
• Resolution lower bounds for the weak pigeonhole principle

This page was built for publication: Satisfiability via Smooth Pictures