Computing and Information Systems - Research Publications
Permanent URI for this collection
Search Results
1 - 5 of 5
-
ItemLazy Clause Generation: Combining the Power of SAT and CP (and MIP?) Solving(SPRINGER-VERLAG BERLIN, 2010)
-
ItemMUSTANG-MR Structural Sieving Server: Applications in Protein Structural Analysis and Crystallography(PUBLIC LIBRARY SCIENCE, 2010-04-06)BACKGROUND: A central tenet of structural biology is that related proteins of common function share structural similarity. This has key practical consequences for the derivation and analysis of protein structures, and is exploited by the process of "molecular sieving" whereby a common core is progressively distilled from a comparison of two or more protein structures. This paper reports a novel web server for "sieving" of protein structures, based on the multiple structural alignment program MUSTANG. METHODOLOGY/PRINCIPAL FINDINGS: "Sieved" models are generated from MUSTANG-generated multiple alignment and superpositions by iteratively filtering out noisy residue-residue correspondences, until the resultant correspondences in the models are optimally "superposable" under a threshold of RMSD. This residue-level sieving is also accompanied by iterative elimination of the poorly fitting structures from the input ensemble. Therefore, by varying the thresholds of RMSD and the cardinality of the ensemble, multiple sieved models are generated for a given multiple alignment and superposition from MUSTANG. To aid the identification of structurally conserved regions of functional importance in an ensemble of protein structures, Lesk-Hubbard graphs are generated, plotting the number of residue correspondences in a superposition as a function of its corresponding RMSD. The conserved "core" (or typically active site) shows a linear trend, which becomes exponential as divergent parts of the structure are included into the superposition. CONCLUSIONS: The application addresses two fundamental problems in structural biology: first, the identification of common substructures among structurally related proteins--an important problem in characterization and prediction of function; second, generation of sieved models with demonstrated uses in protein crystallographic structure determination using the technique of Molecular Replacement.
-
ItemFast Set Bounds Propagation Using a BDD-SAT Hybrid(AI ACCESS FOUNDATION, 2010)Binary Decision Diagram (BDD) based set bounds propagation is a powerful approach to solving set-constraint satisfaction problems. However, prior BDD based techniques in- cur the significant overhead of constructing and manipulating graphs during search. We present a set-constraint solver which combines BDD-based set-bounds propagators with the learning abilities of a modern SAT solver. Together with a number of improvements beyond the basic algorithm, this solver is highly competitive with existing propagation based set constraint solvers.
-
ItemIncremental Satisfiability and Implication for UTVPI Constraints(INFORMS, 2010-09-01)Unit two-variable-per-inequality (UTVPI) constraints form one of the largest class of integer constraints that are polynomial time solvable (unless P = NP). There is considerable interest in their use for constraint solving, abstract interpretation, spatial database algorithms, and theorem proving. In this paper we develop new incremental algorithms for UTVPI constraint satisfaction and implication checking that require ℴ(m + n log n + p) time and ℴ(n + m + p) space to incrementally check satisfiability of m UTVPI constraints on n variables, and we check the implication of p UTVPI constraints. The algorithms can be straightforwardly extended to create nonincremental implication checking and generation of all (nonredundant) implied constraints, as well as generate minimal unsatisfiable subsets and minimal implicants.
-
ItemPhilosophy of the MiniZinc challenge(SPRINGER, 2010-07)