Ace is a package that compiles a Bayesian network into an Arithmetic Circuit (AC) and then uses the AC to answer queries with respect to the network. Compilation proceeds by encoding the network into CNF, factoring the CNF, and extracting the AC from the factored logic.

A compiler for converting CNF into d-DNNF (deterministic, decomposable negation normal form): a tractable form allowing operations such as model counting and clausal entailment to be performed in linear time.

Clone is a branch-and-bound Max-SAT solver which uses a novel approach for computing bounds. Problems instances are first relaxed and then compiled into a tractable form. These techniques together give the branch-and-bound solver the ability to compute bounds, while finding a solution in a reduced search space.

Dtree-SAT is an implementation of a variable group ordering heuristic for Propositional Satisfiability (SAT), proposed in [IJCAI03:HD], which exploits the structure of CNF formulas via their decomposition trees (dtrees). zChaff is used as the underlying SAT solver.

The XAI page includes software packages for explaining machine learning classifiers.

We have a collection of compilers which convert different types of classifiers into Sentential Decision Diagrams. We then use the STEP software package to run explanation queries on the SDDs.

A software package for knowledge compilation and model counting based on exhaustive DPLL. For knowledge compilation, it can be used to compile CNFs into Sentential Decision Diagrams (SDDs). For model counting, it can be used to do (weighted) model counting of CNFs.

Genetic linkage analysis is a statistical method for ordering genes on a chromosome and determining the distance between them, and is very useful in predicting and detecting diseases and associating functions to genes. RC_Link is a tool for doing genetic linkage analysis computations. It models the problem as a Bayesian network, and then simplifies the network and computes the results using the Recursive Conditioning algorithm.

Rsat is a DPLL-based complete SAT solver. Rsat won the third place in the SAT-Race 2006 competition.

SamIam is a comprehensive tool for modeling and reasoning with Bayesian networks, developed in Java by the Automated Reasoning Group of Professor Adnan Darwiche at UCLA.

Samiam includes two main components: a graphical user interface and a reasoning engine. The graphical interface allows users to develop Bayesian network models and to save them in a variety of formats. The reasoning engine supports many tasks including: classical inference; parameter estimation; time-space tradeoffs; sensitivity analysis; and explanation-generation based on MAP and MPE.

The SDD package is a system for constructing, manipulating and optimizing Sentential Decision Diagrams (SDDs).