João Marques-Silva

Proceedings of the Principles and Practice of Constraint Programming, 2020

From Contrastive to Abductive Explanations and Back Again.

[BibT_eX]

[DOI]

Proceedings of the AIxIA 2020 - Advances in Artificial Intelligence, 2020

2019

RC2: an Efficient MaxSAT Solver.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2019

Formally Verifying the Solution to the Boolean Pythagorean Triples Problem.

[BibT_eX]

[DOI]

Luís Cruz-Filipe

Peter Schneider-Kamp

J. Autom. Reason., 2019

From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group).

[BibT_eX]

[DOI]

CoRR, 2019

On Validating, Repairing and Refining Heuristic ML Explanations.

[BibT_eX]

[DOI]

Nina Narodytska

CoRR, 2019

Assessing Heuristic Machine Learning Explanations with Model Counting.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

DRMaxSAT with MaxHS: First Contact.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

On Computing the Union of MUSes.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

On Relating Explanations and Adversarial Examples.

[BibT_eX]

[DOI]

Nina Narodytska

Proceedings of the Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, 2019

Efficient Symmetry Breaking for SAT-Based Minimum DFA Inference.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2019

Model-Based Diagnosis with Multiple Observations.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, 2019

Computing Shortest Resolution Proofs.

[BibT_eX]

[DOI]

Proceedings of the Progress in Artificial Intelligence, 2019

Abduction-Based Explanations for Machine Learning Models.

[BibT_eX]

[DOI]

Nina Narodytska

Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019

2018

Propositional SAT Solving.

[BibT_eX]

[DOI]

Sharad Malik

Proceedings of the Handbook of Model Checking., 2018

PySAT: A Python Toolkit for Prototyping with SAT Oracles.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

Learning Optimal Decision Trees with SAT.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

Computing with SAT Oracles: Past, Present and Future.

[BibT_eX]

[DOI]

Proceedings of the Sailing Routes in the World of Computation, 2018

A SAT-Based Approach to Learn Explainable Decision Sets.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

Premise Set Caching for Enumerating Minimal Correction Subsets.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 2018

MaxSAT Resolution With the Dual Rail Encoding.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 2018

2017

Exact and Hybrid Solutions for the Multi-Objective VM Reassignment Problem.

[BibT_eX]

[DOI]

Int. J. Artif. Intell. Tools, 2017

Horn Maximum Satisfiability: Reductions, Algorithms & Applications.

[BibT_eX]

[DOI]

CoRR, 2017

Model Based Diagnosis of Multiple Observations with Implicit Hitting Sets.

[BibT_eX]

[DOI]

CoRR, 2017

Minimal sets on propositional formulae. Problems and reductions.

[BibT_eX]

[DOI]

Artif. Intell., 2017

Efficient Certified Resolution Proof Checking.

[BibT_eX]

[DOI]

Luís Cruz-Filipe

Peter Schneider-Kamp

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Improving MCS Enumeration via Caching.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28, 2017

On Tackling the Limits of Resolution in SAT Solving.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28, 2017

Cardinality Encodings for Graph Optimization Problems.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

On Computing Generalized Backbones.

[BibT_eX]

[DOI]

Proceedings of the 29th IEEE International Conference on Tools with Artificial Intelligence, 2017

Lean Kernels in Description Logics.

[BibT_eX]

[DOI]

Proceedings of the Semantic Web - 14th International Conference, 2017

Horn Maximum Satisfiability: Reductions, Algorithms and Applications.

[BibT_eX]

[DOI]

Proceedings of the Progress in Artificial Intelligence, 2017

An Achilles' Heel of Term-Resolution.

[BibT_eX]

[DOI]

Proceedings of the Progress in Artificial Intelligence, 2017

Debugging EL+ Ontologies through Horn MUS Enumeration.

[BibT_eX]

[DOI]

Proceedings of the 30th International Workshop on Description Logics, 2017

On Minimal Corrections in ASP.

[BibT_eX]

[DOI]

Proceedings of the 24th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 2017 co-located with the 16th International Conference of the Italian Association for Artificial Intelligence (AI*IA 2017), 2017

