Journal on Satisfiability, Boolean Modeling and Computation - Volume 1, issue 2
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 introduce new approaches intended to speed up determining the satisfiability of a given Boolean formula φ expressed as a conjunction of Boolean functions. A common practice in such cases, when using constraint-oriented methods, is to represent the functions as BDDs, then repeatedly cluster BDDs containing one or more variables, and finally existentially quantify those variables away from the cluster. Clustering is essential because, in general, existential quantification cannot be applied unless the variables occur in only a single BDD. But, clustering incurs significant overhead and may result in BDDs that are too big to allow the process to…complete in a reasonable amount of time. There are two significant contributions in this paper. First, we identify elementary conditions under which the existential quantification of a subset of variables V ′ may be distributed over all BDDs without clustering. We show that when these conditions are satisfied, safe assignments to the variables of V ′ are automatically generated. This is significant because these assignments can be applied, as though they were inferences, to simplify φ . Second, some efficient operations based on these conditions are introduced and can be integrated into existing frameworks of both search-oriented and constraint-oriented methods of satisfiability. All of these operations are relaxations in the use of existential quantification and therefore may fail to find one or more existing safe assignments. Finally, we compare and contrast the relationship of these operations to autarkies and present some preliminary results.
Abstract: The PPSZ Algorithm presented by Paturi, Pudlak, Saks, and Zane in 1998 has the nice feature that the only satisfying solution of a uniquely satisfiable 3-SAT formula can be found in expected running time at most O ( 1.3071 n ) . Its bound degenerates when the number of solutions increases. In 1999, Schöning proved an O ( 1.3334 n ) bound for 3-SAT. In 2003, Iwama and Tamaki combined both algorithms to yield an O ( 1.3238 n ) bound. We tweak…the PPSZ-Bound to get a slightly better contribution to the combined algorithm and prove an O ( 1.32216 n ) bound.
Keywords: 3-SAT, worst case bound, bounded resolution, randomized local search
Abstract: It is well known that satisfiability of random sets of propositional clauses undergoes phase transition while the clause-to-variable ratio of the sets increases. We introduce another parameter of sets of clauses, impurity, and show that the satisfiability undergoes a phase transition as a function of impurity. This phenomenon supports a conjecture that various properties (such as random graph connectivity, perfect integer partition) exhibit phase transition under control of several di erent syntactic parameters.