检索结果-内蒙古大学图书馆

Satisfiability testing of boolean combinations of pseudo-boolean constraints using local-search techniques

constraints 2007年第3期12卷 345-369页

作者： Liu, Lengning Truszczynski, Miroslaw Univ Kentucky Dept Comp Sci Lexington KY 40506 USA

Some search problems are most directly specified by conjunctions of (sets of) disjunctions of pseudo-boolean (PB) constraints. We study a logic PLPB whose formulas are of such form, and design local-search methods to compute models of PLPB theories. In our approach we view a PLPB theory T as a data structure, a concise representation of a certain propositional conjunctive normal form (CNF) theory cl(T) logically equivalent to T. The key idea is an observation that parameters needed by local-search algorithms for CNF theories, such as walksat, can be estimated on the basis of T without the need to compute cl(T) explicitly. We compare our methods to a local-search algorithm wsat(oip). The experiments demonstrate that our approach performs better. In order for wsat(oip) to handle arbitrary PLPB theories, it is necessary to represent disjunctions of PB constraints by sets of PB constraints, which often increases the size of the theory dramatically. A better performance of our method underscores the importance of developing solvers that work directly on PLPB theories.

关键词： pseudo-boolean constraints stochastic local search boolean satisfiability

来源：评论

学校读者我要写书评

暂无评论

N-level Modulo-Based CNF encodings of pseudo-boolean constraints for MaxSAT

引用

constraints 2019年第2期24卷 133-161页

作者： Zha, Aolong Koshimura, Miyuki Fujita, Hiroshi Kyushu Univ Fukuoka Fukuoka 8190395 Japan

Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is NP-hard, more and more practical problems may be solved due to the significant effort which has been devoted to the development of efficient solvers. The art of constraints encoding is as important as the art of devising algorithms for MaxSAT. In this paper, we present several encoding methods of pseudo-boolean constraints into boolean satisfiability problems in Conjunctive Normal Form (CNF) formula, which are based on the idea of modular arithmetic and only generate auxiliary variables for each unique combination of weights. These techniques are efficient in encoding and solving MaxSAT problems. In particular, our solvers won the partial MaxSAT industrial category from 2010 through 2012 and ranked second in the 2017 main weighted track of the MaxSAT evaluation. We prove the correctness and the pseudo-polynomial space complexity of our encodings and also give a heuristics of the base selection for modular arithmetic. Our experimental results show that our encoding compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-the-art SAT solver.

关键词： MaxSAT pseudo-boolean constraints Encoding Modular arithmetic

来源：评论

学校读者我要写书评

暂无评论

Compiling pseudo-boolean constraints to SAT with Order Encoding

Compiling Pseudo-Boolean Constraints to SAT with Order Encod...

引用

25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI)

作者： Tamura, Naoyuki Banbara, Mutsunori Soh, Takehide Kobe Univ Informat Sci & Technol Ctr Nada Ku 1-1 Rokkodai Kobe Hyogo 6578501 Japan

ISBN: (纸本)9781479929719

This paper presents a SAT-based pseudo-boolean (PB for short) solver named PBSugar. PBSugar translates a PB instance to a SAT instance by using the order encoding, and searches its solution by using an external SAT solver, such as Glucose. We first introduce an optimized version of the order encoding, and it is applied to encode each PB constraint a(1)x(1)+ ... a(n)x(n) # k. The encoding is reformulated as a sparse boolean matrix, named Counter Matrix, of size n x (k + 1) constructed for each PB constraint. The same Counter Matrix can be used for any relations >=, <=, =, and not equal and can be reused for other PB constraints having common sub-terms. The experimental results for 669 instances of DEC-SMALLINT-LIN category (decision problems, small integers, linear constraints) demonstrates the superior performance of PBSugar compared to other state-of-the-art PB solvers in terms of the number of solved instances within the given time limit.

关键词： pseudo-boolean constraints SAT encoding Order encoding

来源：评论

学校读者我要写书评

暂无评论

SAT encodings for pseudo-boolean constraints together with at-most-one constraints

引用

ARTIFICIAL INTELLIGENCE 2022年 302卷 103604-103604页

