Abstract
-----------
Recently, we have been witness to significant progress in both theoretical and practical research concerning the backtrack search algorithms for the propositional satisfiability (SAT) problem. The progress is underlined by the fact that several solvers introduced in the SAT 2003 competition were able to solve within 15 minutes instances remained unsolved within six hours by state-of-the-art SAT solvers during the SAT 2002 competition. In our talk we introduce the main ideas behind the SAT solver Jerusat which has displayed good performance during the SAT 2003 competition. After a short overview we will introduce innovations incorporated in Jerusat concerning six independent aspects of SAT research: 1. The CRSAT algorithm -- a new algorithm generalizing DPLL and a few related pruning techniques. 2. ALNIC (Add Low NI-level Clauses) restart strategies, ensuring that paths are not repeated after a restart. 3. VAPQ (Variables Activity Priority Queue), a generic data structure for variable-activity-based heuristic. 4. The WLCC (Watched List with Conflicts Counter) data structure for clause representation, which combines the advantages of the WL data structure and data structures using literal-sifting 5. LDRBL (Literals Density Relevance-Based Learning) -- a technique to filter newly recorded clauses. 6. Shrinking schemes - a way to adjust the assigned variables stack to the input formula structure by shrinking it