"Logic is everywhere!"

Publications

• Tobias Philipp, Valentin Roland, Lukas Schweizer. Smoke Test Planning using Answer Set Programming
  In: Declarative Problem Solving Workshop (2020)

  Smoke testing is an important method to increase stability and reliability of hardware-depending systems. Due to concurrent access to the same physical resource and the impracticality of the use of virtualization, smoke testing requires some form of planning. In this paper, we propose to decompose test cases in terms of atomic actions consisting of preconditions and effects. We present a solution based on answer set programming with multi-shot solving that automatically generates short parallel test plans. Experiments suggest that the approach is feasible for non-inherently sequential test cases and scales up to thousands of test cases.

• Johannes K. Fichte, Markus Hecher, Jakob Rath, Tobias Philipp. Inconsistency Proofs for ASP: The ASP-DRUPE Format
  In: Workshop on Answer Set Programming and Other Computing Paradigms (2019)

  ASP solvers are highly-tuned and complex procedures that implicitly solve the consistency problem, i.e., deciding whether an ASP program admits an answer set. Verifying whether a claimed answer set is formally a correct answer set of the program can be decided in polynomial time for normal programs. However, it is far from immediate to verify whether a program that is claimed to be inconsistent, indeed does not admit any answer sets. In this paper, we address this problem and develop the new proof format ASP-DRUPE for propositional, disjunctive ASP, including weights and optimization. ASP DRUPE is based on the RUP format designed for Boolean satisfiability. We establish correctness of ASP-DRUPE and discuss how to integrate it into modern ASP solvers.

• Emmanuelle-Anna Dietz Saldanha, Steffen Hölldobler, Tobias Philipp. Contextual Abduction and its Complexity Issues
  In: Proceedings of the 4th International Workshop on Defeasible and Ampliative Reasoning (DARe-17), pp. 58–70. CEUR-WS.org (2017)

  In everyday life, it seems that we prefer some explanations for an observation over others because of our contextual background knowledge. Reiter already tried to specify a mechanism within logic that allows us to avoid explicitly considering all exceptions in order to derive a conclusion w.r.t. the usual case. In a recent paper, a contextual reasoning approach has been presented, which takes this contextual background into account and allows us to specify contexts within the logic. This approach is embedded into the Weak Completion Semantics , a Logic Programming approach that aims at adequately modeling human reasoning tasks. As this approach extends the underlying three-valued Łukasiewicz logic, some formal properties of the Weak Completion Semantics do not hold anymore. In this paper, we investigate the effects of this extension and present some surprising results about the complexity issues of contextual abduction.

• Walter Forkel, Tobias Philipp, Elias Werner, Adrian Rebola-Pardo. Fuzzing and Verifying RAT Refutations with Deletion Information
  In: Proceedings of the Thirtieth International Florida Artificial Intelligence Research Society Conference (FLAIRS), AAAI, 2017 (2017)

  Contemporary SAT solvers emit proofs of unsatisfiability in the DRAT format to guarantee correctness of their answers. Therefore, correctness of SAT solvers is reduced to correctness of DRAT checkers, which are relatively small programs that decide whether a DRAT refutation is correct. We present a new fuzzing technique that automatically finds bugs in DRAT checkers by comparing the outputs of two DRAT checkers. In case their outputs are different a mechanically verified DRAT checker finally decides which checker has given the correct answer. Experiments show that our method finds bugs in available checkers, and also demonstrate that a common design choice in efficient DRAT checkers is inconsistent with the specification.

• Emmanuelle-Anna Dietz Saldanha, Steffen Hölldobler, Tobias Philipp. The Complexity of Contextual Abduction in Human Reasoning Tasks
  In: Proceedings of the 2nd Young Scientist’s Second International Workshop on Trends in Information Processing (YSIP), CEUR-WS.org (2017)

  In everyday life, it seems that when we observe something, then, while searching for explanations, we assume some explanation more plausible to others, simply because of our contextual background. Recently, a contextual reasoning approach has been presented, which takes into account this contex-tual background and allows us to specify context within the logic. This approach is embedded into the Weak Completion Semantics, a Logic Programming approach that aims at adequately modeling human reasoning tasks. As this approach extends the underlying three-valued Łukasiewicz logic, some formal properties of the Weak Completion Semantics do not hold anymore. In this paper, we investigate the effects of this extension with respect to former results. In particular, we present some interesting results about the complexity of contextual abduction.

