LOGPROG - Lògica i Programació: Enviaments recents

Ara es mostren els items 1-12 de 67

    • Efficient deduction in equality Horn logic by Horn-completion 

      Nieuwenhuis, Robert Lukas Mario; Nivela Alós, M. Pilar Brígida (1991)
      Report de recerca
      Accés obert
      We present a new unfailing completion procedure for Horn clauses with equality, including goal clauses. It is refutationally complete, and improves previous methods in that superpositions are computed only with unconditional ...

    • An implementation of the KNS ordering 

      Rivero Almeida, José Miguel (1991-04)
      Report de recerca
      Accés obert
      We describe an implementation of the KNS ordering within the TRIP system, a Quintus-Prolog written laboratory for experimenting with new rewrite-like approaches to theorem proving in first-order logic. The aim of the TRIP ...

    • Automatic generation of polynomial loop invariants for imperative programs 

      Rodríguez Carbonell, Enric; Kapur, Deepak (2003-11)
      Report de recerca
      Accés obert
      A general framework is presented for automatig the discovery of loop invariants for imperative programs. Theoretical results about the correctness and completeness of the proposed method are given. More importantly, it is ...

    • Choosing the root of the tree decomposition when solving WCSPs: preliminary results 

      Petrova, Aleksandra; Larrosa Bondia, Francisco Javier; Rollón Rico, Emma (IOS Press, 2021)
      Text en actes de congrés
      Accés obert
      In this paper we analyze the effect of selecting the root in a tree decomposition when using decomposition-based backtracking algorithms. We focus on optimization tasks for Graphical Models using the BTD algorithm. We show ...

    • Employee scheduling with SAT-based pseudo-boolean constraint solving 

      Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rollón Rico, Emma (Institute of Electrical and Electronics Engineers (IEEE), 2021)
      Article
      Accés obert
      The aim of this paper is practical: to show that, for at least one important real-world problem, modern SAT-based technology can beat the extremely mature branch-and-cut solving methods implemented in well-known state-of-the-art ...

    • A heuristic approach to the design of optimal cross-docking boxes 

      Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Institute of Electrical and Electronics Engineers (IEEE), 2021-09-03)
      Article
      Accés obert
      Multinational companies frequently work with manufacturers that receive large orders for different products (or product varieties: size, shape, color, texture, material), to serve thousands of different final destinations ...

    • Stuck-at-off fault analysis in memristor-based architecture for synchronization 

      Escudero, Manuel; Vourkas, Ioannis; Rubio Gimeno, Alberto (Institute of Electrical and Electronics Engineers (IEEE), 2019)
      Text en actes de congrés
      Accés restringit per política de l'editorial
      Nonlinear circuits may be interconnected and organized in networks to couple their dynamics and achieve synchronization, a process that is commonly observed in nature. Recent works have shown that memristors may be used ...

    • Decision levels are stable: towards better SAT heuristics 

      Nieuwenhuis, Robert Lukas Mario; Lozano Navarro, Adrián; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (EasyChair Publications, 2020)
      Text en actes de congrés
      Accés restringit per política de l'editorial
      We shed new light on the Literal Block Distance (LBD) and glue-based heuristics used in current SAT solvers. For this, we first introduce the concept of stickiness: given a run of a CDCL SAT solver, for each pair of literals ...

    • First-order completion with ordering constraints: some positive and some negative results 

      Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto (1991-10-15)
      Report de recerca
      Accés obert
      We show by means of counter examples that some well-known results on the completeness of deduction methods with ordering constraints are incorrect. The problem is caused by the fact that the usual lifting lemmata do not ...

    • Basic superposition is complete 

      Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto (1991-10-15)
      Report de recerca
      Accés obert
      We define a formalism of equality constraints and use it to prove the completeness of what we have called basic superposition: a restricted form of superposition in which only the subterms not originated in previous ...

    • Augmenting the power of (partial) MaxSat resolution with extension 

      Larrosa Bondia, Francisco Javier; Rollón Rico, Emma (AAAI Press, 2020)
      Comunicació de congrés
      Accés restringit per política de l'editorial
      The refutation power of SAT and MaxSAT resolution is challenged by problems like the soft and hard Pigeon Hole Problem PHP for which short refutations do not exist. In this paper we augment the MaxSAT resolution proof ...

    • On one query self-reducible sets 

      Lozano Boixadors, Antoni; Ogiwara, Mitsunori (1991-01)
      Report de recerca
      Accés obert
      We study one word-decreasing self-reducible sets, which were introduced by Lozano and Torán. These are usual self-reducible sets with the peculiarity that the self-reducibility machine makes at most one query and this is ...