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 |
|