• Tobias Philipp, Adrian Rebola-Pardo. Towards a Semantics of Unsatisfiability Proofs with Inprocessing
  In: Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), EasyChair Publications, 2017 (2017)

  Delete Resolution Asymmetric Tautology (DRAT) proofs have become a de facto standard to certify unsatisfiability results from SAT solvers with inprocessing. However, DRAT shows behaviors notably different from other proof systems: DRAT inferences are non- monotonic, and clauses that are not consequences of the premises can be derived. In this paper, we clarify some discrepancies on the notions of reverse unit propagation (RUP) clauses and asymmetric tautologies (AT), and furthermore develop the concept of resolution consequences. This allows us to present an intuitive explanation of RAT in terms of permissive definitions. We prove that a formula derived using RATs can be stratified into clause sets depending on which definitions they require, which give a strong invariant along RAT proofs. We furthermore study its interaction with clause deletion, characterizing DRAT derivability as satisfiability-preservation.

• Tobias Philipp, Anna Tigunova. A Verified Decision Procedure for Pseudo-Boolean Formulas
  In: Proceedings of the 34th Workshop of the UK Planning and Scheduling Special Interest Group (PlanSIG) (2016)

  Pseudo-Boolean formulas frequently arise in planning, scheduling and optimization problems. We describe an efficient and easily verifiablede decision procedure for pseudo-Boolean formulas, that is based on encoding PB formulas into the propositional satisfiability problem with the cutting-edge sequential weighted counter encoding. State-of-the-art SAT solvers that emit unsatisfiability proofs are used to solve the resulting instances. The combination of a verified translation to SAT, and certified SAT solvers leads to a verified decision procedure for PB formulas. The verification of the encoding is carried out in the Coq proof assistant.

• Tobias Philipp. Unsatisfiability Proofs for Parallel SAT Solver Portfolios with Clause Sharing and Inprocessing
  In: Proceedings of the 2nd Global Conference on Artificial Intelligence (GCAI), EasyChair Publications (2016)

  State-of-the-art SAT solvers are highly tuned systematic-search procedures augmented with formula simplification techniques. They emit unsatisfiability proofs in the DRAT format to guarantee correctness of their answers. However, the DRAT format is inadequate to model some parallel SAT solvers such as the award-winning system plingeling. In plingeling, each solver in the portfolio applies clause addition and elimination techniques. Clause sharing is restricted to clauses that do not contain melted literals. In this paper, we develop a transition system that models the computation of such parallel portfolio solvers. The transition system allows us to formally reason about portfolio solvers, and we show that the formalism is sound and complete. Based on the formalism, we derive a new proof format, called parallel DRAT, which can be used to certify UNSAT answers.

• Tobias Philipp. An Expressive Model for Instance Decomposition Based Parallel SAT Solvers
  In: Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCos), pp. 101–116. Springer (2015)

  SAT solvers are highly efficient programs that decide the satisfiability problem for propositional formulas in conjunctive normal form. Contemporary SAT solvers combine many advanced techniques such as clause sharing and inprocessing. Clause sharing is a form of cooperation in parallel SAT solvers based on clause learning, whereas inprocessing simplifies formulas in a satisfiability-preserving way. In this paper, we present the instance decomposition formalism ID that models parallel SAT solvers with label-based clause sharing and inprocessing. We formally prove soundness of ID and show that the concept of labels can be used to ensure satisfiability-preserving operations. Moreover, we develop a new proof format for SAT solvers based on this approach, which is derived from ID.

• Norbert Manthey, Tobias Philipp. Checking Unsatisfiability Proofs in Parallel
  In: Proceedings of the Pragmatics of SAT (POS), pp. 34--49, EasyChair (2015)

  Contemporary SAT solvers emit unsatisfiability proofs in the DRAT format to increase confidence in their answers. The state-of-the-art proof verifier drat-trim uses backward- checking and deletion information to efficiently check unsatisfiability results. Checking large proofs still takes as long as solving a formula, and therefore parallelization seems to be a promising approach. However, Heule et al. stated that parallelization of the backward-checking procedure is difficult since clausal proofs do not include dependency information. In this paper, we present a parallelization approach and a prototypical implementation that scales reasonably compared to its sequential version.

• Tobias Philipp, Peter Steinke. PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF
  In: Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 9–16. Springer (2015)

  PBLib is an easy-to-use and efficient library, written in C++, for translating pseudo-Boolean (PB) constraints into CNF. We have implemented fifteen different encodings of PB constraints. Our aim is to use efficient encodings, in terms of formula size and whether unit propagation maintains generalized arc consistency. Moreover, PBLib normalizes PB constraints and automatically uses a suitable encoder for the translation. We also support incremental strengthening for optimization problems, where the tighter bound is realized with few additional clauses, as well as conditions for PB constraints.