作者： Bofill, Miquel Coll, Jordi Nightingale, Peter Suy, Josep Ulrich-Oltean, Felix Villaret, Mateu Univ Girona Girona Spain Aix Marseille Univ Univ Toulon LIS CNRS Marseille France Univ York York N Yorkshire England

When solving a combinatorial problem using propositional satisfiability (SAT), the encoding of the problem is of vital importance. We study encodings of pseudo-boolean (PB) constraints, a common type of arithmetic constraint that appears in a wide variety of combinatorial problems such as timetabling, scheduling, and resource allocation. In some cases PB constraints occur together with at-most-one (AMO) constraints over subsets of their variables (forming PB(AMO) constraints). Recent work has shown that taking account of AMOs when encoding PB constraints using decision diagrams can produce a dramatic improvement in solver efficiency. In this paper we extend the approach to other state-of-the-art encodings of PB constraints, developing several new encodings for PB(AMO) constraints. Also, we present a more compact and efficient version of the popular Generalized Totalizer encoding, named Reduced Generalized Totalizer. This new encoding is also adapted for PB(AMO) constraints for a further gain. Our experiments show that the encodings of PB(AMO) constraints can be substantially smaller than those of PB constraints. PB(AMO) encodings allow many more instances to be solved within a time limit, and solving time is improved by more than one order of magnitude in some cases. We also observed that there is no single overall winner among the considered encodings, but efficiency of each encoding may depend on PB(AMO) characteristics such as the magnitude of coefficient values. (C) 2021 Published by Elsevier B.V.

关键词： pseudo-boolean constraints Encoding At-most-one constraints SAT

来源：评论

学校读者我要写书评

暂无评论

Learning to select SAT encodings for pseudo-boolean and linear integer constraints

引用

constraints 2023年第3期28卷 397-426页

作者： Ulrich-Oltean, Felix Nightingale, Peter Walker, James Alfred Univ York Dept Comp Sci Deramore Lane York YO10 5GH England

Many constraint satisfaction and optimisation problems can be solved effectively by encoding them as instances of the boolean Satisfiability problem (SAT). However, even the simplest types of constraints have many encodings in the literature with widely varying performance, and the problem of selecting suitable encodings for a given problem instance is not trivial. We explore the problem of selecting encodings for pseudo-boolean and linear constraints using a supervised machine learning approach. We show that it is possible to select encodings effectively using a standard set of features for constraint problems;however we obtain better performance with a new set of features specifically designed for the pseudo-boolean and linear constraints. In fact, we achieve good results when selecting encodings for unseen problem classes. Our results compare favourably to AutoFolio when using the same feature set. We discuss the relative importance of instance features to the task of selecting the best encodings, and compare several variations of the machine learning method.

关键词： Constraint programming SAT encodings Machine learning Global constraints pseudo-boolean constraints Linear constraints

来源：评论

学校读者我要写书评

暂无评论

pseudo-boolean optimisation for RobinX sports timetabling

引用

JOURNAL OF SCHEDULING 2022年第3期25卷 287-299页

作者： Lester, Martin Mariusz Univ Reading Dept Comp Sci Reading Berks England

We report on the development of Reprobate, a tool for solving sports timetabling problems in a subset of the RobinX format. Our tool is based around a monolithic translation of a sports timetabling instance into a pseudo-boolean (PB) optimisation problem;this instance can be solved using existing pseudo-boolean solvers. Once the tool has found a feasible solution, it can improve it using a second encoding that alters only the home/away pattern of games. We entered our tool into the International Timetabling Competition 2021. While it was effective on many instances, it struggled to cope with schedules involving large break constraints. However, among instances for which it could initially find a feasible solution, the combination of use of a portfolio of solvers, a range of variations on the encoding and the aforementioned local improvement process yielded an average reduction in solution cost of 23%.

关键词： pseudo-boolean constraints Sports timetabling International Timetabling Competition RobinX

来源：评论

学校读者我要写书评

暂无评论

Tools for modeling and solving search problems

引用

AI COMMUNICATIONS 2006年第4期19卷 301-312页

作者： East, Deborah Iakhiaev, Mikhail Mikitiuk, Artur Truszczynski, Miroslaw SW Texas State Univ Dept Comp Sci San Marcos TX 78666 USA Univ Texas Dept Comp Sci Austin TX 78712 USA Univ Texas Dept Comp Sci Tyler TX 75799 USA Univ Kentucky Dept Comp Sci Lexington KY 40506 USA

