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.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Castaño, José M.; Castaño, Rodrigo: A finite state intersection approach to propositional satisfiability (2012)
- Xu, Yanyan; Chen, Wei; Su, Kaile; Zhang, Wenhui: Solving difficult SAT problems by using OBDDs and greedy clique decomposition (2012)
- Castaño, José M.; Castaño, Rodrigo: Variable and clause ordering in an FSA approach to propositional satisfiability (2011)
- Jussila, Toni; Sinz, Carsten; Biere, Armin: Extended resolution proofs for symbolic SAT solving with quantification (2006)
- Sinz, Carsten; Biere, Armin: Extended resolution proofs for conjoining BDDs (2006)
- Su, Kai-Le; Chen, Qing-Liang; Sattar, Abdul; Yue, Wei-Ya; Lv, Guan-Feng; Zheng, Xi-Zhong: Verification of authentication protocols for epistemic goals via SAT compilation (2006) ioport
- Jin, HoonSang; Somenzi, Fabio: CirCUs: A hybrid satisfiability solver (2005)
- Pan, Guoqiang; Vardi, Moshe Y.: Symbolic techniques in satisfiability solving (2005)
- Pan, Guoqiang; Vardi, Moshe Y.: Search vs. symbolic techniques in satisfiability solving (2005)
- Franco, John; Kouril, Michal; Schlipf, John; Ward, Jeffrey; Weaver, Sean; Dransfield, Michael; Vanfleet, W. Mark: SBSAT: a state-based, BDD-based satisfiability solver (2004)