• Norbert Manthey, Tobias Philipp, Peter Steinke. A More Compact Translation of Pseudo-Boolean Constraints into CNF Such That Generalized Arc Consistency Is Maintained
  In: Proceedings of the 37th Annual German Conference on AI (KI), pp. 123–134. Springer (2014)

  In this paper we answer the open question for the existence of a more compact encoding from Pseudo-Boolean constraints into CNF that maintains generalized arc consistency by unit propagation, formalized by Bailleux et al.. In contrast to other encodings our approach is defined in an abstract way and we present a concrete instantiation, resulting in a space complexity of \(\mathcal{O}(n^2 \text{log}^2(n)\text{log}(w_{\mathsf{max}}))\) clauses in contrast to \(\mathcal{O}(n^3 \text{log}(n)\text{log}(w_{\mathsf{max}}))\) clauses generated by the previously best known encoding that maintains generalized arc consistency.

• Mario Alviano, Carmine Dodaro, Johannes Klaus Fichte, Markus Hecher, Tobias Philipp, Jakob Rath.. Inconsistency Proofs for ASP: The ASP - DRUPE Format
  In: Theory and Practice of Logic Programming 19(5-6), pp. 891-907 (2019)

  Answer Set Programming (ASP) solvers are highly-tuned and complex procedures that implicitly solve the consistency problem, i.e., deciding whether a logic program admits an answer set. Verifying whether a claimed answer set is formally a correct answer set of the program can be decided in polynomial time for (normal) programs. However, it is far from immediate to verify whether a program that is claimed to be inconsistent, indeed does not admit any answer sets. In this paper, we address this problem and develop the new proof format ASP-DRUPE for propositional, disjunctive logic programs, including weight and choice rules. ASP-DRUPE is based on the Reverse Unit Propagation (RUP) format designed for Boolean satisfiability. We establish correctness of ASP-DRUPE and discuss how to integrate it into modern ASP solvers. Later, we provide an implementation of ASP-DRUPE into the wasp solver for normal logic programs.

• Mario Alviano, Carmine Dodaro, Johannes Klaus Fichte, Markus Hecher, Tobias Philipp, Jakob Rath. Inconsistency Proofs for ASP: The ASP - DRUPE Format
  In: CoRR (35th International Conference on Logic Programming) abs/1907.10389 (2019). (2019)

  ASP solvers are highly-tuned and complex procedures that implicitly solve the consistency problem, i.e., deciding whether an ASP program admits an answer set. Verifying whether a claimed answer set is formally a correct answer set of the program can be decided in polynomial time for normal programs. However, it is far from immediate to verify whether a program that is claimed to be inconsistent, indeed does not admit any answer sets. In this paper, we address this problem and develop the new proof format ASP-DRUPE for propositional, disjunctive ASP, including weights and optimization. ASP DRUPE is based on the RUP format designed for Boolean satisfiability. We establish correctness of ASP-DRUPE and discuss how to integrate it into modern ASP solvers.

• Emmanuelle-Anna Dietz Saldanha, Steffen Hölldobler, Tobias Philipp. Contextual Abduction and its Complexity Issues
  In: Proceedings of the 4th International Workshop on Defeasible and Ampliative Reasoning (DARe-17), pp. 58–70. CEUR-WS.org (2017)

  In everyday life, it seems that we prefer some explanations for an observation over others because of our contextual background knowledge. Reiter already tried to specify a mechanism within logic that allows us to avoid explicitly considering all exceptions in order to derive a conclusion w.r.t. the usual case. In a recent paper, a contextual reasoning approach has been presented, which takes this contextual background into account and allows us to specify contexts within the logic. This approach is embedded into the Weak Completion Semantics , a Logic Programming approach that aims at adequately modeling human reasoning tasks. As this approach extends the underlying three-valued Łukasiewicz logic, some formal properties of the Weak Completion Semantics do not hold anymore. In this paper, we investigate the effects of this extension and present some surprising results about the complexity issues of contextual abduction.

• Tobias Philipp, Anna Tigunova. A Verified Decision Procedure for Pseudo-Boolean Formulas
  In: Proceedings of the 34th Workshop of the UK Planning and Scheduling Special Interest Group (PlanSIG) (2016)

  Pseudo-Boolean formulas frequently arise in planning, scheduling and optimization problems. We describe an efficient and easily verifiablede decision procedure for pseudo-Boolean formulas, that is based on encoding PB formulas into the propositional satisfiability problem with the cutting-edge sequential weighted counter encoding. State-of-the-art SAT solvers that emit unsatisfiability proofs are used to solve the resulting instances. The combination of a verified translation to SAT, and certified SAT solvers leads to a verified decision procedure for PB formulas. The verification of the encoding is carried out in the Coq proof assistant.

• Tobias Sebastian Hahn, Norbert Manthey, Tobias Philipp. Solving the Module Game with SAT
  In: Benchmark Descriptions for the SAT Race (2015)

  We describe a CNF encoding of the Modulo game, acertain form of a combinatorial puzzle. To solve this game, tileshave to be placed on a field such that the sum of all overlayingvalues of a cell sums up to a multiple of a predefined value.We modify sorting networks to encode a modulo constraint fornumbers that are represented unary.

• Tobias Philipp. Clause Simplifications in Search-Space Decomposition-Based SAT Solvers
  In: Proceedings of the 7th European Starting AI Researcher Symposium (STAIRS), pp. 211–219. IOS Press (2014)

  Inprocessing is to apply clause simplification techniques during search and is a very attractive idea since it allows to apply computationally expensive techniques. In this paper we present the search space decomposition formalism SSD that models parallel SAT solvers with clause sharing and inprocessing. The main result of this paper is that the sharing model SSD is sound. In the formalism, we combine clause addition and clause elimination techniques, and it covers many SAT solvers such as PaSAT, PaMira, PMSat, MiraXT and ccc. Inprocessing is not used in these solvers, and we therefore propose a novel way how to combine clause sharing, search space decomposition and inprocessing.

• Norbert Manthey, Tobias Philipp. Formula Simplifications as DRAT Derivations
  In: Proceedings of the 37th Annual German Conference on AI (KI), pp. 111–122. Springer, 2014 (2014)

  Many real world problems are solved with satisfiability testing (SAT). However, SAT solvers have documented bugs and therefore the answer that a formula is unsatisfiable can be incorrect. Certifying algorithms are an attractive approach to increase the reliability of SAT solvers. For unsatisfiable formulas an unsatisfiability proof has to be created. This paper presents certificate constructions for various formula simplification techniques, which are crucial to the success of modern SAT solvers.

• Steffen Hölldobler, Norbert Manthey, Tobias Philipp, Peter Steinke. Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers
  In: Proceedings of the 1st Young Scientist’s Second International Workshop on Trends in Information Processing (YSIP), pp. 25–34. CEUR-WS.org (2014)

  Modern propositional satisfiability (or SAT) solvers are very powerful due to recent developments on the underlying data structures, the used heuristics to guide the search, the deduction techniques to in- fer knowledge, and the formula simplification techniques that are used during pre- and inprocessing. However, when all these techniques are put together, the soundness of the combined algorithm is not guaranteed any more. In this paper we present a small set of rules that allows to model modern SAT solvers in terms of a state transition system. With these rules all techniques which are applied in modern SAT solvers can be adequately modeled. Finally, we compare Generic CDCL with related systems.

• Tobias Philipp. MiPiSAT – Probing as Inprocessing in MiniSAT
  In: SAT Competition 2014 Solver and Benchmark Descriptions, pp. 49–50. University of Helsinki (2014)

  We submit the solver MIPISAT to the MiniSATHack-track: The solver extends MINISAT 2.2 by inprocessingcapabilities. In particular, we implemented failed literals andnecessary assignments as inprocessing. The technique is appliedon variables with high activity and therefore also exploitsinformation that is not available for preprocessors.

• Martin Philipp, Tobias Philipp. Solving Polarium Puzzles with SAT
  In: SAT Competition 2014 Solver and Benchmark Descriptions, pp. 96–97. University of Helsinki (2014)

  Polarium is a popular Nintendo DS puzzle consist-ing of a grid surrounded by a border. The task is to build a paththrough the puzzle, meeting the following conditions: 1. it mustnot cross itself, 2. it must be one single line, 3. for each row whichdoes not belong to the border, the path must contain either allwhite or all black cells. We submit CNF files to the application SAT+UNSAT track that encode the Polarium puzzle where weminimize the required time to enter the solution in the originalgame, and the required steps.