In this paper, we describe a language PSpb to model search problems that are specified in terms of boolean combinations of pseudo-boolean constraints. We then describe software tools that allow one to use SAT and SAT(... 详细信息

关键词： SAT pseudo-boolean constraints grounder

来源：评论

学校读者我要写书评

暂无评论

Predicate-calculus-based logics for modeling and solving search problems

引用

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC 2006年第1期7卷 38-83页

作者： East, Deborah Truszczynski, Miroslaw Texas State Univ San Marcos Dept Comp Sci San Marcos TX 78666 USA Univ Kentucky Dept Comp Sci Lexington KY 40506 USA

The answer-set programming (ASP) paradigm is a way of using logic to solve search problems. Given a search problem, to solve it one designs a logic theory so that models of this theory represent problem solutions. To compute a solution to the problem, one computes a model of the theory. Several answer-set programming formalisms have been developed on the basis of logic programming with the semantics of answer sets. In this article we show that predicate logic also gives rise to effective implementations of the ASP paradigm, similar in spirit to logic programming with the answer-set semantics and with a similar scope of applicability. Specifically, we propose two logics based on predicate calculus as formalisms for encoding search problems. We show that the expressive power of these logics is given by the class NPMV. We demonstrate their use in programming and discuss computational approaches to model finding. To address this latter issue, we follow a two-pronged approach. On the one hand, we show that the problem can be reduced to that of computing models of propositional theories and, more generally, of collections of pseudo-boolean constraints. Consequently, programs (solvers) developed in the areas of propositional and pseudo-boolean satisfiability can be used to compute models of theories in our logics. On the other hand, we develop native solvers designed specifically to exploit features of our formalisms. We present experimental results demonstrating the computational effectiveness of the overall approach.

关键词： theory language satisfiability pseudo-boolean constraints predicate logic search problems constraints

来源：评论

学校读者我要写书评

暂无评论

An Efficient Obstacle-Avoiding Rectilinear Steiner Tree Construction Method Using PB-SAT

引用

IETE JOURNAL OF RESEARCH 2023年第6期69卷 3346-3356页

作者： Kundu, Sudeshna Roy, Suchismita Mukherjee, Shyamapada Natl Inst Technol Durgapur India Natl Inst Technol Comp Sci & Engn Durgapur India Natl Inst Technol Silchar India

Rectilinear Steiner tree (RST) construction is an important part of recent VLSI physical design. This article presents an efficient satisfiability (SAT) based approach to construct an obstacle-avoiding Rectilinear Steiner tree for a given set of pins in the presence of a given set of rectilinear obstacles. Initially, a spanning tree is generated without considering the obstacles and the net is decomposed into 2-pin sub-nets. Then, the RST is constructed for each subnet considering obstacles. RST is generated by applying a pseudo-boolean (PB) SAT-based technique. The proposed technique has been verified on several benchmark circuits. The results indicate that the proposed technique is able to produce a shorter wire length than other state-of-the-art RST tools in many cases.

关键词： Physical design Rectilinear Steiner tree Global routing Obstacle pseudo-boolean satisfiability pseudo-boolean constraints

来源：评论

学校读者我要写书评

暂无评论

Constrained pseudo-Propositional Logic

引用

LOGICA UNIVERSALIS 2020年第4期14卷 523-535页

作者： Azizi-Sultan, Ahmad-Saher Taibah Univ POB 30098 Medina Munawarah Saudi Arabia

Propositional logic, with the aid of SAT solvers, has become capable of solving a range of important and complicated problems. Expanding this range, to contain additional varieties of problems, is subject to the complexity resulting from encoding counting constraints in conjunctive normal form (CNF). Due to the limitation of the expressive power of propositional logic, generally, such an encoding increases the numbers of variables and clauses excessively. This work eliminates the indicated drawback by interpolating constraint symbols and the set of natural numbers N into the alphabet of propositional logic and adjusting the underlying language accordingly. In the extended logic counting constraints are naturally formulated, while many important aspects, such as boolean nature and the soundness and completeness theorems, are kept preserved.

关键词： Propositional logic Proof system pseudo-boolean constraints SAT

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：