Journal on Satisfiability, Boolean Modeling and Computation - Volume 15, issue 1

Authors: Nadel, Alexander

Article Type: Research Article

Abstract: We present our anytime MaxSAT solver TT-Open-WBO-Inc , focusing on its evolution since the initial version that won both of the weighted incomplete tracks of MaxSAT Evaluation 2019 (MSE19). The solver’s MSE20 version claimed victory in these tracks at MSE20 and secured second place in both unweighted incomplete tracks. The major innovation in the MSE20 version was the integration of SAT-based local search. The contributions of this paper include: (1) Introducing a previously unpublished variant of the SAT-based local search algorithm Polosat , Polosat-OBV , applied by default already in the MSE20 version, and showing its superiority for weighted solving; …(2) Describing and analyzing TT-Open-WBO-Inc ’s unweighted component, not studied in previous work; (3) Demonstrating that integrating the local search algorithm SATLike into TT-Open-WBO-Inc as a preprocessor enables it to outperform the winners of MSE20 in all four incomplete tracks. Show more

Keywords: MaxSAT, anytime MaxSAT, Mrs. Beaver, Polosat, SAT-based Local Search

DOI: 10.3233/SAT-231504

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 15, no. 1, pp. 1-7, 2024

Authors: Beyersdorff, Olaf | Clymo, Judith | Dantchev, Stefan | Martin, Barnaby

Article Type: Research Article

Abstract: We give an analogue of the Riis Complexity Gap Theorem in Resolution for Quantified Boolean Formulas (QBFs). Every first-order sentence ϕ without finite models gives rise to a sequence of QBFs whose minimal refutations in tree-like QBF Resolution systems are either of polynomial size (if ϕ has no models) or at least exponential in size (if ϕ has some infinite model). However, we show that this gap theorem is sensitive to the translation and different translations are needed for different QBF resolution systems. For tree-like Q-Resolution, the translation to QBF must be given additional structure in order for the polynomial …upper bound to hold. This extra structure is not needed in the system tree-like ∀Exp+ Res, where we see the complexity gap on a natural translation to QBF. Show more

Keywords: Complexity gap, proof complexity, quantified boolean formulas, resolution

DOI: 10.3233/SAT-231505

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 15, no. 1, pp. 9-25, 2024

Authors: Beyersdorff, Olaf | Hoffmann, Tim | Spachmann, Luc N.

Article Type: Research Article

Abstract: Recently, the proof system MICE for the model counting problem #SAT was introduced by Fichte, Hecher and Roland (SAT’22). As demonstrated by Fichte et al., the system MICE can be used for proof logging for state-of-the-art #SAT solvers. We perform a proof-complexity study of MICE . For this we first simplify the rules of MICE and obtain a calculus MIC E ′ that is polynomially equivalent to MICE . We then establish an exponential lower bound for the number …of proof steps in MIC E ′ (and hence also in MICE ) for a specific family of CNFs. We also explain a tight connection between MIC E ′ proofs and decision DNNFs. Show more

Keywords: Model counting, #SAT, proof complexity, proof systems, lower bounds

DOI: 10.3233/SAT-231507

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 15, no. 1, pp. 27-59, 2024