You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

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

open access

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.

Backdoors into Two Occurrences

Authors: Johannsen, Jan

Article Type: Research Article

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. … Show more

Keywords: Backdoor set, fixed-parameter tractability, parameterized complexity, completeness, formulas with two variable occurrences

DOI: 10.3233/SAT-200125

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

Get PDF open access

Polarity and Variable Selection Heuristics for SAT-Based Anytime MaxSAT

Authors: Nadel, Alexander

Article Type: Research Article

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.

Keywords: SAT, MAXSAT, heuristics

DOI: 10.3233/SAT-200126

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 12, no. 1, pp. 17-22, 2020

Get PDF open access
Show more