skip to main content
10.5555/1015090.1015324acmconferencesArticle/Chapter ViewAbstractPublication PagesaspdacConference Proceedingsconference-collections
Article

Satisfiability and integer programming as complementary tools

Published: 27 January 2004 Publication History

Abstract

Satisfiability (SAT) and integer linear programming (ILP) are two related NP-complete problems. They both have a lot of important applications. We study the effectiveness of using them as a complementary tool to each other. We propose three different ILP formulations to solve SAT and compare them with state-of-the-art SAT solvers Berkmin and zchaff. On the other hand, we give two methods to solve ILP by using SAT solvers. In both cases, we achieve speed-ups of several orders for most of our tested examples.

References

[1]
P. Barth, A Davis-Putnam based Enumeration Algorithm for Linear Pseudo-Boolean Optimization, Technical Report MPI-I-95-2-003, Max-Planck-Institut Fr Informatik, 1995.
[2]
P. Barth, OPBDP: A Davis-Putnam based Enumeration Algorithm for Linear Pseudo-Boolean Optimization, http://www.mpi-sb.mpg.de/units/ag2/software/opbdp.
[3]
H. Xu, R. Rutenbar, K. Sakallah, sub-SAT: A Formulation for Relaxed Boolean Satisfiability with Applications in Routing, in Proc. of the Int'l Symposium on Physical Design, 2002.
[4]
F. Aloul, A. Ramani, I. Markov, and K. Sakallah, Generic ILP versus Specialized 0-1 ILP: an Update, ICCAD 2002.
[5]
E. Goldberg, and Novikov, BerkMin: A Fast and Robust Sat-Solver, 2002 Design, Automation and Test in Europe Conference and Exhibition (DATE'02)
[6]
D. Chai and A. Kuehlmann, A fast pseudo-boolean constraint solver, Proc. of the Design Automation Conference, pp. 830--835, 2003.
[7]
S. Devadas, Optimal layout via boolean satisfiability, IEEE/ACM ICCAD, pp 294--297, 1989.
[8]
R.Wood and R. A. Rutenbar, FPGA routing and routability estimation via boolean satisfiability. IEEE Tran. VLSI, pp. 222--231, June, 1998.
[9]
R. Bayardo, and R. Schrag, Using CSP look-back techniques to solve real-world SAT instances, Proc. of the 14th Na.(US) Conf. on Artificial Intelligence(AAAI-97), AAAI Press/The MIT Press, 1997.
[10]
S.A.Cook, The complexity if theorem proving procedures, Proceedings of 3rd Annual ACM Symposium on the Theory of Computing, New York, 1971, pp:151--158.
[11]
M. Davis, G. Logemann, and D. Loveland, A Machine Program for Theorem Proving, Communications of the ACM, 5(7), pp. 394--397, 1962.
[12]
J. N. Hook, unpublished note.
[13]
http://www.caam.rice.edu/~bixby/miplib/miplib3.html
[14]
http://www.ps.uni-sb.de/~walser/acc/acc.html
[15]
http://www.eecs.umich.edu/~faloul/benchmarks.html
[16]
ILOG CPLEX, http://www.ilog.com/products/cplex
[17]
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: Engineering an Efficient SAT Solver, in Proc. of the Design Automation Conference, pp. 530--535, 2001.
[18]
V. Manquinho, J. Marques-Silva, Search pruning techniques in SAT-based branch-and-bound algorithms for the binate covering problem, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 21(5), pp. 505--516, May 2002.
[19]
J.P. Marques-Silva and K. A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Tranctions on Computers, vol. 48, 506--521, 1999.
[20]
S. Slijepcevic and M. Potkonjak, Power efficient organization of wireless sensor networks. IEEE International Conference on Communications, Vol. 2, pp. 472--476, 2001.
[21]
Joost P. Warners, A linear-time transformation of linear inequlities into conjunctive normal form. Information Processing Letters 68 (1998) 63--69.
[22]
H. Zhang, SATO: an efficient proposition solver, Proceedings of the International Conference on Automated deduction, July 1997.
[23]
L. Zhang, C. Madigan, M. Moskewicz and S. Malik, Efficient conflict driven learning in a Boolean satisfiability solver. IEEE/ACM International Conference on Computer Aided Design, pp. 279--285, 2001.

Cited By

View all
  • (2015)A Constraint Approach to Pivot-Based Bilingual Dictionary InductionACM Transactions on Asian and Low-Resource Language Information Processing10.1145/272314415:1(1-26)Online publication date: 21-Nov-2015
  • (2014)Polyhedral Labellings for Argumentation FrameworksProceedings of the 8th International Conference on Scalable Uncertainty Management - Volume 872010.1007/978-3-319-11508-5_8(86-99)Online publication date: 15-Sep-2014
  • (2012)Answer set programming via mixed integer programmingProceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning10.5555/3031843.3031848(32-42)Online publication date: 10-Jun-2012
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ASP-DAC '04: Proceedings of the 2004 Asia and South Pacific Design Automation Conference
January 2004
957 pages
ISBN:0780381750

Sponsors

Publisher

IEEE Press

Publication History

Published: 27 January 2004

Check for updates

Qualifiers

  • Article

Conference

ASPDAC04
Sponsor:

Acceptance Rates

Overall Acceptance Rate 466 of 1,454 submissions, 32%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)1
  • Downloads (Last 6 weeks)0
Reflects downloads up to 13 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2015)A Constraint Approach to Pivot-Based Bilingual Dictionary InductionACM Transactions on Asian and Low-Resource Language Information Processing10.1145/272314415:1(1-26)Online publication date: 21-Nov-2015
  • (2014)Polyhedral Labellings for Argumentation FrameworksProceedings of the 8th International Conference on Scalable Uncertainty Management - Volume 872010.1007/978-3-319-11508-5_8(86-99)Online publication date: 15-Sep-2014
  • (2012)Answer set programming via mixed integer programmingProceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning10.5555/3031843.3031848(32-42)Online publication date: 10-Jun-2012
  • (2012)Bounded model checking for parametric timed automataTransactions on Petri Nets and Other Models of Concurrency V10.5555/2231056.2231062(141-159)Online publication date: 1-Jan-2012
  • (2007)Solving difficult SAT instances using greedy clique decompositionProceedings of the 7th International conference on Abstraction, reformulation, and approximation10.5555/1770681.1770711(359-374)Online publication date: 18-Jul-2007

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media