• Norbert Manthey, Tobias Philipp, Christoph Wernhard.. Soundness of Inprocessing in Clause Sharing SAT Solvers
  In: Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 22–39. Springer (2013)

  We present a formalism that models the computation of clause sharing portfolio solvers with inprocessing. The soundness o fthese solvers is not a straightforward property since shared clauses can make a formula unsatisfiable. Therefore, we develop characterizations of simplification techniques and suggest various settings how clause sharing and inprocessing can be combined. Our formalization models most of the recent implemented portfolio systems and we indicate possibilities to improve these. A particular improvement is a novel way to combine clause addition techniques - like blocked clause addition - with clause deletion techniques - like blocked clause elimination or variable elimination.

• Steffen Hölldobler, Tobias Philipp, Christoph Wernhard. An Abductive Model for Human Reasoning
  In: Proceedings of the AAAI Spring Symposium 2011 - Logical Formalizations of Com- monsense Reasoning, AAAI (2011)

  In this paper we contribute to bridging the gap between human reasoning as studied in Cognitive Science and commonsense reasoning based on formal logics and formal theories. In particular, the suppression task studied in Cognitive Science provides an interesting challenge problem for human reasoning based on logic. The work presented in the paper is founded on the recent approach by Stenning and van Lambalgen to model human reasoning by means of logic programs with a specific three-valued completion semantics and a semantic fixpoint operator that yields a least model, as well as abduction. Their approach has been subsequently made more precise and technically accurate by switching to three-valued Łukasiewicz logic. In this paper, we extend this refined approach by abduction. We show that the inclusion of abduction permits to adequately model additional empiric results reported from Cognitive Science. For the arising abductive reasoning tasks we give complexity results. Finally, we outline several open research issues that emerge from the application of logic to model human reasoning.

• Tobias Philipp and Adrian Rebola-Pardo. DRAT Proofs for XOR Reasoning
  In: Proceedings of the 15th European Conference on Logics in Artificial Intelligence (JELIA), pp. 415–429. Springer (2016)

  Unsatisfiability proofs in the DRAT format became the de facto standard to increase the reliability of contemporary SAT solvers. We consider the problem of generating proofs for the XOR reasoning component in SAT solvers and propose two methods: direct translation transforms every XOR constraint addition inference into a DRAT proof, whereas T-translation avoids the exponential blow-up in direct translations by using fresh variables. T-translation produces DRAT proofs from Gaussian elimination records that are polynomial in the size of the input CNF formula. Experiments show that a combination of both approaches with a simple prediction method outperforms the BDD-based method.

• Marijn Heule, Norbert Manthey, Tobias Philipp.. Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers.
  In: Proceedings of the Fifth Pragmatics of SAT workshop (POS) (2014)

  As satisfiability (SAT) solver performance has improved, so has their complexity, which make it more likely that SAT solvers contain bugs. One important source of increased complexity is clause sharing in parallel SAT solvers. SAT solvers can emit a proof of unsatisfiability to gain confidence that the their results are correct. Such proofs must contain deletion information in order to check them efficiently. Computing deletion information is easy and cheap for parallel solvers without clause sharing, but tricky for parallel solvers with clause sharing. We present a method to generate unsatisfiability proofs from clause sharing parallel SAT solvers. We show that the overhead of our method is small and that the produced proofs can be validated in a time similar to the solving (CPU) time. However, proofs produced by parallel solvers without clause sharing can be checked in a similar to the solving (wall-clock) time. This raises the question whether our method can be improved such that the checking time of proofs from parallel solvers without clause sharing is comparable to the time to check proofs from parallel solver with clause sharing.

• Steffen Hölldobler, Norbert Manthey, Tobias Philipp, Peter Steinke. Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers.
  In: Proceedings of Fifth Pragmatics of SAT workshop (POS) (2014)

  Modern propositional satisfiability (or SAT) solvers are very powerful due to recent developments on the underlying data structures, the used heuristics to guide the search, the deduction techniques to infer knowledge, and the formula simplification techniques that are used during pre- and inprocessing. However, when all these techniques are put together, the soundness of the combined algorithm is not guaranteed any more, and understanding the complex dependencies becomes non-trivial. In this paper we present a small set of rules that allows to model modern SAT solvers in terms of a state transition system. With these rules all techniques which are applied in modern SAT solvers can be modeled adequately. Furthermore, we show that this set of rules results is sound, complete and confluent. Finnaly, we compare the proposed transition system to related systems, and show how widely used solving techniques can be modeled.