SBSAT swMATH ID: 828 Software Authors: Franco, John; Kouril, Michal; Schlipf, John; Ward, Jeffrey; Weaver, Sean; Dransfield, Michael; Vanfleet, W.Mark Description: SBSAT: a state-based, BDD-based satisfiability solver We present a new approach to SAT solvers, supporting efficient implementation of highly sophisticated search heuristics over a range of propositional inputs, including CNF formulas, but particularly sets of arbitrary boolean constraints, represented as BDDs. The approach preprocesses the BDDs into state machines to allow for fast inferences based upon any single input constraint. It also simplifies the set of constraints, using a tool set similar to standard BDD engines. And it memoizes search information during an extensive preprocessing phase, allowing for a new form of lookahead, called local-function-complete lookahead. This approach has been incorporated, along with existing tools such as lemmas, to build a SAT tool we call SBSAT.par Because of its memoization of constraint-by-constraint lookahead information, besides incorporation of standard lemmas, SBSAT also provides a convenient platform for experimentation with search heuristics. This experimentation is ongoing.par We show the feasibility of SBSAT by comparing it to zChaff on several of the benchmarks. We also show an interesting dependence of some standard benchmarks upon simply the independent/dependent variable distinction. Homepage: http://www.cs.uc.edu/~weaversa/SBSAT.html Keywords: Satisfiability; State Machine; Binary Decision Diagram; DAG Related Software: FORCE; Chaff; BerkMin; zChaff; sharpSAT; MiniSat; Velev SAT Benchmarks; CUDD; CirCUs Cited in: 9 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year SBSAT: a state-based, BDD-based satisfiability solver. Zbl 1204.68193Franco, John; Kouril, Michal; Schlipf, John; Ward, Jeffrey; Weaver, Sean; Dransfield, Michael; Vanfleet, W. Mark 2004 all top 5 Cited by 20 Authors 2 Biere, Armin 2 Castaño, José M. 2 Castaño, Rodrigo 2 Pan, Guoqiang 2 Sinz, Carsten 2 Vardi, Moshe Ya’akov 1 Chen, Wei 1 Dransfield, Michael R. 1 Franco, John V. 1 Jin, HoonSang 1 Jussila, Toni 1 Kouril, Michal 1 Schlipf, John Stewart 1 Somenzi, Fabio 1 Su, Kaile 1 Vanfleet, W. Mark 1 Ward, Jeffrey A. 1 Weaver, Sean A. 1 Xu, Yanyan 1 Zhang, Wenhui Cited in 2 Serials 1 Theoretical Computer Science 1 Journal of Automated Reasoning Cited in 1 Field 9 Computer science (68-XX) Citations by Year