Abstract: Backdoor sets for the class CNF(2) of CNF-formulas in which every variable has at most two occurrences are studied in terms of parameterized complexity. The question whether there exists a CNF(2)-backdoor set of size k is hard for the class W[2] , for both weak and strong backdoors, and in both cases it becomes fixed-parameter tractable when restricted to inputs in d-CNF for a fixed d . Besides that, it is shown that the problem of finding weak backdoor sets is W[2]-complete, for certain tractable cases. These are the first completeness results in lower levels of the W-hierarchy for any backdoor set problems.
Journal on Satisfiability, Boolean Modeling and Computation ISSN: 1574-0617
JSAT is an open access peer reviewed journal, publishing high quality original research papers and
survey papers which evidently contribute to deeper insight. It is an electronic medium, guaranteeing
fast publication.
JSAT volume 12
Volume for papers published in 2020.
JSAT promotes Open Science. As such, the authors are encouraged to provide additional resources to complement their article:
Software
Benchmarks
Raw data
Scripts/Tools
The above icons before the title of the article mean that the article is complemented by those resources. Articles provided all of them are awarded the open science badge.
Table of Contents
Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT System Description, , 17-22.
SAT
MAXSAT
Heuristics
Abstract: This paper is a system description of the anytime MaxSAT solver TT-Open-WBO-Inc, which won both of the weighted incomplete tracks of MaxSAT Evaluation 2019. We implemented the recently introduced polarity and variable selection heuristics, TORC and TSB, respectively, in the Open-WBO-Inc-BMO algorithm within the open-source anytime MaxSAT solver Open-WBO-Inc. As a result, the solver is substantially more efficient.
Software