Software Title:Ace
Web-Site:http://reasoning.cs.ucla.edu/ace
Description:
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.
Software Title:c2d Compiler
Web-Site:http://reasoning.cs.ucla.edu/c2d/
Description:
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.
Software Title:Clone
Web-Site:http://reasoning.cs.ucla.edu/clone
Description:
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.
Software Title:Dtree-SAT
Web-Site:http://reasoning.cs.ucla.edu/dtree_sat/
Description:
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.
Software Title:miniC2D
Web-Site:http://reasoning.cs.ucla.edu/minic2d/
Description:
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.
Software Title:RC_Link
Web-Site:http://reasoning.cs.ucla.edu/rc_link
Description:
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.
Software Title:RSat
Web-Site:http://reasoning.cs.ucla.edu/rsat
Description:
Rsat is a DPLL-based complete SAT solver. Rsat won the third place in the SAT-Race 2006 competition.
Software Title:SamIam
Web-Site:http://reasoning.cs.ucla.edu/samiam/
Description:
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.
Software Title:Sentential Decision Diagrams (SDDs)
Web-Site:http://reasoning.cs.ucla.edu/sdd/
Description:
The SDD package is a system for constructing, manipulating and optimizing Sentential Decision Diagrams (SDDs).