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

Authors: Weaver, Sean | Franco, John | Schlipf, John

Article Type: Research Article

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

Keywords: satisfiability, autarky, safe assignment, inference

DOI: 10.3233/SAT190004

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 1, no. 2, pp. 89-110, 2006

Authors: Rolf, Daniel

Article Type: Research Article

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

Keywords: 3-SAT, worst case bound, bounded resolution, randomized local search

DOI: 10.3233/SAT190005

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 1, no. 2, pp. 111-122, 2006

Authors: Lozinskii, Eliezer L.

Article Type: Research Article

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.

Keywords: SAT, phase transition, impurity

DOI: 10.3233/SAT190006

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 1, no. 2, pp. 123-141, 2006