NDLI: Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings

Content Provider	Springer Nature Link
Author	Frisch, Alan M. Peugniez, Timothy J. Doggett, Anthony J. Nightingale, Peter W.
Copyright Year	2006
Abstract	Much excitement has been generated by the success of stochastic local search procedures at finding solutions to large, very hard satisfiability problems. Many of the problems on which these procedures have been effective are non-Boolean in that they are most naturally formulated in terms of variables with domain sizes greater than two. Approaches to solving non-Boolean satisfiability problems fall into two categories. In the direct approach, the problem is tackled by an algorithm for non-Boolean problems. In the transformation approach, the non-Boolean problem is reformulated as an equivalent Boolean problem and then a Boolean solver is used.This paper compares four methods for solving non-Boolean problems: one direct and three transformational. The comparison first examines the search spaces confronted by the four methods, and then tests their ability to solve random formulas, the round-robin sports scheduling problem, and the quasigroup completion problem. The experiments show that the relative performance of the methods depends on the domain size of the problem and that the direct method scales better as domain size increases.Along the route to performing these comparisons we make three other contributions. First, we generalize Walksat, a highly successful stochastic local search procedure for Boolean satisfiability problems, to work on problems with domains of any finite size. Second, we introduce a new method for transforming non-Boolean problems to Boolean problems and improve on an existing transformation. Third, we identify sufficient conditions for omitting at-least-one and at-most-one clauses from a transformed formula. Fourth, for use in our experiments we propose a model for generating random formulas that vary in domain size but are similar in other respects.
Starting Page	143
Ending Page	179
Page Count	37
File Format	PDF
ISSN	01687433
Journal	Journal of Automated Reasoning
Volume Number	35
Issue Number	1-3
e-ISSN	15730670
Language	English
Publisher	Springer Netherlands
Publisher Date	2006-01-19
Publisher Place	Dordrecht
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	satisfiability propositional logic local search encodings Symbolic and Algebraic Manipulation Mathematical Logic and Foundations Artificial Intelligence (incl. Robotics) Mathematical Logic and Formal Languages
Content Type	Text
Resource Type	Article
Subject	Artificial Intelligence Computational Theory and Mathematics Software

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

Boolean Functions as Models for Quantified Boolean Formulas

Clause Weighting Local Search for SAT

Answer Set Programming Based on Propositional Satisfiability

Symbolic Techniques in Satisfiability Solving

An Experiment with Satisfiability Modulo SAT

Heuristic-Based Backtracking Relaxation for Propositional Satisfiability

Stochastic Boolean Satisfiability

An Efficient Approach to Solving Random k-sat Problems

Axiomatizing the Skew Boolean Propositional Calculus

Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings

Similar Documents

Boolean Functions as Models for Quantified Boolean Formulas

Clause Weighting Local Search for SAT

Answer Set Programming Based on Propositional Satisfiability

Symbolic Techniques in Satisfiability Solving

An Experiment with Satisfiability Modulo SAT

Heuristic-Based Backtracking Relaxation for Propositional Satisfiability

Stochastic Boolean Satisfiability

An Efficient Approach to Solving Random k-sat Problems

Axiomatizing the Skew Boolean Propositional Calculus

Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings