Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
64 | Éric Grégoire, Bertrand Mazure, Cédric Piette |
MUST: Provide a Finer-Grained Explanation of Unsatisfiability.  |
CP  |
2007 |
DBLP DOI BibTeX RDF |
unsatisfiability, MUC, MUS, MUST, CSP, explanation, constraint networks |
53 | Ohad Shacham, Karen Yorav |
On-The-Fly Resolve Trace Minimization.  |
DAC  |
2007 |
DBLP DOI BibTeX RDF |
|
49 | João Marques-Silva 0001, Vasco M. Manquinho |
Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms.  |
SAT  |
2008 |
DBLP DOI BibTeX RDF |
|
49 | Loganathan Lingappan, Niraj K. Jha |
Efficient Design for Testability Solution Based on Unsatisfiability for Register-Transfer Level Circuits.  |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.  |
2007 |
DBLP DOI BibTeX RDF |
|
49 | Zhenyu Chen 0001, Decheng Ding |
Variable Minimal Unsatisfiability.  |
TAMC  |
2006 |
DBLP DOI BibTeX RDF |
|
49 | Jinbo Huang |
MUP: a minimal unsatisfiability prover.  |
ASP-DAC  |
2005 |
DBLP DOI BibTeX RDF |
|
49 | Albert Atserias |
On sufficient conditions for unsatisfiability of random formulas.  |
J. ACM  |
2004 |
DBLP DOI BibTeX RDF |
Random CNF formulas, propositional resolution, satisfiability, datalog, phase transitions, pebble games |
49 | Evguenii I. Goldberg, Yakov Novikov |
Verification of Proofs of Unsatisfiability for CNF Formulas.  |
DATE  |
2003 |
DBLP DOI BibTeX RDF |
|
49 | Alexis C. Kaporis, Lefteris M. Kirousis, Yannis C. Stamatiou, Malvina Vamvakari, Michele Zito 0001 |
Coupon Collectors, q-Binomial Coefficients and the Unsatisfiability Threshold.  |
ICTCS  |
2001 |
DBLP DOI BibTeX RDF |
|
39 | Vasco M. Manquinho, João Marques-Silva 0001, Jordi Planes |
Algorithms for Weighted Boolean Optimization.  |
SAT  |
2009 |
DBLP DOI BibTeX RDF |
|
39 | Sudeshna Dasgupta, Vijay Chandru |
Minimal Unsatisfiable Sets: Classification and Bounds.  |
ASIAN  |
2004 |
DBLP DOI BibTeX RDF |
Minimal Unsatisfiable Sets, satisfiability, propositional logic, Boolean formulas |
36 | Koen Claessen, Ann Lillieström |
Automated Inference of Finite Unsatisfiability.  |
CADE  |
2009 |
DBLP DOI BibTeX RDF |
|
36 | Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell |
Efficient Generation of Unsatisfiability Proofs and Cores in SAT.  |
LPAR  |
2008 |
DBLP DOI BibTeX RDF |
|
36 | Allen Van Gelder |
Verifying Propositional Unsatisfiability: Pitfalls to Avoid.  |
SAT  |
2007 |
DBLP DOI BibTeX RDF |
|
36 | Steven D. Prestwich, Inês Lynce |
Local Search for Unsatisfiability.  |
SAT  |
2006 |
DBLP DOI BibTeX RDF |
|
36 | Mustafa Jarrar, Stijn Heymans |
Unsatisfiability Reasoning in ORM Conceptual Schemes.  |
EDBT Workshops  |
2006 |
DBLP DOI BibTeX RDF |
|
36 | Loganathan Lingappan, Niraj K. Jha |
Unsatisfiability Based Efficient Design for Testability Solution for Register-Transfer Level Circuits.  |
VTS  |
2005 |
DBLP DOI BibTeX RDF |
|
36 | Ashish Tiwari 0001 |
An Algebraic Approach for the Unsatisfiability of Nonlinear Constraints.  |
CSL  |
2005 |
DBLP DOI BibTeX RDF |
|
36 | Amin Coja-Oghlan, Andreas Goerdt, André Lanka, Frank Schädlich |
Certifying Unsatisfiability of Random 2k-SAT Formulas Using Approximation Techniques.  |
FCT  |
2003 |
DBLP DOI BibTeX RDF |
|
36 | Piotr Berman, Marek Karpinski |
Approximating minimum unsatisfiability of linear equations.  |
SODA  |
2002 |
DBLP BibTeX RDF |
|
28 | Bing Li, Chao Wang 0001, Fabio Somenzi |
Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure.  |
Int. J. Softw. Tools Technol. Transf.  |
2005 |
DBLP DOI BibTeX RDF |
Unsatisfiability proof, Bounded model checking, Satisfiability problem, Abstraction refinement |
28 | Hans Kleine Büning |
An Upper Bound for Minimal Resolution Refutations.  |
CSL  |
1998 |
DBLP DOI BibTeX RDF |
propositional formulas, length of proofs, minimal unsatisfiability, resolution |
28 | Vasek Chvátal, Bruce A. Reed |
Mick Gets Some (the Odds Are on His Side)  |
FOCS  |
1992 |
DBLP DOI BibTeX RDF |
unsatisfiability, truth assignment, randomly generated boolean formula, probability, time complexity, satisfiability, conjunctive normal form, linear-time algorithm |
28 | Peter B. Andrews |
Refutations by Matings.  |
IEEE Trans. Computers  |
1976 |
DBLP DOI BibTeX RDF |
clause-occurrence, mating, unsatisfiability, first-order logic, resolution, merge, cycle, Automatic theorem proving, refutation |
26 | K. Subramani 0001 |
Optimal Length Resolution Refutations of Difference Constraint Systems.  |
J. Autom. Reason.  |
2009 |
DBLP DOI BibTeX RDF |
Difference constraint systems, Resolution refutation, Optimal length, Minimum unsatisfiable subset, Fourier-Motzkin elimination |
26 | Lukas Kroc, Ashish Sabharwal, Bart Selman |
Relaxed DPLL Search for MaxSAT.  |
SAT  |
2009 |
DBLP DOI BibTeX RDF |
|
26 | Engin Uzuncaova, Sarfraz Khurshid |
Constraint Prioritization for Efficient Analysis of Declarative Models.  |
FM  |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Nathan Segerlind |
On the Relative Efficiency of Resolution-Like Proofs and Ordered Binary Decision Diagram Proofs.  |
CCC  |
2008 |
DBLP DOI BibTeX RDF |
lower bounds, resolution, ordered binary decision diagrams, propositional proof complexity |
26 | Joanna Golinska-Pilarek, Ewa Orlowska |
Tableaux and Dual Tableaux: Transformation of Proofs.  |
Stud Logica  |
2007 |
DBLP DOI BibTeX RDF |
first-order logic with identity, tableaux systems, Rasiowa-Sikorski proof system |
26 | Jun Liu 0001, Luis Martínez-López 0001, Yang Xu 0001, Zhirui Lu |
Automated Reasoning Algorithm for Linguistic Valued Lukasiewicz Propositional Logic.  |
ISMVL  |
2007 |
DBLP DOI BibTeX RDF |
|
26 | Jianmin Zhang, ShengYu Shen, Sikun Li |
A Heuristic Local Search Algorithm for Unsatisfiable Cores Extraction.  |
ICCSA (3)  |
2007 |
DBLP DOI BibTeX RDF |
Unsatisfiable core, Unit clause propagation, Binary clause resolution, Equality reduction, Local search |
26 | Engin Uzuncaova, Sarfraz Khurshid |
Kato: A Program Slicing Tool for Declarative Specifications.  |
ICSE  |
2007 |
DBLP DOI BibTeX RDF |
|
26 | Dominique D'Almeida, Jean-François Condotta, Christophe Lecoutre, Lakhdar Sais |
Relaxation of Qualitative Constraint Networks.  |
SARA  |
2007 |
DBLP DOI BibTeX RDF |
|
26 | Miguel F. Anjos |
An explicit semidefinite characterization of satisfiability for Tseitin instances on toroidal grid graphs.  |
Ann. Math. Artif. Intell.  |
2006 |
DBLP DOI BibTeX RDF |
Mathematics Subject Classifications (2000) 90C22, 03B05, 90C09, 90C90, 68T15 |
26 | Engin Uzuncaova, Sarfraz Khurshid |
Program slicing for declarative models.  |
ACM SIGSOFT Softw. Eng. Notes  |
2006 |
DBLP DOI BibTeX RDF |
|
26 | Allen Van Gelder |
Independently Checkable Proofs from Decision Procedures: Issues and Progress.  |
LPAR  |
2005 |
DBLP DOI BibTeX RDF |
|
26 | Albert Atserias |
Definability on a Random 3-CNF Formula.  |
LICS  |
2005 |
DBLP DOI BibTeX RDF |
|
26 | Babita Sharma, Paritosh K. Pandya, Supratik Chakraborty |
Bounded Validity Checking of Interval Duration Logic.  |
TACAS  |
2005 |
DBLP DOI BibTeX RDF |
|
26 | Kenneth L. McMillan, Nina Amla |
Automatic Abstraction without Counterexamples.  |
TACAS  |
2003 |
DBLP DOI BibTeX RDF |
|
26 | Dimitris Achlioptas, Paul Beame, Michael S. O. Molloy |
A sharp threshold in proof complexity.  |
STOC  |
2001 |
DBLP DOI BibTeX RDF |
|
26 | Luís Baptista, João Marques-Silva 0001 |
Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability.  |
CP  |
2000 |
DBLP DOI BibTeX RDF |
|
26 | Oliver Kullmann |
An Application of Matroid Theory to the SAT Problem.  |
CCC  |
2000 |
DBLP DOI BibTeX RDF |
|
23 | Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike, John Backes |
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories.  |
CoRR  |
2024 |
DBLP DOI BibTeX RDF |
|
23 | Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, Marc Vinyals |
Proving Unsatisfiability with Hitting Formulas.  |
ITCS  |
2024 |
DBLP DOI BibTeX RDF |
|
23 | Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike, John Backes |
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories.  |
TACAS (1)  |
2024 |
DBLP DOI BibTeX RDF |
|
23 | Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, Marc Vinyals |
Proving Unsatisfiability with Hitting Formulas.  |
Electron. Colloquium Comput. Complex.  |
2023 |
DBLP BibTeX RDF |
|
23 | Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, Marc Vinyals |
Proving Unsatisfiability with Hitting Formulas.  |
CoRR  |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen |
Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers.  |
TACAS (1)  |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Denis Firsov, Sven Laur, Ekaterina Zhuchko |
Unsatisfiability of Comparison-Based Non-malleability for Commitments.  |
ICTAC  |
2022 |
DBLP DOI BibTeX RDF |
|
23 | Nobutaka Suzuki, Takuya Okada, Yeondae Kwon |
On CSS Unsatisfiability Problem in the Presense of DTDs.  |
IEICE Trans. Inf. Syst.  |
2021 |
DBLP DOI BibTeX RDF |
|
23 | Marijn J. H. Heule |
Proofs of Unsatisfiability.  |
Handbook of Satisfiability  |
2021 |
DBLP DOI BibTeX RDF |
|
23 | Hans Kleine Büning, Oliver Kullmann |
Minimal Unsatisfiability and Autarkies.  |
Handbook of Satisfiability  |
2021 |
DBLP DOI BibTeX RDF |
|
23 | Abderrahim Ait Wakrime, Mouna Rekik 0001, Saïd Jabbour |
Cloud service composition using minimal unsatisfiability and genetic algorithm.  |
Concurr. Comput. Pract. Exp.  |
2020 |
DBLP DOI BibTeX RDF |
|
23 | Hans Kleine Büning, Piotr Wojciechowski 0002, K. Subramani 0001 |
NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability.  |
Math. Struct. Comput. Sci.  |
2020 |
DBLP DOI BibTeX RDF |
|
23 | Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias S. Kotsireas, Vijay Ganesh |
Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem.  |
CoRR  |
2020 |
DBLP BibTeX RDF |
|
23 | Daya Ram Gaur, Muhammad Khan |
Testing Unsatisfiability of Constraint Satisfaction Problems via Tensor Products.  |
CoRR  |
2020 |
DBLP BibTeX RDF |
|
23 | Daya Ram Gaur, Muhammad Khan |
Testing Unsatisfiability of Constraint Satisfaction Problems via Tensor Products.  |
ISAIM  |
2020 |
DBLP BibTeX RDF |
|
23 | Jingchao Chen |
Fast Verifying Proofs of Propositional Unsatisfiability via Window Shifting.  |
ISAIM  |
2020 |
DBLP BibTeX RDF |
|
23 | Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias S. Kotsireas, Vijay Ganesh |
Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem.  |
IJCAI  |
2020 |
DBLP DOI BibTeX RDF |
|
23 | Ziliang Chen, Zhanfu Yang |
Graph Neural Reasoning May Fail in Certifying Boolean Unsatisfiability.  |
CoRR  |
2019 |
DBLP BibTeX RDF |
|
23 | Norbert Manthey, Tobias Philipp |
Checking Unsatisfiability Proofs in Parallel.  |
POS@SAT  |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Hoda Abbasizanjani, Oliver Kullmann |
Minimal Unsatisfiability and Minimal Strongly Connected Digraphs.  |
SAT  |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Rohan Fossé, Laurent Simon |
On the Non-degeneracy of Unsatisfiability Proof Graphs Produced by SAT Solvers.  |
CP  |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Miguel F. Anjos, Manuel V. C. Vieira |
On semidefinite least squares and minimal unsatisfiability.  |
Discret. Appl. Math.  |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Tobias Philipp, Adrián Rebola-Pardo |
Towards a Semantics of Unsatisfiability Proofs with Inprocessing.  |
LPAR  |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Oliver Kullmann |
Minimal unsatisfiability and deficiency: recent developments.  |
CoRR  |
2016 |
DBLP BibTeX RDF |
|
23 | Jingchao Chen |
Fast Verifying Proofs of Propositional Unsatisfiability via Window Shifting.  |
CoRR  |
2016 |
DBLP BibTeX RDF |
|
23 | Takuro Kutsuna, Yoshinao Ishii |
Analyzing Unsatisfiability in Bounded Model Checking Using Max-SMT and Dual Slicing.  |
FMICS-AVoCS  |
2016 |
DBLP DOI BibTeX RDF |
|
23 | Tobias Philipp |
Unsatisfiability Proofs for Parallel SAT Solver Portfolios with Clause Sharing and Inprocessing.  |
GCAI  |
2016 |
DBLP DOI BibTeX RDF |
|
23 | Oliver Kullmann, Xishun Zhao |
Parameters for minimal unsatisfiability: Smarandache primitive numbers and full clauses.  |
CoRR  |
2015 |
DBLP BibTeX RDF |
|
23 | Till Mossakowski, Lutz Schröder |
On Inconsistency and Unsatisfiability.  |
Int. J. Softw. Informatics  |
2015 |
DBLP BibTeX RDF |
|
23 | Abderrahim Ait Wakrime, Saïd Jabbour |
Minimum Unsatisfiability based QoS Web Service Composition over the Cloud Computing.  |
ISDA  |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Yiyuan Wang, Dantong Ouyang, Liming Zhang 0005 |
Improved Algorithm of Unsatisfiability-based Maximum Satisfiability.  |
IWOST-1  |
2015 |
DBLP BibTeX RDF |
|
23 | Ruben Martins, Saurabh Joshi 0001, Vasco M. Manquinho, Inês Lynce |
On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving.  |
J. Satisf. Boolean Model. Comput.  |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
Bridging the gap between easy generation and efficient verification of unsatisfiability proofs.  |
Softw. Test. Verification Reliab.  |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Marijn Heule, Norbert Manthey, Tobias Philipp |
Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers.  |
POS@SAT  |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Lavinia María Picollo |
Yablo's Paradox in Second-Order Languages: Consistency and Unsatisfiability.  |
Stud Logica  |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Lu-lu Wu, Hai-Jun Zhou, Mikko Alava, Erik Aurell, Pekka Orponen |
Witness of unsatisfiability for a random 3-satisfiability formula  |
CoRR  |
2013 |
DBLP BibTeX RDF |
|
23 | Ricardo Menchaca-Mendez |
Unsatisfiability Bounds for Random Constraint Satisfaction Problems from an Energetic Interpolation Method.  |
|
2013 |
RDF |
|
23 | Matthias Baaz, Agata Ciabattoni, Christian G. Fermüller |
Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability  |
Log. Methods Comput. Sci.  |
2012 |
DBLP DOI BibTeX RDF |
|
23 | Dimitris Achlioptas, Ricardo Menchaca-Mendez |
Unsatisfiability Bounds for Random CSPs from an Energetic Interpolation Method.  |
ICALP (1)  |
2012 |
DBLP DOI BibTeX RDF |
|
23 | Benjamin Andres, Benjamin Kaufmann, Oliver Matheis, Torsten Schaub |
Unsatisfiability-based optimization in clasp.  |
ICLP (Technical Communications)  |
2012 |
DBLP DOI BibTeX RDF |
|
23 | Martin Fürer |
Efficient Arbitrary and Resolution Proofs of Unsatisfiability for Restricted Tree-Width.  |
LATIN  |
2012 |
DBLP DOI BibTeX RDF |
|
23 | Oliver Kullmann |
Constraint Satisfaction Problems in Clausal Form II: Minimal Unsatisfiability and Conflict Structure.  |
Fundam. Informaticae  |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Koen Claessen, Ann Lillieström |
Automated Inference of Finite Unsatisfiability.  |
J. Autom. Reason.  |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Jakob Nordström, Alexander A. Razborov |
On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution.  |
ICALP (1)  |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Federico Heras, João Marques-Silva 0001 |
Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms.  |
IJCAI  |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Roberto Javier Asín Achá, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell |
Practical algorithms for unsatisfiability proof and core generation in SAT solvers.  |
AI Commun.  |
2010 |
DBLP DOI BibTeX RDF |
|
23 | Vasco M. Manquinho, Ruben Martins, Inês Lynce |
Improving Unsatisfiability-Based Algorithms for Boolean Optimization.  |
SAT  |
2010 |
DBLP DOI BibTeX RDF |
|
23 | João Marques-Silva 0001 |
Minimal Unsatisfiability: Models, Algorithms and Applications (Invited Paper).  |
ISMVL  |
2010 |
DBLP DOI BibTeX RDF |
|
23 | Jakob Nordström, Alexander A. Razborov |
On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution.  |
Electron. Colloquium Comput. Complex.  |
2009 |
DBLP BibTeX RDF |
|
23 | Manuel Clavel, Marina Egea, Miguel Angel García de Dios |
Checking Unsatisfiability for OCL Constraints.  |
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.  |
2009 |
DBLP DOI BibTeX RDF |
|
23 | Jakob Nordström, Alexander A. Razborov |
On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution  |
CoRR  |
2009 |
DBLP BibTeX RDF |
|
23 | David Pereira, Inês Lynce, Steven D. Prestwich |
On Improving Local Search for Unsatisfiability  |
LSCS  |
2009 |
DBLP DOI BibTeX RDF |
|
23 | Hans Kleine Büning, Oliver Kullmann |
Minimal Unsatisfiability and Autarkies.  |
Handbook of Satisfiability  |
2009 |
DBLP DOI BibTeX RDF |
|
23 | Stefan Kupferschmid, Tino Teige, Bernd Becker 0001, Martin Fränzle |
Proofs of Unsatisfiability for mixed Boolean and Non-linear Arithmetic Constraint Formulae.  |
MBMV  |
2009 |
DBLP BibTeX RDF |
|
23 | Richard Ostrowski, Lionel Paris |
Detecting Boolean Functions for Proving Unsatisfiability.  |
ICTAI  |
2009 |
DBLP DOI BibTeX RDF |
|
23 | Michael Molloy 0001 |
When does the giant component bring unsatisfiability?  |
Comb.  |
2008 |
DBLP DOI BibTeX RDF |
|
23 | Knot Pipatsrisawat, Adnan Darwiche |
A New Clause Learning Scheme for Efficient Unsatisfiability Proofs.  |
AAAI  |
2008 |
DBLP BibTeX RDF |
|
23 | Allen Van Gelder |
Verifying RUP Proofs of Propositional Unsatisfiability.  |
ISAIM  |
2008 |
DBLP BibTeX RDF |
|