2016

Fast, flexible MUS enumeration.

[BibT_eX]

[DOI]

Constraints An Int. J., 2016

Quantified maximum satisfiability.

[BibT_eX]

[DOI]

Constraints An Int. J., 2016

Reports of the 2016 AAAI Workshop Program.

[BibT_eX]

[DOI]

AI Mag., 2016

Maximal falsifiability.

[BibT_eX]

[DOI]

AI Commun., 2016

On the query complexity of selecting minimal sets for monotone predicates.

[BibT_eX]

[DOI]

Artif. Intell., 2016

Solving QBF with counterexample guided refinement.

[BibT_eX]

[DOI]

Artif. Intell., 2016

MCS Extraction with Sublinear Oracle Queries.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

BEACON: An Efficient SAT-Based Tool for Debugging <i>EL</i>^+ Ontologies.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

Efficient Reasoning for Inconsistent Horn Formulae.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence - 15th European Conference, 2016

Propositional Abduction with Implicit Hitting Sets.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands, 2016

On Finding Minimum Satisfying Assignments.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2016

Preface: The Beyond NP Workshop.

[BibT_eX]

[DOI]

Adnan Darwiche

Pierre Marquis

Proceedings of the Beyond NP, 2016

2015

Expansion-based QBF solving versus Q-resolution.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2015

Towards Efficient Axiom Pinpointing of EL+ Ontologies.

[BibT_eX]

[DOI]

M. Fareed Arif

CoRR, 2015

Algorithms for computing backbones of propositional formulae.

[BibT_eX]

[DOI]

AI Commun., 2015

MaxSAT-based encodings for Group MaxSAT.

[BibT_eX]

[DOI]

AI Commun., 2015

SAT-Based Horn Least Upper Bounds.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

Computing Maximal Autarkies with Few and Simple Oracle Queries.

[BibT_eX]

[DOI]

Oliver Kullmann

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

SAT-Based Formula Simplification.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing.

[BibT_eX]

[DOI]

M. Fareed Arif

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

Efficient Axiom Pinpointing with EL2MCS.

[BibT_eX]

[DOI]

M. Fareed Arif

Proceedings of the KI 2015: Advances in Artificial Intelligence, 2015

Prime Compilation of Non-Clausal Formulae.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

Literal-Based MCS Extraction.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

Efficient Model Based Diagnosis with Maximum Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

Solving QBF by Clause Selection.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

MILP for the Multi-objective VM Reassignment Problem.

[BibT_eX]

[DOI]

Proceedings of the 27th IEEE International Conference on Tools with Artificial Intelligence, 2015

Smallest MUS Extraction with Minimal Hitting Set Dualization.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2015

2014

MSCG: Robust Core-Guided MaxSAT Solving.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2014

On the Query Complexity of Selecting Few Minimal Sets.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2014

Computing Minimal Sets on Propositional Formulae I: Problems & Reductions.

[BibT_eX]

[DOI]

CoRR, 2014

Algorithms for computing minimal equivalent subformulas.

[BibT_eX]

[DOI]

Artif. Intell., 2014

On lazy and eager interactive reconfiguration.

[BibT_eX]

[DOI]

Goetz Botterweck

Proceedings of the Eighth International Workshop on Variability Modelling of Software-intensive Systems, 2014

Synthesizing Safe Bit-Precise Invariants.

[BibT_eX]

[DOI]

Arie Gurfinkel

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

On Computing Preferred MUSes and MCSes.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

On Reducing Maximum Independent Set to Minimum Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

MUS Extraction Using Clausal Proofs.

[BibT_eX]

[DOI]

Marijn Heule

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence - 14th European Conference, 2014

Efficient Relaxations of Over-constrained CSPs.

[BibT_eX]

[DOI]

Proceedings of the 26th IEEE International Conference on Tools with Artificial Intelligence, 2014

Towards efficient optimization in package management systems.

[BibT_eX]

[DOI]

Proceedings of the 36th International Conference on Software Engineering, 2014

Efficient Autarkies.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, 2014

