With growing emphasis on sustainable manufacturing, we address the energy-aware Simple Assembly Line Balancing Problem with Power Peak Minimization (SALB3PM). We propose a metaheuristic to solve the SALB3PM. Our metaheuristic combines (1) a multi-start framework with three neighborhood operators (insertion, swap, delay incrementing) and (2) a dynamic penalty mechanism for handling cycle-time infeasibility. We designed and compared four algorithm variants to evaluate the impact of components. We conducted computational experiments on benchmark instances. The results show that our best variant achieves an average optimality gap of 2.38% when considering known optima, and optimal solutions were achieved in all runs for over 50% of instances. The approach contributes to sustainable manufacturing through energy-efficient production line design.

In this paper, we present a tool, called MS-Builder, which generates certificates for the Max-SAT problem in the particular form of a sequence of equivalence-preserving transformations. To generate a certificate, MS-Builder iteratively calls a SAT oracle to get a SAT resolution refutation which is handled and adapted into a sound refutation for Max-SAT. In particular, the size of the computed Max-SAT refutation is linear with respect to the size of the initial refutation if it is semi-read-once, tree-like regular, tree-like or semi-tree-like. Additionally, we propose an extendable tool, called MS-Checker, able to verify the validity of any Max-SAT certificate using Max-SAT inference rules.

Adapting a SAT resolution proof into a Max-SAT resolution proof without considerably increasing its size is an open problem. Read-once resolution, where each clause is used at most once in the proof, represents the only fragment of resolution for which an adaptation using exclusively Max-SAT resolution is known and trivial. Proofs containing non read-once clauses are difficult to adapt because the Max-SAT resolution rule replaces the premises by the conclusions. This paper contributes to this open problem by defining, for the first time since the introduction of Max-SAT resolution, a new fragment of resolution whose proofs can be adapted to Max-SAT resolution proofs without substantially increasing their size. In this fragment, called crossing-free resolution, non read-once clauses are used independently to infer new information thus enabling to bring along each non read-once clause while unfolding the proof until a substitute is required.

Current Max-SAT solvers are able to efficiently compute the optimal value of an input instance but they do not provide any certificate of its validity. In this paper, we present a tool, called MS-Builder, which generates certificates for the Max-SAT problem in the particular form of a sequence of equivalence-preserving transformations. To generate a certificate, MS-Builder iteratively calls a SAT oracle to get a SAT resolution refutation which is handled and adapted into a sound refutation for Max-SAT. In particular, we prove that the size of the computed Max-SAT refutation is linear with respect to the size of the initial refutation if it is semi-read-once, tree-like regular, tree-like or semi-tree-like. Additionally, we propose an extendable tool, called MS-Checker, able to verify the validity of any Max-SAT certificate using Max-SAT inference rules. Both tools are evaluated on the unweighted and weighted benchmark instances of the 2020 Max-SAT Evaluation.

Adapting a resolution refutation for SAT into a Max-SAT resolution refutation without increasing considerably the size of the refutation is an open question. This paper contributes to this topic by introducing an algorithm, called substitute generation, able to adapt any resolution refutation to get a Max-SAT refutation using SAT oracles. This algorithm is able to efficiently adapt k-stacked diamond patterns, whose transformation is exponential in the literature.

In this paper, we are interested in proof systems for Max-SAT and particularly in the construction of Max-SAT equivalence-preserving transformations to infer information from a given formula. To this end, we introduce the notion of explainability and we provide a characterization for explainable clauses and formulas. Furthermore, we introduce a new proof system, called Explanation Calculus (ExC) and composed of two rules: symmetric cut and expansion. We study the relation between ExC and several existing proof systems. Then, we introduce a new algorithm, called explanation algorithm, able to construct an explanation in ExC for any clause or refute its explainability and we extend it for formula explanations. Finally, we use our results on explainability to provide proofs for the Max-SAT problem with a new bound on the number of inference steps in the proof, improving the bound obtained with the Max-SAT resolution calculus.

Adapting a resolution proof for SAT to a Max-SAT resolution proof without increasing considerably the size of the proof is an open question. This paper contributes to this topic by exhibiting linear adaptations, in terms of the input SAT proof size, in restricted cases which are regular tree resolution refutations, tree resolution refutations and a new introduced class of refutations that we refer to as semi-tree resolution refutations. We also extend these results by proposing a complete adaptation for any unrestricted SAT refutation to a Max-SAT refutation, which is exponential in the worst case.