Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories

Maximum satisfiability (MaxSat) solving is an active area of research motivated by numerous successful applications to solving NP-hard combinatorial optimization problems. One of the most successful approaches for solving MaxSat instances from real world domains are the so called implicit hitting set (IHS) solvers. IHS solvers decouple MaxSat solving into separate core-extraction (i.e. reasoning) and optimization steps which are tackled by a Boolean satisfiability (SAT) and an integer linear programming (IP) solver, respectively. While the approach shows state-of-the-art performance on many industrial instances, it is known that there exists instances on which IHS solvers need to extract an exponential number of cores before terminating. Motivated by the simplest of these problematic instances, we propose abstract cores, a compact representation for a potentially exponential number of regular cores. We demonstrate how to incorporate abstract core reasoning into the IHS algorithm and report on an empirical evaluation demonstrating, that including abstract cores into a state-of-the-art IHS solver improves its performance enough to surpass the best performing solvers of the 2019 MaxSat Evaluation.

Download Full-text

Concurrency Debugging with MaxSMT

Proceedings of the AAAI Conference on Artificial Intelligence ◽

10.1609/aaai.v33i01.33011608 ◽

2019 ◽

Vol 33 ◽

pp. 1608-1616 ◽

Cited By ~ 2

Author(s):

Miguel Terra-Neves ◽

Nuno Machado ◽

Ines Lynce ◽

Vasco Manquinho

Keyword(s):

Satisfiability Modulo Theories ◽

Huge Number ◽

Sequential Programs ◽

Concurrency Bugs ◽

Maximum Satisfiability ◽

Smt Solver ◽

Root Cause ◽

Recent Approach ◽

Sat Solver ◽

Current Maximum

Current Maximum Satisfiability (MaxSAT) algorithms based on successive calls to a powerful Satisfiability (SAT) solver are now able to solve real-world instances in many application domains. Moreover, replacing the SAT solver with a Satisfiability Modulo Theories (SMT) solver enables effective MaxSMT algorithms. However, MaxSMT has seldom been used in debugging multi-threaded software.Multi-threaded programs are usually non-deterministic due to the huge number of possible thread operation schedules, which makes them much harder to debug than sequential programs. A recent approach to isolate the root cause of concurrency bugs in multi-threaded software is to produce a report that shows the differences between a failing and a non-failing execution. However, since they rely solely on heuristics, these reports can be unnecessarily large. Hence, reports may contain operations that are not relevant to the bug’s occurrence.This paper proposes the use of MaxSMT for the generation of minimal reports for multi-threaded software with concurrency bugs. The proposed techniques report situations that the existing techniques are not able to identify. Experimental results show that using MaxSMT can significantly improve the accuracy of the generated reports and, consequently, their usefulness in debugging the root cause of concurrency bugs.

Download Full-text

Reduced Cost Fixing for Maximum Satisfiability

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

10.24963/ijcai.2018/723 ◽

2018 ◽

Cited By ~ 2

Author(s):

Fahiem Bacchus ◽

Antti Hyttinen ◽

Matti Järvisalo ◽

Paul Saikko

Keyword(s):

Integer Programming ◽

Real World ◽

Recent Trend ◽

Optimization Problems ◽

State Of The Art ◽

Boolean Satisfiability ◽

Maximum Satisfiability ◽

Hitting Set ◽

Sat Solvers ◽

Speed Up

Maximum satisfiability (MaxSAT) offers a competitive approach to solving NP-hard real-world optimization problems. While state-of-the-art MaxSAT solvers rely heavily on Boolean satisfiability (SAT) solvers, a recent trend, brought on by MaxSAT solvers implementing the so-called implicit hitting set (IHS) approach, is to integrate techniques from the realm of integer programming (IP) into the solving process. This allows for making use of additional IP solving techniques to further speed up MaxSAT solving. In this line of work, we investigate the integration of the technique of reduced cost fixing from the IP realm into IHS solvers, and empirically show that reduced cost fixing considerable speeds up a state-of-the-art MaxSAT solver implementing the IHS approach.

Download Full-text

Engineering Theories with Z3

10.29007/x7b4 ◽

2018 ◽

Author(s):

Nikolaj Bjorner

Keyword(s):

Satisfiability Modulo Theories ◽

Smt Solver ◽

Testing Tools ◽

Software And Hardware ◽

Design And Testing

Modern Satisfiability Modulo Theories (SMT)solvers are fundamental to many programanalysis, verification, design and testing tools. They are a goodfit for the domain of software and hardware engineering becausethey support many domains that are commonly used by the tools.The meaning of domains are captured by theories that can beaxiomatized or supported by efficient <i>theory solvers</i>.Nevertheless, not all domains are handled by all solvers andmany domains and theories will never be native to any solver.We here explore different theories that extend MicrosoftResearch's SMT solver Z3's basicsupport. Some can be directly encoded or axiomatized,others make use of user theory plug-ins.Plug-ins are a powerful way for tools to supply their custom domains.

Download Full-text

Satisfiability modulo theories for high integrity development

ACM SIGAda Ada Letters ◽

10.1145/2658982.2527287 ◽

2013 ◽

Vol 33 (3) ◽

pp. 5-6 ◽

Cited By ~ 1

Author(s):

Nikolaj Bjorner

Keyword(s):

Satisfiability Modulo Theories ◽

High Integrity

Download Full-text

Unsatisfiable Core Analysis and Aggregates for Optimum Stable Model Search

Fundamenta Informaticae ◽

10.3233/fi-2020-1974 ◽

2020 ◽

Vol 176 (3-4) ◽

pp. 271-297

Author(s):

Mario Alviano ◽

Carmine Dodaro

Keyword(s):

State Of The Art ◽

Answer Set Programming ◽

Efficient Algorithms ◽

Satisfiability Problem ◽

Core Analysis ◽

Stable Model ◽

Maximum Satisfiability ◽

Model Search ◽

Unsatisfiable Core ◽

Stable Models

Many efficient algorithms for the computation of optimum stable models in the context of Answer Set Programming (ASP) are based on unsatisfiable core analysis. Among them, algorithm OLL was the first introduced in the context of ASP, whereas algorithms ONE and PMRES were first introduced for solving the Maximum Satisfiability problem (MaxSAT) and later on adapted to ASP. In this paper, we present the porting to ASP of another state-of-the-art algorithm introduced for MaxSAT, namely K, which generalizes ONE and PMRES. Moreover, we present a new algorithm called OLL-IN-ONE that compactly encodes all aggregates of OLL by taking advantage of shared aggregate sets propagators. The performance of the algorithms have been empirically compared on instances taken from the latest ASP Competition.

Download Full-text