Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability

• URL: http://arxiv.org/abs/2501.17493v1
• Date: Wed, 29 Jan 2025 09:01:26 GMT
• Title: Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability
• Authors: Christoph Jabs, Jeremias Berg, Bart Bogaerts, Matti Järvisalo,
• Abstract summary: We present proof logging based on the VeriPB proof format for multi-objective MaxSAT (MO-MaxSAT) optimization techniques. By implementing VeriPB proof logging into a state-of-the-art multi-objective MaxSAT solver, we show empirically that proof logging can be made scalable for MO-MaxSAT with reasonable overhead.
• Score: 9.078413809849447
• License:
• Abstract: Due to the wide employment of automated reasoning in the analysis and construction of correct systems, the results reported by automated reasoning engines must be trustworthy. For Boolean satisfiability (SAT) solvers - and more recently SAT-based maximum satisfiability (MaxSAT) solvers - trustworthiness is obtained by integrating proof logging into solvers, making solvers capable of emitting machine-verifiable proofs to certify correctness of the reasoning steps performed. In this work, we enable for the first time proof logging based on the VeriPB proof format for multi-objective MaxSAT (MO-MaxSAT) optimization techniques. Although VeriPB does not offer direct support for multi-objective problems, we detail how preorders in VeriPB can be used to provide certificates for MO-MaxSAT algorithms computing a representative solution for each element in the non-dominated set of the search space under Pareto-optimality, without extending the VeriPB format or the proof checker. By implementing VeriPB proof logging into a state-of-the-art multi-objective MaxSAT solver, we show empirically that proof logging can be made scalable for MO-MaxSAT with reasonable overhead.

Related papers

• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  We propose ProofAug, a novel theorem proving method that enjoys superior sample efficiency. Our method is validated on the miniF2F-test benchmark using the open-source deepseek-math-7b-base model and the Isabelle proof assistant.
  arXiv  Detail & Related papers  (2025-01-30T12:37:06Z)
• LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
  The framework combines Monte Carlo Tree Search (MCTS) with iterative Self-Refine to optimize the reasoning path. The framework has been tested on general and advanced benchmarks, showing superior performance in terms of search efficiency and problem-solving capability.
  arXiv  Detail & Related papers  (2024-10-03T18:12:29Z)
• Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects [1.6727186769396274]
  Satisfiability-based automated reasoning is successfully used in software engineering to validate complex software. We tackle the challenge of validating the correctness of FOL* unsatisfiability results. We develop a proof-based diagnosis to explain the cause of unsatisfiability.
  arXiv  Detail & Related papers  (2024-09-13T22:25:58Z)
• Certified MaxSAT Preprocessing [9.717669529984349]
  MaxSAT has become a viable approach for solving NP-hard optimization problems. ensuring correctness of MaxSAT solvers has remained an important concern. We show how pseudo-Boolean proof logging can be used to certify the correctness of a range of modern MaxSAT preprocessing techniques.
  arXiv  Detail & Related papers  (2024-04-26T10:55:06Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  Constrained optimization problems abound in industry, from portfolio optimization to logistics. One of the major roadblocks in solving these problems is the presence of non-trivial hard constraints which limit the valid search space. In this work, we encode arbitrary integer-valued equality constraints of the form Ax=b, directly into U(1) symmetric networks (TNs) and leverage their applicability as quantum-inspired generative models.
  arXiv  Detail & Related papers  (2022-11-16T18:59:54Z)
• DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving [45.21499915442282]
  We propose a novel dynamic-programming approach for solving generalized MaxSAT problems with hybrid constraints. Our versatile framework admits many generalizations of CNF-MaxSAT, such as MaxSAT, Min-MaxSAT, and MinSAT with hybrid constraints. Empirical results indicate that DPMS is able to solve certain problems quickly, where other algorithms based on various techniques all fail.
  arXiv  Detail & Related papers  (2022-05-08T00:31:53Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Incomplete MaxSAT Approaches for Combinatorial Testing [0.0]
  We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length. This problem is central in Combinatorial Testing for the detection of system failures.
  arXiv  Detail & Related papers  (2021-05-26T14:00:56Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)
• Fault Tree Analysis: Identifying Maximum Probability Minimal Cut Sets with MaxSAT [0.342658286826597]
  We model the MPMCS problem as a weighted Partial MaxSAT problem and solve it using a parallel SAT-solving architecture. The results obtained with our open source tool indicate that the approach is effective and efficient.
  arXiv  Detail & Related papers  (2020-05-05T19:47:15Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.