NDLI: Solution and Optimization of Systems of Pseudo-Boolean Constraints

Content Provider	IEEE Xplore Digital Library
Author	Aloul, F.A. Ramani, A. Sakallah, K.A. Markov, I.L.
Copyright Year	1968
Abstract	Optimized solvers for the Boolean satisfiability (SAT) problem have many applications in areas such as hardware and software verification, FPGA routing, planning, and so forth. Further uses are complicated by the need to express "counting constraints" in conjunctive normal form (CNF). Expressing such constraints by pure CNF leads to more complex SAT instances. Alternatively, those constraints can be handled by integer linear programming (ILP), but generic ILP solvers may ignore the Boolean nature of 0-1 variables. Therefore, specialized 0-1 ILP solvers extend SAT solvers to handle these so-called "pseudo-Boolean" (PB) constraints. This work provides an update on the on-going competition between generic ILP techniques and specialized 0-1 ILP techniques. To make a fair comparison, we generalize recent ideas for fast SAT-solving to more general 0-1 ILP problems that may include counting constraints and optimization. This generalization is embodied in our PB constraint solver and optimizer PBS, which is compared with state-of-the-art CNF and generic ILP solvers. Another aspect of our comparison is the evaluation on 0-1 ILP benchmarks that originate in electronic design automation (EDA) but that cannot be directly solved by an SAT solver. Specifically, we solve instances of the max-SAT and max-ONEs optimization problems, which seek to maximize the number of satisfied clauses and the "true" values over all satisfying assignments, respectively. Those problems have straightforward applications to SAT-based routing and are additionally important due to reductions from max-cut, max-clique, and min vertex cover. Our experimental results show that specialized 0-1 techniques implemented in PBS tend to outperform generic ILP techniques on Boolean optimization problems, as well as on general EDA SAT problems.
Sponsorship	IEEE Computer Society Technical Committee on Distributed Process IEEE Computer Society Technical Committee on VLSI IEEE Technical Committee on Computer Architecture IEEE Computer Society
File Size	2682489
File Format	PDF
ISSN	00189340
Volume Number	56
Issue Number	10
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2007-10-01
Publisher Place	U.S.A.
Access Restriction	One Nation One Subscription (ONOS)
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Routing Optimization Engines Linear programming Boolean functions Construction industry Data structures Global Routing Boolean Satisfiability (SAT) Integer Linear Programming (ILP) Backtrack Search Conjunctive Normal Form (CNF) Pseudo Boolean (PB) Max-SAT Max-ONE
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Computational Theory and Mathematics Software Hardware and Architecture

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Efficient symmetry breaking for Boolean satisfiability

Optimizing Complex Cluster Formation in MANETs Using SAT/ILP Techniques

Satisfiability Testing of Boolean Combinations of Pseudo-Boolean Constraints using Local-search Techniques

ILP/SMT-Based Method for Design of Boolean Networks Based on Singleton Attractors

A fast pseudo-Boolean constraint solver

Compact Linearization for Binary Quadratic Problems Comprising Linear Constraints

A comparative study of two Boolean formulations of FPGA detailed routing constraints

A new FPGA detailed routing approach via search-based Boolean satisfiability

An Algorithm to Decide Feasibility of Linear Integer Constraints Occurrng in Decision Tables

Solution and Optimization of Systems of Pseudo-Boolean Constraints

Similar Documents

Efficient symmetry breaking for Boolean satisfiability

Optimizing Complex Cluster Formation in MANETs Using SAT/ILP Techniques

Satisfiability Testing of Boolean Combinations of Pseudo-Boolean Constraints using Local-search Techniques

ILP/SMT-Based Method for Design of Boolean Networks Based on Singleton Attractors

A fast pseudo-Boolean constraint solver

Compact Linearization for Binary Quadratic Problems Comprising Linear Constraints

A comparative study of two Boolean formulations of FPGA detailed routing constraints

A new FPGA detailed routing approach via search-based Boolean satisfiability

An Algorithm to Decide Feasibility of Linear Integer Constraints Occurrng in Decision Tables

Solution and Optimization of Systems of Pseudo-Boolean Constraints