Timeout-Sensitive Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, 2014

Progression in Maximum Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, 2014

A Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems.

[BibT_eX]

[DOI]

Proceedings of the Integration of AI and OR Techniques in Constraint Programming, 2014

Core-Guided MaxSAT with Soft Cardinality Constraints.

[BibT_eX]

[DOI]

Carmine Dodaro

Proceedings of the Principles and Practice of Constraint Programming, 2014

SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Tractability: Practical Approaches to Hard Problems, 2014

2013

A Two-Variable Model for SAT-Based ATPG.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2013

On Propositional QBF Expansions and Q-Resolution.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2013

SAT-based Preprocessing for MaxSAT (extended version).

[BibT_eX]

[DOI]

CoRR, 2013

Iterative and core-guided MaxSAT solving: A survey and assessment.

[BibT_eX]

[DOI]

Constraints An Int. J., 2013

Formula Preprocessing in MUS Extraction.

[BibT_eX]

[DOI]

Matti Järvisalo

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Quantified Maximum Satisfiability: - A Core-Guided Approach.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013

Parallel MUS Extraction.

[BibT_eX]

[DOI]

Norbert Manthey

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013

On QBF Proofs and Preprocessing.

[BibT_eX]

[DOI]

Radu Grigore

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Maximal Falsifiability - Definitions, Algorithms, and Applications.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

SAT-Based Preprocessing for MaxSAT.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

On Computing Minimal Correction Subsets.

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2013, 2013

Model-Guided Approaches for MaxSAT Solving.

[BibT_eX]

[DOI]

Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence, 2013

Core minimization in SAT-based abstraction.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation and Test in Europe, 2013

Solving QBF with Free Variables.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2013

Minimal Sets over Monotone Predicates in Boolean Formulae.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Partial MUS Enumeration.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, 2013

2012

SMT-Based Bounded Model Checking for Embedded ANSI-C Software.

[BibT_eX]

[DOI]

Lucas C. Cordeiro

IEEE Trans. Software Eng., 2012

Computing Minimally Unsatisfiable Subformulas: State of the Art and Future Directions.

[BibT_eX]

[DOI]

J. Multiple Valued Log. Soft Comput., 2012

PackUp: Tools for Package Upgradability Solving.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2012

TG-Pro: A SAT-based ATPG System.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2012

MUSer2: An Efficient MUS Extractor.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2012

Hybrid Incremental Algorithms for Boolean Satisfiability.

[BibT_eX]

[DOI]

Florian Letombe

Int. J. Artif. Intell. Tools, 2012

Generalizing Redundancy in Propositional Logic: Foundations and Hitting Sets Duality

[BibT_eX]

[DOI]

CoRR, 2012

Towards efficient MUS extraction.

[BibT_eX]

[DOI]

AI Commun., 2012

Knowledge Compilation with Empowerment.

[BibT_eX]

[DOI]

Lucas Bordeaux

Proceedings of the SOFSEM 2012: Theory and Practice of Computer Science, 2012

Improvements to Core-Guided Binary Search for MaxSAT.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

On Efficient Computation of Variable MUSes.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Lower Bounds and Upper Bounds for MaxSAT.

[BibT_eX]

[DOI]

Proceedings of the Learning and Intelligent Optimization - 6th International Conference, 2012

On Unit-Refutation Complete Formulae with Existentially Quantified Variables.

[BibT_eX]

[DOI]

Proceedings of the Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, 2012

Iterative SAT Solving for Minimum Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the IEEE 24th International Conference on Tools with Artificial Intelligence, 2012

MaxSAT-Based MCS Enumeration.

[BibT_eX]

[DOI]

Mark H. Liffiton

Proceedings of the Hardware and Software: Verification and Testing, 2012

New & improved models for SAT-based bi-decomposition.

[BibT_eX]

[DOI]

Proceedings of the Great Lakes Symposium on VLSI 2012, 2012

QBf-based boolean function bi-decomposition.

[BibT_eX]

[DOI]

Proceedings of the 2012 Design, Automation & Test in Europe Conference & Exhibition, 2012

On Computing Minimal Equivalent Subformulas.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2012

