150 citations · 619 across the 52 of their papers we have counts for
19 papers · 1 filter
Solving QBF with Counterexample Guided Refinement
Mikoláš Janota, William Klieber, Joao Marques-Silva +1
We propose two novel approaches for using Counterexample-Guided Abstraction Refinement (CEGAR) in Quantified Boolean Formula (QBF) solvers. The first approach develops a recursive…
Solving QBF by Clause Selection
Mikoláš Janota, Joao Marques-Silva
Algorithms based on the enumeration of implicit hitting sets find a growing number of applications, which include maximum satisfiability and model based diagnosis, among others. Th…
Model Based Diagnosis of Multiple Observations with Implicit Hitting Sets
Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva
Model based diagnosis finds a growing range of practical applications, and significant performance-wise improvements have been achieved in recent years. Some of these improvements…
Horn Maximum Satisfiability: Reductions, Algorithms & Applications
Joao Marques-Silva, Alexey Ignatiev, Antonio Morgado
Recent years have witness remarkable performance improvements in maximum satisfiability (MaxSAT) solvers. In practice, MaxSAT algorithms often target the most generic MaxSAT formul…
On Tackling the Limits of Resolution in SAT Solving
Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva
The practical success of Boolean Satisfiability (SAT) solvers stems from the CDCL (Conflict-Driven Clause Learning) approach to SAT solving. However, from a propositional proof com…
Efficient Certified Resolution Proof Checking
Luís Cruz-Filipe, Joao Marques-Silva, Peter Schneider-Kamp
We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstra…