Boolean Satisfiability
URI permanente para esta colección:
Artículos en la categoría Boolean Satisfiability publicados en las Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019).
Notificar un error en esta colección
Examinar
Envíos recientes
Artículo Satisfiability Solvers based on Resolution and Cutting Planes Proof SystemsBonet, Maria Luisa. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.Satisfiability (SAT) is the canonical NP-Complete problem. Many other interesting and practical problems can be encoded into SAT. This is why it is important from a theoretical and practical point of view. Nowadays there are very good algorithms to solve SAT, the best from the point of view of industrial instances can be shown equivalent to the proof system Resolution. We will present the algorithm, and the equivalence to Resolution. Other proof systems are more powerful than Resolution, and still might be amenable to finding refutation algorithms, like Cutting Planes. We will talk about posible ways to automatize Cutting Planes. Also we will present the dual-rail encoding of formulas, to be then refuted using MaxSAT algorithms, as another methodology for SAT more powerful than Resolution.Artículo SMT-based Test-Case Generation with Complex PreconditionsPeña Marí, Ricardo; Sánchez-Hernández, Jaime; Garrido, Miguel; Sagredo, Javier. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.We present a system which can automatically generate an exhaustive set of black-box test-cases, up to a given size, for programs under test requiring complex preconditions. The key of the approach is to translate a formal precondition into a set of constraints belonging to the decidable logics of SMT solvers. By checking the satisfiability of the constraints, then the models returned by the solver automatically synthesize the cases. We also show how to use SMT solvers to automatically check for validity the test-case results, and also to complement the black-box cases with white-box ones. Finally, we use of solver to perform what we call automatic partial verification of the program. In summary, we propose a system in which exhaustive black-box and white-box testing, result checking, and partial verification, can all be done automatically. The only extra effort required from programmers is to write formal specifications.Artículo infChecker: A Tool for Checking InfeasibilityGutiérrez, Raúl; Lucas, Salvador. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.Given a CTRS R and terms s and t, we say that the reachability condition s = t is feasible if there is a substitution sigma instantiating the variables in s and t such that the reachability test sigma(s) ->*R sigma(t) succeeds; otherwise, we call it infeasible. Given a sequence of reachability conditions (s1 = t1),...,(sn = tn), where n > 0, we say that the sequence is R-feasible if there is a substitution such that all the reachability tests sigma(si) ->*R sigma(ti) are satised. In [5, 6] we presented an approach to deal with infeasibility using a semantic criterion. In this paper we present infChecker, a new tool for checking infeasibility conditions of CTRSs based on this approach. We succesfully participated in the 2019 Confuence Competition in the INF (infeasibility) category, being the most powerful tool for checking both infeasibility and feasibility.