An Empirical Study of Encodings for Group MaxSAT.

[BibT_eX]

[DOI]

Proceedings of the Advances in Artificial Intelligence, 2012

2011

Restoring CSP Satisfiability with MaxSAT.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2011

Anatomy and Empirical Evaluation of Modern SAT Solvers.

[BibT_eX]

[DOI]

Bull. EATCS, 2011

Lazy Decomposition for Distributed Decision Procedures

[BibT_eX]

[DOI]

Youssef Hamadi

Christoph M. Wintersteiger

Proceedings of the Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, 2011

Haplotype inference with pseudo-Boolean optimization.

[BibT_eX]

[DOI]

Ann. Oper. Res., 2011

Boolean lexicographic optimization: algorithms & applications.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2011

Improvements to Satisfiability-Based Boolean Function Bi-Decomposition.

[BibT_eX]

[DOI]

Proceedings of the VLSI-SoC: Advanced Research for Systems on Chip, 2011

On Improving MUS Extraction Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Empirical Study of the Anatomy of Modern Sat Solvers.

[BibT_eX]

[DOI]

Hadi Katebi

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Abstraction-Based Algorithm for 2QBF.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Minimally Unsatisfiable Boolean Circuits.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

cmMUS: A Tool for Circumscription-Based MUS Membership Testing.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2011

Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms.

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2011, 2011

On Validating Boolean Optimizers.

[BibT_eX]

[DOI]

Proceedings of the IEEE 23rd International Conference on Tools with Artificial Intelligence, 2011

Accelerating MUS extraction with recursive model rotation.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

On Deciding MUS Membership with QBF.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming - CP 2011, 2011

Core-Guided Binary Search Algorithms for Maximum Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence, 2011

Haplotype Inference Using Propositional Satisfiability.

[BibT_eX]

[DOI]

Ana Graça

Proceedings of the Mathematical Approaches to Polymer Sequence Analysis and Related Problems, 2011

2010

Automated Design Debugging With Maximum Satisfiability.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2010

Haplotype Inference by Pure Parsimony: A Survey.

[BibT_eX]

[DOI]

J. Comput. Biol., 2010

Combinatorial Optimization Solutions for the Maximum Quartet Consistency Problem.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2010

Solving Linux Upgradeability Problems Using Boolean Optimization

[BibT_eX]

[DOI]

Proceedings of the Proceedings First International Workshop on Logics for Component Configuration, 2010

How to Complete an Interactive Configuration Process?

[BibT_eX]

[DOI]

Proceedings of the SOFSEM 2010: Theory and Practice of Computer Science, 2010

Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription.

[BibT_eX]

[DOI]

Radu Grigore

Proceedings of the Logics in Artificial Intelligence - 12th European Conference, 2010

Minimal Unsatisfiability: Models, Algorithms and Applications (Invited Paper).

[BibT_eX]

[DOI]

Proceedings of the 40th IEEE International Symposium on Multiple-Valued Logic, 2010

Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking.

[BibT_eX]

[DOI]

Ashish Darbari

Proceedings of the Theoretical Aspects of Computing, 2010

Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking.

[BibT_eX]

[DOI]

Lucas C. Cordeiro

Proceedings of the 17th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, 2010

On Computing Backbones of Propositional Theories.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2010, 2010

Boolean Lexicographic Optimization.

[BibT_eX]

[DOI]

Proceedings of the 17th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, 2010

Efficient and Accurate Haplotype Inference by Combining Parsimony and Pedigree Information.

[BibT_eX]

[DOI]

Proceedings of the Algebraic and Numeric Biology - 4th International Conference, 2010

2009

Conflict-Driven Clause Learning SAT Solvers.

[BibT_eX]

[DOI]

Sharad Malik

Proceedings of the Handbook of Satisfiability, 2009

Industrial-Strength Formally Certified SAT Solving

[BibT_eX]

[DOI]

Ashish Darbari

CoRR, 2009

Algorithms for finding dispensable variables

[BibT_eX]

[DOI]

Radu Grigore

CoRR, 2009

