NDLI: Multi-Domain Logic and its Applications to SAT

Content Provider	IEEE Xplore Digital Library
Author	Jebelean, T. Kusper, G.
Copyright Year	2008
Description	Author affiliation: RISC, Linz, Austria (Jebelean, T.)
Abstract	We describe a new formalism and special proof methods for a novel generalization of propositional logic, which is especially suitable for solving the satisfiability problem (SAT). A multi-domain logic (MDL) formula is quantifier-free and contains only atoms of the form x isin A, where x is a variable and A is a constant set. For formulae in conjunctive normal form, we are interested in finding solutions (assignments to variables which satisfy all clauses). Classical propositional logic corresponds to the special case when each set is either {T} or {F}. The union of all the sets occurring for a certain variable can be seen as rdquothe domainrdquo of that variable, thus MDL is also a generalization of multi-valued logic, but with different domains for variables. The most distinctive feature is, however, the indication of the sub-domain in each clause. The notions of resolution, subsumption, as well as the basic steps of the DPLL method generalize in an elegant and straightforward way. As a novel MDL specific technique, variable clustering consists in creating a new variable ranging over the cartesian product of the domains of several rdquoclusteredrdquo variables. This allows the transformation of classical SAT problems in MDL problems with less literals, and in which the propagation of information can be performed more efficiently than classical unit propagation. The basic idea of MDL originates from the earlier work of the second author on rdquohyper-unitrdquo propagation (that is simultaneous propagation of several unit clauses) and on the representation and propagation of rdquok-literalsrdquo (generalized literals containing information on several propositional variables). Preliminary experiments with a prototype Java implementation exhibit speed-ups of up to 30 times.
Starting Page	3
Ending Page	8
File Size	191392
Page Count	6
File Format	PDF
ISBN	9780769535234
DOI	10.1109/SYNASC.2008.93
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2008-09-26
Publisher Place	Romania
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Java Reduced instruction set computing Boolean functions Scientific computing Prototypes Educational institutions Multivalued logic
Content Type	Text
Resource Type	Article

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

From fuzzy to real sets

Reduced offsets for two-level multi-valued logic minimization

Completeness criteria in many-valued set logic under compositions with Boolean functions

Default Reasoning with Imperfect Information in Multivalued Logics

Reconfigurable multi-processor architecture for streaming applications

Boolean complex logic

Toward Problems for Mathematical Fuzzy Logic

Canonical representation of multivalued logic functions

Notice of Violation of IEEE Publication PrinciplesBoolean Functions for Pair Sharing Analysis

Multi-Domain Logic and its Applications to SAT

Similar Documents

From fuzzy to real sets

Reduced offsets for two-level multi-valued logic minimization

Completeness criteria in many-valued set logic under compositions with Boolean functions

Default Reasoning with Imperfect Information in Multivalued Logics

Reconfigurable multi-processor architecture for streaming applications

Boolean complex logic

Toward Problems for Mathematical Fuzzy Logic

Canonical representation of multivalued logic functions

Notice of Violation of IEEE Publication PrinciplesBoolean Functions for Pair Sharing Analysis

Multi-Domain Logic and its Applications to SAT