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

Horn Upper Bounds and Renaming

Authors: Langlois, Marina | Sloan, Robert H. | Turán, György

Article Type: Research Article

Abstract: Selman and Kautz [22] proposed an approach to compute a Horn CNF approximation of CNF formulas. We extend this approach and propose a new algorithm for the Horn least upper bound that involves renaming variables. Although we provide negative results for the quality of approximation, experimental results for random CNF demonstrate that the proposed algorithm improves both computational efficiency and approximation quality. We observe an interesting behavior in the Horn approximation sizes and errors which we call the “Horn bump”: Maxima occur in an intermediate range of densities below the satisfiability threshold.

Keywords: Horn approximation, renaming, random satisfying assignment

DOI: 10.3233/SAT190072

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

Get PDF open access

Resolution on Quantified Generalized Clause-sets

Authors: Jin, Jiwei | Zhao, Xishun

Article Type: Research Article

Abstract: This paper is devoted to investigate resolution for quantified generalized clause-sets (QCLS). The soundness and refutation completeness are proved. Then quantified generalized Horn clause-sets are introduced for which a restricted resolution, called quantified positive unit resolution, is proved to be sound and refutationally complete. Moreover, it is shown that the satisfiability for quantified generalized Horn clause-sets is solvable in polynomial time. On the one hand, the work of this paper can be considered as a generalization of resolution for generalized clause-sets (CLS). On the other hand, it also can be considered as a generalization of Q-resolution for … Show more

Keywords: quantified generalized clause-sets, satisfiability, Q-resolution, Horn

DOI: 10.3233/SAT190073

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 1, pp. 17-34, 2010

Get PDF open access

Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond

Authors: Tveretina, Olga | Sinz, Carsten | Zantema, Hans

Article Type: Research Article

Abstract: Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has exponential size, and that limited OBDD derivations cannot simulate resolution polynomially. Here we show that an arbitrary OBDD refutation of the pigeonhole formula has exponential size: we prove that for any order of computation at least one intermediate OBDD in the proof has size Ω ( 1.14 n ) . We also present a family of CNFs that show an exponential blow-up for all OBDD refutations compared to unrestricted resolution refutations.

Keywords: ordered binary decision diagrams, resolution, pigeonhole formulas, lower bounds

DOI: 10.3233/SAT190074

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 1, pp. 35-58, 2010

Get PDF open access
Show more