On Solving Boolean Multilevel Optimization Problems

[BibT_eX]

[DOI]

Josep Argelich

CoRR, 2009

A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas.

[BibT_eX]

[DOI]

Constraints An Int. J., 2009

Algorithms for Weighted Boolean Optimization.

[BibT_eX]

[DOI]

Jordi Planes

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

On Solving Boolean Multilevel Optimization Problemse.

[BibT_eX]

[DOI]

Josep Argelich

Proceedings of the IJCAI 2009, 2009

A Lazy Unbounded Model Checker for Event-B.

[BibT_eX]

[DOI]

Paulo J. Matos

Proceedings of the Formal Methods and Software Engineering, 2009

Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Embedded Software and Systems, 2009

TG-PRO: A new model for SAT-based ATPG.

[BibT_eX]

[DOI]

Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2009

Spatial and temporal design debug using partial MaxSAT.

[BibT_eX]

[DOI]

Proceedings of the 19th ACM Great Lakes Symposium on VLSI 2009, 2009

2008

Backtracking.

[BibT_eX]

[DOI]

Proceedings of the Wiley Encyclopedia of Computer Science and Engineering, 2008

Model checking with Boolean Satisfiability.

[BibT_eX]

[DOI]

J. Algorithms, 2008

Haplotype Inference with Boolean Satisfiability.

[BibT_eX]

[DOI]

Int. J. Artif. Intell. Tools, 2008

A Pseudo-Boolean Solution to the Maximum Quartet Consistency Problem

[BibT_eX]

[DOI]

CoRR, 2008

Boosting Haplotype Inference with Local Search.

[BibT_eX]

[DOI]

Steve Prestwich

Constraints An Int. J., 2008

Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2008

Improvements to Hybrid Incremental SAT Algorithms.

[BibT_eX]

[DOI]

Florian Letombe

Proceedings of the Theory and Applications of Satisfiability Testing, 2008

Symmetry Breaking for Maximum Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2008

Haplotype Inference with Boolean Constraint Solving: An Overview.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2008), 2008

On Applying Unit Propagation-Based Lower Bounds in Pseudo-Boolean Optimization.

[BibT_eX]

[DOI]

Proceedings of the Twenty-First International Florida Artificial Intelligence Research Society Conference, 2008

A MAX-SAT Algorithm Portfolio.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2008, 2008

Algorithms for Maximum Satisfiability using Unsatisfiable Cores.

[BibT_eX]

[DOI]

Jordi Planes

Proceedings of the Design, Automation and Test in Europe, 2008

Efficient Haplotype Inference with Combined CP and OR Techniques.

[BibT_eX]

[DOI]

Proceedings of the Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 2008

Model Checking Event-B by Encoding into Alloy.

[BibT_eX]

[DOI]

Paulo J. Matos

Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

2007

Random backtracking in backtrack search algorithms for satisfiability.

[BibT_eX]

[DOI]

Discret. Appl. Math., 2007

On Using Unsatisfiability for Solving Maximum Satisfiability

[BibT_eX]

[DOI]

Jordi Planes

CoRR, 2007

Report on the SAT 2007 Conference on Theory and Applications of Satisfiability Testing.

[BibT_eX]

[DOI]

AI Mag., 2007

Breaking Symmetries in SAT Matrix Models.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Towards Equivalence Checking Between TLM and RTL Models.

[BibT_eX]

[DOI]

Proceedings of the 5th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2007), May 30, 2007

Efficient and Tight Upper Bounds for Haplotype Inference by Pure Parsimony Using Delayed Haplotype Selection.

[BibT_eX]

[DOI]

Proceedings of the Progress in Artificial Intelligence, 2007

Towards Robust CNF Encodings of Cardinality Constraints.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2007

Efficient Haplotype Inference with Pseudo-boolean Optimization.

[BibT_eX]

[DOI]

Proceedings of the Algebraic Biology, Second International Conference, 2007

2006

On Using Cutting Planes in Pseudo-Boolean Optimization.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2006

Interpolant Learning and Reuse in SAT-Based Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Fourth International Workshop on Bounded Model Checking, 2006

