Sathiamoorthy Subbarayan

IJCAI Conference 2007 Conference Paper

• Sathiamoorthy Subbarayan
• Henrik Reif Andersen

Hypertree decomposition has been shown to be the most general CSP decomposition method. However, so far the exact methods are not able to find optimal hypertree decompositions of realistic instances. We present a backtracking procedure which, along with isomorphic component detection, results in optimal hypertree decompositions. We also make the procedure generic; variations of which results in two new tractable decompositions: hyperspread and connected hypertree. We show that the hyperspread width is bounded by both the hypertree width and the spread cut width, which solves a recently stated open problem. In our experiments on several realistic instances, our methods find many optimal decompositions, while the previous methods can find at most one.

AAAI Conference 2007 Conference Paper

Knowledge Compilation Properties of Tree-of-BDDs

• Sathiamoorthy Subbarayan

We present a CNF to Tree-of-BDDs (ToB) compiler with complexity at most exponential in the tree width. We then present algorithms for interesting queries on ToB. Although some of the presented query algorithms are in the worst case exponential in the tree width, our experiments show that ToB can answer non-trivial queries like clausal entailment in reasonable time for several realistic instances. While our ToB-tool compiles all the used 91 instances, d-DNNF compilation failed for 12 or 8 of them based on the decomposition heuristic used. Also, on the succeeded instances, a d-DNNF is up to 1000 times larger than the matching ToB. The ToB compilations are often an order of magnitude faster than the d-DNNF compilation. This makes ToB a quite interesting knowledge compilation form.

SAT Conference 2004 Conference Paper

NiVER: Non Increasing Variable Elimination Resolution for Preprocessing SAT instances

• Sathiamoorthy Subbarayan
• Dhiraj K. Pradhan

The original algorithm for the SAT problem, Variable Elimination Resolution (VER/DP) has exponential space complexity. To tackle that, the backtracking based DPLL procedure [2] is used in SAT solvers. We present a combination of both of the techniques. We use NiVER, a special case of VER, to eliminate some variables in a preprocessing step and then solve the simplified problem using a DPLL SAT solver. NiVER is a strictly formula size not increasing resolution based preprocessor. Best worst-case upper bounds for general SAT solving (arbitrary clause length) in terms of N (Number of variables), K (Number of clauses) and L (Literal count) are 2N , 20.30897K and 20.10299L , respectively [14]. In the experiments, NiVER resulted in upto 74% decrease in N , 58% decrease in K and 46% decrease in L. In many real life instances, we observed that most of the resolvents for several variables are tautologies. There will be no increase in space due to VER on them. Hence, despite its simplicity, NiVER does result in easier instances. In most of the cases, NiVER takes less than one second for preprocessing. In case NiVER removable variables are not present, due to very low overhead, the cost of NiVER is insignificant. We also study the effect of combining NiVER with HyPre [3], a preprocessor based on hyper binary resolution. Based on experimental results, we classify the SAT instances into 4 classes. NiVER consistently performs well in all those classes and hence can be incorporated into all general purpose SAT solvers.