Multiple Query Satisfiability of Constrained Horn Clauses

• URL: http://arxiv.org/abs/2211.15207v2
• Date: Thu, 11 Jan 2024 21:55:46 GMT
• Title: Multiple Query Satisfiability of Constrained Horn Clauses
• Abstract summary: We propose a technique that takes as input a set of CHCs, including a set of queries, and returns as output a new set of CHCs. The transformed CHCs incorporate in each new query suitable information coming from the other ones so that the CHC satisfiability algorithm is able to exploit the relationships among all queries.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We address the problem of checking the satisfiability of a set of constrained Horn clauses (CHCs) possibly including more than one query. We propose a transformation technique that takes as input a set of CHCs, including a set of queries, and returns as output a new set of CHCs, such that the transformed CHCs are satisfiable if and only if so are the original ones, and the transformed CHCs incorporate in each new query suitable information coming from the other ones so that the CHC satisfiability algorithm is able to exploit the relationships among all queries. We show that our proposed technique is effective on a non trivial benchmark of sets of CHCs that encode many verification problems for programs manipulating algebraic data types such as lists and trees.

Related papers

• CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses [0.0]
  Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for verification tasks.<n>This paper introduces a portfolio-based CHC solver that adopts a software verification approach for solving CHCs.
  arXiv  Detail & Related papers  (2025-10-30T12:25:06Z)
• The benefits of query-based KGQA systems for complex and temporal questions in LLM era [55.20230501807337]
  Large language models excel in question-answering (QA) yet still struggle with multi-hop reasoning and temporal questions.<n> Query-based knowledge graph QA (KGQA) offers a modular alternative by generating executable queries instead of direct answers.<n>We explore multi-stage query-based framework for WikiData QA, proposing multi-stage approach that enhances performance on challenging multi-hop and temporal benchmarks.
  arXiv  Detail & Related papers  (2025-07-16T06:41:03Z)
• Transformers for Complex Query Answering over Knowledge Hypergraphs [48.55646194244594]
  Triple KGs, as the classic KGs composed of entities and relations of arity 2, have limited representation of real-world facts. We propose a two-stage transformer model, the Logical Knowledge Hypergraph Transformer (LKHGT), which consists of a Projection for atomic projection and a Logical for complex logical operations. Experimental results on CQA datasets show that LKHGT is a state-of-the-art CQA method over KHG and is able to generalize to out-of-distribution query types.
  arXiv  Detail & Related papers  (2025-04-23T09:07:21Z)
• Zero-Shot and Efficient Clarification Need Prediction in Conversational Search [7.791642719869652]
  We propose a zero-shot and efficient CNP framework (Zef-CNP) We first prompt large language models (LLMs) in a zero-shot manner to generate two sets of synthetic queries. We then use the generated queries to train efficient CNP models.
  arXiv  Detail & Related papers  (2025-02-28T20:49:18Z)
• Improving Scientific Document Retrieval with Concept Coverage-based Query Set Generation [49.29180578078616]
  Concept Coverage-based Query set Generation (CCQGen) framework designed to generate a set of queries with comprehensive coverage of the document's concepts. We identify concepts not sufficiently covered by previous queries, and leverage them as conditions for subsequent query generation. This approach guides each new query to complement the previous ones, aiding in a thorough understanding of the document.
  arXiv  Detail & Related papers  (2025-02-16T15:59:50Z)
• Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification [0.09786690381850355]
  Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA.
  arXiv  Detail & Related papers  (2024-04-23T16:46:27Z)
• Matching Game for Optimized Association in Quantum Communication Networks [65.16483325184237]
  This paper proposes a swap-stable request-QS association algorithm for quantum switches. It achieves a near-optimal (within 5%) performance in terms of the percentage of served requests. It is shown to be scalable and maintain its near-optimal performance even when the size of the QCN increases.
  arXiv  Detail & Related papers  (2023-05-22T03:39:18Z)
• NQE: N-ary Query Embedding for Complex Query Answering over Hyper-Relational Knowledge Graphs [1.415350927301928]
  Complex query answering is an essential task for logical reasoning on knowledge graphs. We propose a novel N-ary Query Embedding (NQE) model for CQA over hyper-relational knowledge graphs (HKGs) NQE utilizes a dual-heterogeneous Transformer encoder and fuzzy logic theory to satisfy all n-ary FOL queries. We generate a new CQA dataset WD50K-NFOL, including diverse n-ary FOL queries over WD50K.
  arXiv  Detail & Related papers  (2022-11-24T08:26:18Z)
