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 14, 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.

An Isomorphism-Invariant Distance Function on Propositional Formulas in CNF

Authors: Dantsin, Evgeny | Wolpert, Alexander

Article Type: Research Article

Abstract: We define a distance function on propositional formulas in CNF as a measure of non-isomorphism of formulas: the larger the distance between two formulas is, the further they are from being isomorphic. This distance induces a metric on isomorphism classes of formulas. We show how this distance can be used for SAT solving, namely for per-instance algorithm selection where there is a “portfolio” of SAT solvers and there is a “meta-solver” that chooses a solver from the portfolio for a given input formula.

Keywords: Distance on CNF formulas, isomorphism invariants, per-instance algorithm selection

DOI: 10.3233/SAT-220006

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

Get PDF open access

OMTPlan: A Tool for Optimal Planning Modulo Theories

Authors: Leofante, Francesco

Article Type: Research Article

Abstract: OMTPlan is a Python platform for optimal planning in numeric domains via reductions to Satisfiability Modulo Theories (SMT) and Optimization Modulo Theories (OMT). Currently, OMTPlan supports the expressive power of PDDL2.1 level 2 and features procedures for both satisficing and optimal planning. OMTPlan provides an open, easy to extend, yet efficient implementation framework. These goals are achieved through a modular design and the extensive use of state-of-the-art systems for SMT/OMT solving.

Keywords: Planning as Satisfiability, Optimisation Modulo Theories

DOI: 10.3233/SAT-220001

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 14, no. 1, pp. 17-23, 2023

Get PDF open access
Show more