Open Access. Powered by Scholars. Published by Universities.®

Physical Sciences and Mathematics Commons

Open Access. Powered by Scholars. Published by Universities.®

Computer Sciences

University of Nebraska at Omaha

Propositional satisfiability

Articles 1 - 7 of 7

Full-Text Articles in Physical Sciences and Mathematics

What Is Answer Set Programming To Propositional Satisfiability, Yuliya Lierler Dec 2016

What Is Answer Set Programming To Propositional Satisfiability, Yuliya Lierler

Computer Science Faculty Publications

Propositional satisfiability (or satisfiability) and answer set programming are two closely related subareas of Artificial Intelligence that are used to model and solve difficult combinatorial search problems. Satisfiability solvers and answer set solvers are the software systems that find satisfying interpretations and answer sets for given propositional formulas and logic programs, respectively. These systems are closely related in their common design patterns. In satisfiability, a propositional formula is used to encode problem specifications in a way that its satisfying interpretations correspond to the solutions of the problem. To find solutions to a problem it is then sufficient to use a …


Integration Schemas For Constraint Answer Set Programming: A Case Study, Marcello Balduccini, Yuliya Lierler Jul 2013

Integration Schemas For Constraint Answer Set Programming: A Case Study, Marcello Balduccini, Yuliya Lierler

Computer Science Faculty Publications

Recently, researchers in answer set programming and constraint programming spent significant efforts in the development of hybrid languages and solving algorithms combining the strengths of these traditionally separate fields. These efforts resulted in a new research area: constraint answer set programming (CASP). CASP languages and systems proved to be largely successful at providing efficient solutions to problems involving hybrid reasoning tasks, such as scheduling problems with elements of planning. Yet, the development of CASP systems is difficult, requiring non-trivial expertise in multiple areas. This suggests a need for a study identifying general development principles of hybrid systems. Once these principles …


Parsing Combinatory Categorial Grammar With Answer Set Programming: Preliminary Report, Yuliya Lierler, Peter Schüller Jan 2011

Parsing Combinatory Categorial Grammar With Answer Set Programming: Preliminary Report, Yuliya Lierler, Peter Schüller

Computer Science Faculty Proceedings & Presentations

Combinatory categorial grammar (CCG) is a grammar formalism used for natural language parsing. CCG assigns structured lexical categories to words and uses a small set of combinatory rules to combine these categories to parse a sentence. In this work we propose and implement a new approach to CCG parsing that relies on a prominent knowledge representation formalism, answer set programming (ASP) — a declarative programming paradigm. We formulate the task of CCG parsing as a planning problem and use an ASP computational tool to compute solutions that correspond to valid parses. Compared to other approaches, there is no need to …


Sat-Based Answer Set Programming, Yuliya Lierler May 2010

Sat-Based Answer Set Programming, Yuliya Lierler

Computer Science Faculty Publications

Answer set programming (ASP) is a declarative programming paradigm oriented towards difficult combinatorial search problems. Syntactically, ASP programs look like Prolog programs, but solutions are represented in ASP by sets of atoms, and not by substitutions, as in Prolog. Answer set systems, such as SMODELS, SMODELSCC, and DLV, compute answer sets of a given program in the sense of the answer set (stable model) semantics. This is different from the functionality of Prolog systems, which determine when a given query is true relative to a given logic program. ASP has been applied to many areas of science and technology, from …


Experiments With Sat-Based Answer Set Programming, Enrico Giunchiglia, Yuliya Lierler, Marco Maratea, A. Tacchella Jan 2006

Experiments With Sat-Based Answer Set Programming, Enrico Giunchiglia, Yuliya Lierler, Marco Maratea, A. Tacchella

Computer Science Faculty Proceedings & Presentations

Answer Set Programming (ASP) emerged in the late 1990s as a new logic programming paradigm which has been successfully applied in various application domains. Propositional satisfiability (SAT) is one of the most studied problems in Computer Science. ASP and SAT are closely related: Recent works have studied their relation, and efficient SAT-based ASP solvers (like assat and Cmodels) exist. In this paper we report about (i) the extension of the basic procedures in Cmodels in order to incorporate the most popular SAT reasoning strategies, and (ii) an extensive comparative analysis involving also other state-of-the-art answer set solvers. The experimental analysis …


Disjunctive Answer Set Programming Via Satisfiability, Yuliya Lierler Jan 2005

Disjunctive Answer Set Programming Via Satisfiability, Yuliya Lierler

Computer Science Faculty Proceedings & Presentations

Using SAT solvers as inference engines in answer set programming systems showed to be a promising approach in building efficient systems. Nowadays SAT based answer set programming systems successfully work with nondisjunctive programs. This paper proposes a way to use SAT solvers for finding answer sets for disjunctive logic programs. We implement two different ways of SAT solver invocation used in nondisjunctive answer set programming. The algorithms are based on the definition of completion for disjunctive programs and the extension of loop formula to the disjunctive case. We propose the necessary modifications to the algorithms known for nondisjunctive programs in …


Sat-Based Answer Set Programming, Enrico Giunchiglia, Yuliya Lierler, Marco Maratea Jan 2004

Sat-Based Answer Set Programming, Enrico Giunchiglia, Yuliya Lierler, Marco Maratea

Computer Science Faculty Proceedings & Presentations

The relation between answer set programming (ASP) and propositional satisfiability (SAT) is at the center of many research papers, partly because of the tremendous performance boost of SAT solvers during last years. Various translations from ASP to SAT are known but the resulting SAT formula either includes many new variables or may have an unpractical size. There are also well known results showing a one-to-one correspondence between the answer sets of a logic program and the models of its completion. Unfortunately, these results only work for specific classes of problems. In this paper we present a SAT-based decision procedure for …