Counting Models in Integer Domains.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

SAT in Bioinformatics: Making the Case with Haplotype Inference.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel.

[BibT_eX]

[DOI]

Oliver Kullmann

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

Efficient Haplotype Inference with Boolean Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 2006

2005

Heuristic-Based Backtracking Relaxation for Propositional Satisfiability.

[BibT_eX]

[DOI]

J. Autom. Reason., 2005

Efficient data structures for backtrack search SAT solvers.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2005

A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2005

On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2005

Good Learning and Implicit Model Enumeration.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2005), 2005

Satisfiability-Based Algorithms for Pseudo-Boolean Optimization Using Gomory Cuts and Search Restarts.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2005), 2005

Effective Lower Bounding Techniques for Pseudo-Boolean Optimization.

[BibT_eX]

[DOI]

Proceedings of the 2005 Design, 2005

Improvements to the Implementation of Interpolant-Based Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2005

2004

Satisfiability-Based Algorithms for Boolean Optimization.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2004

Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization.

[BibT_eX]

[DOI]

Proceedings of the SAT 2004, 2004

On Computing Minimum Unsatisfiable Cores.

[BibT_eX]

[DOI]

Proceedings of the SAT 2004, 2004

Using Rewarding Mechanisms for Improving Branching Heuristics.

[BibT_eX]

[DOI]

Elsa Carvalho

Proceedings of the SAT 2004, 2004

Integration of Lower Bound Estimates in Pseudo-Boolean Optimization.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2004), 2004

Hidden Structure in Unsatisfiable Random 3-SAT: An Empirical Study.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2004), 2004

2003

Solving Satisfiability in Combinational Circuits.

[BibT_eX]

[DOI]

Luís Guerra e Silva

IEEE Des. Test Comput., 2003

An Overview of Backtrack Search Satisfiability Algorithms.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2003

Heuristic Backtracking Algorithms for SAT.

[BibT_eX]

[DOI]

Proceedings of the Fourth International Workshop on Microprocessor Test and Verification, 2003

Probing-Based Preprocessing Techniques for Propositional Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the 15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2003), 2003

Heuristic-Based Backtracking for Propositional Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Progress in Artificial Intelligence, 2003

2002

Satisfiability models and algorithms for circuit delay computation.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2002

Search pruning techniques in SAT-based branch-and-bound algorithmsfor the binate covering problem.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2002

Building State-of-the-Art SAT Solvers.

[BibT_eX]

Proceedings of the 15th European Conference on Artificial Intelligence, 2002

Tuning Randomization in Backtrack Search SAT Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2002

The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Recent Advances in Constraints, 2002

2001

An exact solution to the minimum size test pattern problem.

[BibT_eX]

[DOI]

Horácio C. Neto

ACM Trans. Design Autom. Electr. Syst., 2001

Efficient Algorithms for the Inference of Minimum Size DFAs.

[BibT_eX]

[DOI]

Arlindo L. Oliveira

Mach. Learn., 2001

Stochastic Systematic Search Algorithms for Satisfiability.

[BibT_eX]

[DOI]

Luís Baptista

Electron. Notes Discret. Math., 2001

Towards Provably Complete Stochastic Search Algorithms for Satisfiability.

[BibT_eX]

[DOI]

Luís Baptista

Proceedings of the Progress in Artificial Intelligence, 2001

Improving SAT Algorithms by Using Search Pruning Techniques.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2001

2000

Search Pruning Conditions for Boolean Optimization.

[BibT_eX]

Proceedings of the ECAI 2000, 2000

An Experimental Study of Satisfiability Search Heuristics.

[BibT_eX]

[DOI]

Fadi A. Aloul

Proceedings of the 2000 Design, 2000

On Using Satisfiability-Based Pruning Techniques in Covering Algorithms.

[BibT_eX]

[DOI]

Proceedings of the 2000 Design, 2000

On Applying Incremental Satisfiability to Delay Fault Testing.

[BibT_eX]

[DOI]

Joonyoung Kim

Jesse Whittemore

Proceedings of the 2000 Design, 2000

Boolean satisfiability in electronic design automation.

