Journal on Satisfiability, Boolean Modeling and Computation - Volume 15, issue 1
Open Access
ISSN
1574-0617 (E)
The scope of JSAT is propositional reasoning, modeling, and computation. The Satisfiability discipline is a central focus of JSAT. We welcome all sorts of contributions to this theme but also encourage authors to submit papers on related topics as Computational Logic, Constraint Programming, Satisfiability Modulo Theories, Quantified Boolean Logic, Pseudo Boolean Methods, zero-one Programming, Integer Programming and Operations Research, whenever the link to Satisfiability is apparent.
Especially JSAT welcomes substantial extensions of conference papers, where the actual conference contribution must be cited. As such, authors are able to provide more detailed information about their work (theoretical details, proofs or theorems, algorithmic or implementation details, more exhaustive empirical evaluations) which were enforced to be omitted in the conference proceedings simply because of strict page limitations.
JSAT also welcomes detailed descriptions of new promising but challenging applications around SAT, to make the SAT community aware of those new applications, and to provide it the opportunity to tackle those challenges.
Occasionally JSAT also publishes Research Notes. Research Notes are also thoroughly reviewed but are not considered full Journal publications and hence will be designated and must be referenced to as such. Also, JSAT publishes papers on System Descriptions, being contributions with a focus on the internals of a Solver.
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
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
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