Abstract
At the heart of computer science and artificial intelligence, logic is often used as a powerful language to model and solve complex problems that arise in academia and in real-world applications. A well-known formalism in this context is the Satisfiability (SAT) problem which simply checks whether a given propositional formula in the form of a set of constraints, called clauses, can be satisfied. A natural optimization extension of this problem is Maximum Satisfiability (Max-SAT) which consists in determining the maximum number of clausal constraints that can be satisfied within the formula. In our work, we are interested in studying the power and limits of inference and reasoning in the context of (Maximum) Satisfiability. Our first contributions revolve around investigating inference in SAT and Max-SAT solving. First, we study statistical inference within a Multi-Armed Bandit (MAB) framework for online selection of branching heuristics in SAT and we show that it can further enhance the efficiency of modern clause-learning solvers. Moreover, we provide further insights on the power of inference in Branch and Bound algorithms for Max-SAT solving through the property of UP-resilience. Our contributions also extend to SAT and Max-SAT proof theory. We particularly attempt to theoretically bridge the gap between SAT and Max-SAT inference.
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Cherif, M.S. Reasoning and inference for (Maximum) satisfiability: new insights. Constraints 28, 513–514 (2023). https://doi.org/10.1007/s10601-023-09365-0
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10601-023-09365-0