Abstraction-based Satisfiability Solving of Presburger Arithmetic

Topics:
Electrical and Electronic
Tags:
Abstraction,
Carnegie-Mellon University,
Engineering,
Formula
Source:
Carnegie Mellon University

FREE Registration is required

Overview: This white paper presents a new abstraction-based framework for deciding satisfiability of quantifier free Presburger arithmetic formulas. The efficiency of this approach derives from the ability of SAT solvers to extract small unsatisfiable cores, leading to small abstracted formulas. The paper also presents experimental results which suggest that the algorithm is considerably more efficient than directly invoking the theorem prover on the original formula.

(Is this item miscategorized? Does it need more tags? Let us know.)

Format: PDF | Size: 194KB | Date: Jan 2004 | Pages: 16

Top results from Electrical and Electronic

White Paper Asserting Control, Seizing Opportunity in High Tech: Five Critical Success Factors
White Paper Control Schema Yields a Better Textile Machine
White Paper Electronics Manufacturing in Emerging Markets Will See Five-Year Growth of $60 Billion by 2005
White Paper Essential Cooling System Requirements for Next Generation Data Centers
White Paper Merchant Markets and Applications for AC/DC Switching Power Supplies, DC/DC Converters, and Telecom Rectifiers

» View all Electrical and Electronic listings

advertisement
advertisement
  • Click Here
  • Click Here
  • Click Here
advertisement

Returning users: Log In Here!

Already registered on BNET, TechRepublic, or ZDNet? Simply log in.

Free Membership: Sign Up Now!

Sign up for a free membership today and get instant and unlimited access to one of the largest databases of white papers, webcasts, and casestudies anywhere. Your FREE membership allows you to:

  • Download an unlimited amount of content, including classic and current white papers, case studies, webcasts and more
  • Track content on your chosen topics of interest
  • Receive targeted email alerts when your favorite content is added
  • Save content for future reading
  • Receive our member newsletter

When you register to access this directory, you become a member of BNET. In addition, you allow us to share your information with companies that produce products or services featured in the library--so that such companies may contact you with information and offers regarding their products and services. This enables us to keep the library a free service. As a directory registrant, you will receive a complimentary subscription to the BNET member newsletter, The BNET Report. You can unsubscribe from this newsletter at any time. By clicking the Sign up button, you indicate that you agree to our Terms and Conditions and have read and understand our Privacy Policy (updated).