[BibT_eX]

[DOI]

Proceedings of the 37th Conference on Design Automation, 2000

Algebraic Simplification Techniques for Propositional Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2000

Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability.

[BibT_eX]

[DOI]

Luís Baptista

Proceedings of the Principles and Practice of Constraint Programming, 2000

Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

On Solving Boolean Optimization with Satisfiability-Based Algorithms.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2000

1999

GRASP: A Search Algorithm for Propositional Satisfiability.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 1999

Assignment and Reordering of Incompletely Specified Pattern Sequences Targetting Minimum Power Dissipation.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on VLSI Design (VLSI Design 1999), 1999

Test pattern generation for width compression in BIST.

[BibT_eX]

[DOI]

Horácio C. Neto

Krishnendu Chakrabarty

Proceedings of the 1999 International Symposium on Circuits and Systems, ISCAS 1999, Orlando, Florida, USA, May 30, 1999

Satisfiability-Based Functional Delay Fault Testing.

[BibT_eX]

Joonyoung Kim

Proceedings of the VLSI: Systems on a Chip, 1999

On Applying Set Covering Models to Test Set Compaction.

[BibT_eX]

[DOI]

Horácio C. Neto

Proceedings of the 9th Great Lakes Symposium on VLSI (GLS-VLSI '99), 1999

The Impact of Branching Heuristics in Propositional Satisfiability Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Progress in Artificial Intelligence, 1999

Algorithms for Solving Boolean Satisfiability in Combinational Circuits.

[BibT_eX]

[DOI]

Luís Guerra e Silva

Luís Miguel Silveira

Proceedings of the 1999 Design, 1999

Combinational Equivalence Checking Using Satisfiability and Recursive Learning.

[BibT_eX]

[DOI]

Thomas Glass

Proceedings of the 1999 Design, 1999

1998

Efficient Search Techniques for the Inference of Minimum Size Finite Automata.

[BibT_eX]

[DOI]

Arlindo L. Oliveira

Proceedings of the String Processing and Information Retrieval: A South American Symposium, 1998

Timing analysis using propositional satisfiability.

[BibT_eX]

[DOI]

Luís Guerra e Silva

Luís Miguel Silveira

Proceedings of the 5th IEEE International Conference on Electronics, Circuits and Systems, 1998

Integer Programming Models for Optimization Problems in Test Generation.

[BibT_eX]

[DOI]

Proceedings of the ASP-DAC '98, 1998

1997

Prime Implicant Computation Using Satisfiability Algorithms.

[BibT_eX]

[DOI]

Arlindo L. Oliveira

Proceedings of the 9th International Conference on Tools with Artificial Intelligence, 1997

Robust Search Algorithms for Test Pattern Generation.

[BibT_eX]

[DOI]

Proceedings of the Digest of Papers: FTCS-27, 1997

1996

Ravel-XL: a hardware accelerator for assigned-delay compiled-code logic gate simulation.

[BibT_eX]

[DOI]

Michael A. Riepe

Richard B. Brown

IEEE Trans. Very Large Scale Integr. Syst., 1996

Conflict Analysis in Search Algorithms for Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Eigth International Conference on Tools with Artificial Intelligence, 1996

GRASP - a new search algorithm for satisfiability.

[BibT_eX]

[DOI]

Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, 1996

1994

Efficient and Robust Test Generation-Based Timing Analysis.

[BibT_eX]

[DOI]

Proceedings of the 1994 IEEE International Symposium on Circuits and Systems, ISCAS 1994, London, England, UK, May 30, 1994

Dynamic Search-Space Pruning Techniques in Path Sensitization.

[BibT_eX]

[DOI]

Proceedings of the 31st Conference on Design Automation, 1994

1993

An Analysis of Path Sensitization Criteria.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1993 International Conference on Computer Design: VLSI in Computers & Processors, 1993

Concurrent path sensitization in timing analysis.

[BibT_eX]

[DOI]

Proceedings of the European Design Automation Conference 1993, 1993

1991

FPD - An Environment for Exact Timing Analysis.

[BibT_eX]

[DOI]