• Multi-Type Conversational Question-Answer Generation with Closed-ended and Unanswerable Questions [3.6825890616838066]
  Conversational question answering (CQA) facilitates an incremental and interactive understanding of a given context. We introduce a novel method to synthesize data for CQA with various question types, including open-ended, closed-ended, and unanswerable questions. Across four domains, CQA systems trained on our synthetic data indeed show good performance close to the systems trained on human-annotated data.
  arXiv  Detail & Related papers  (2022-10-24T07:01:51Z)
• PACIFIC: Towards Proactive Conversational Question Answering over Tabular and Textual Data in Finance [96.06505049126345]
  We present a new dataset, named PACIFIC. Compared with existing CQA datasets, PACIFIC exhibits three key features: (i) proactivity, (ii) numerical reasoning, and (iii) hybrid context of tables and text. A new task is defined accordingly to study Proactive Conversational Question Answering (PCQA), which combines clarification question generation and CQA. UniPCQA performs multi-task learning over all sub-tasks in PCQA and incorporates a simple ensemble strategy to alleviate the error propagation issue in the multi-task learning by cross-validating top-$k$ sampled Seq2Seq
  arXiv  Detail & Related papers  (2022-10-17T08:06:56Z)
• Bayes risk CTC: Controllable CTC alignment in Sequence-to-Sequence tasks [63.189632935619535]
  Bayes risk CTC (BRCTC) is proposed to enforce the desired characteristics of the predicted alignment. By using BRCTC with another preference for early emissions, we obtain an improved performance-latency trade-off for online models.
  arXiv  Detail & Related papers  (2022-10-14T03:55:36Z)
• Satisfiability and Containment of Recursive SHACL [4.8986598953553555]
  The Shapes Constraint Language (SHACL) is the recent W3C recommendation language for validating RDF data, by verifying certain shapes on graphs. Previous work has largely focused on the validation problem and the standard decision problems of satisfiability and containment. We provide a comprehensive study of the different features of SHACL, by providing a translation to a new first-order language, called SCL, that precisely captures the semantics of SHACL. We also present MSCL, a second-order extension of SCL, which allows us to define, in a single formal logic framework, the main
  arXiv  Detail & Related papers  (2021-08-30T08:51:03Z)
• An Efficient Diagnosis Algorithm for Inconsistent Constraint Sets [68.8204255655161]
  We introduce a divide-and-conquer based diagnosis algorithm (FastDiag) which identifies minimal sets of faulty constraints in an over-constrained problem. We compare FastDiag with the conflict-directed calculation of hitting sets and present an in-depth performance analysis.
  arXiv  Detail & Related papers  (2021-02-17T19:55:42Z)
• Generating Diverse and Consistent QA pairs from Contexts with Information-Maximizing Hierarchical Conditional VAEs [62.71505254770827]
  We propose a conditional variational autoencoder (HCVAE) for generating QA pairs given unstructured texts as contexts. Our model obtains impressive performance gains over all baselines on both tasks, using only a fraction of data for training.
  arXiv  Detail & Related papers  (2020-05-28T08:26:06Z)
• Query Resolution for Conversational Search with Limited Supervision [63.131221660019776]
  We propose QuReTeC (Query Resolution by Term Classification), a neural query resolution model based on bidirectional transformers. We show that QuReTeC outperforms state-of-the-art models, and furthermore, that our distant supervision method can be used to substantially reduce the amount of human-curated data required to train QuReTeC.
  arXiv  Detail & Related papers  (2020-05-24T11:37:22Z)
• XCSP3: An Integrated Format for Benchmarking Combinatorial Constrained Problems [3.149883354098941]
  The new format is made compact, highly readable, and rather easy to parse. XCSP3 encompasses practically all constraints that can be found in major constraint solvers. The user can make sophisticated queries for selecting instances from very precise criteria.
  arXiv  Detail & Related papers  (2016-11-10T17:00:56Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.