Skip to main content
Top

2021 | OriginalPaper | Chapter

Tree-Like Unit Refutations in Horn Constraint Systems

Authors : K. Subramani, Piotr Wojciechowski

Published in: Language and Automata Theory and Applications

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In this paper, we examine the problem of finding unit refutations of Horn constraint systems (HCSs). Recall that a Horn constraint is a linear constraint in which every coefficient belongs to the set \(\{0,1,-1\}\) and in which at most one coefficient is positive. In the current work, we extend the notion of unit refutations from CNF formulas to systems of linear constraints. Recall that for CNF formulas a unit resolution refutation is one in which every resolution step uses a one-literal (unit) clause. The equivalent notion in linear systems requires every inference step to use a one-variable (absolute) constraint. We analyze two problems associated with unit refutations of Horn constraint systems. In the length-bounded tree-like unit refutation (TLUR\(_{D}\)) problem, we ask if a given Horn constraint system has a tree-like unit refutation using at most L inference steps. In the optimal tree-like unit refutation (TLUR\(_{Opt}\)) problem, we ask for a tree-like unit refutation with the fewest inference steps. We show that the former problem is NP-complete and the latter is NPO-complete. We also show that the TLUR\(_{D}\) problem does not admit a polynomial size kernel with respect to a natural output parameter under some well-accepted complexity theoretic assumptions.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
1.
go back to reference Ausiello, G., D’Atri, A., Protasi, M.: Lattice theoretic ordering properties for NP-complete optimization problems. Fundam. Informaticae 4(1), 83–94 (1981)MathSciNetMATH Ausiello, G., D’Atri, A., Protasi, M.: Lattice theoretic ordering properties for NP-complete optimization problems. Fundam. Informaticae 4(1), 83–94 (1981)MathSciNetMATH
2.
go back to reference Baumgartner, P.: Linear and unit-resulting refutations for horn theories. J. Autom. Reason. 16(3), 241–319 (1996)MathSciNetCrossRef Baumgartner, P.: Linear and unit-resulting refutations for horn theories. J. Autom. Reason. 16(3), 241–319 (1996)MathSciNetCrossRef
3.
go back to reference Chandrasekaran, R., Subramani, K.: A combinatorial algorithm for Horn programs. Discrete Optim. 10, 85–101 (2013)MathSciNetCrossRef Chandrasekaran, R., Subramani, K.: A combinatorial algorithm for Horn programs. Discrete Optim. 10, 85–101 (2013)MathSciNetCrossRef
4.
go back to reference Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977) Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)
5.
go back to reference de Moura,L., Owre, S., Ruess, H., Rushby, J.M., Shankar, N.: The ICS decision procedures for embedded deduction. In: IJCAR, pp. 218–222 (2004) de Moura,L., Owre, S., Ruess, H., Rushby, J.M., Shankar, N.: The ICS decision procedures for embedded deduction. In: IJCAR, pp. 218–222 (2004)
6.
go back to reference Duterre, B., de Moura, L.: The yices SMT solver. Technical report, SRI International (2006) Duterre, B., de Moura, L.: The yices SMT solver. Technical report, SRI International (2006)
7.
go back to reference Farkas, G.: Über die Theorie der Einfachen Ungleichungen. Journal für die Reine und Angewandte Mathematik 124(124), 1–27 (1902)MathSciNetMATH Farkas, G.: Über die Theorie der Einfachen Ungleichungen. Journal für die Reine und Angewandte Mathematik 124(124), 1–27 (1902)MathSciNetMATH
8.
go back to reference Fomin, F.V., Lokshtanov, D., Saurabh, S., Zehavi, M.: Theory of Parameterized Preprocessing. Cambridge University Press, Kernelization (2019)MATH Fomin, F.V., Lokshtanov, D., Saurabh, S., Zehavi, M.: Theory of Parameterized Preprocessing. Cambridge University Press, Kernelization (2019)MATH
9.
go back to reference Ford, J., Shankar, N.: Formal verification of a combination decision procedure. In: CADE, pp. 347–362 (2002) Ford, J., Shankar, N.: Formal verification of a combination decision procedure. In: CADE, pp. 347–362 (2002)
10.
11.
go back to reference Kann, V.: On the Approximability of NP-complete Optimization Problems. Ph.D. thesis, Royal Institute of Technology Stockholm (1992) Kann, V.: On the Approximability of NP-complete Optimization Problems. Ph.D. thesis, Royal Institute of Technology Stockholm (1992)
12.
go back to reference Komuravelli, A., Bjørner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In: Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, 27–30 September 2015, pp. 89–96 (2015) Komuravelli, A., Bjørner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In: Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, 27–30 September 2015, pp. 89–96 (2015)
13.
go back to reference Lueker, G.S.: Two NP-complete Problems in Nonnegative Integer Programming. Princeton University, Department of Electrical Engineering (1975) Lueker, G.S.: Two NP-complete Problems in Nonnegative Integer Programming. Princeton University, Department of Electrical Engineering (1975)
14.
go back to reference Neiman, V.S.: Refutation search for horn sets by a subgoal-extraction method. J. Log. Program. 9(2&3), 267–284 (1990)MathSciNetCrossRef Neiman, V.S.: Refutation search for horn sets by a subgoal-extraction method. J. Log. Program. 9(2&3), 267–284 (1990)MathSciNetCrossRef
15.
go back to reference Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, New York (1987)MATH Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, New York (1987)MATH
16.
go back to reference Subramani, K.: Optimal length resolution refutations of difference constraint systems. J. Autom. Reason. (JAR) 43(2), 121–137 (2009)MathSciNetCrossRef Subramani, K.: Optimal length resolution refutations of difference constraint systems. J. Autom. Reason. (JAR) 43(2), 121–137 (2009)MathSciNetCrossRef
17.
go back to reference Subramani, K., Wojciechowki, P.: A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints. Algorithmica 81(7), 2765–2794 (2019)MathSciNetCrossRef Subramani, K., Wojciechowki, P.: A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints. Algorithmica 81(7), 2765–2794 (2019)MathSciNetCrossRef
18.
go back to reference Veinott, A.F., LiCalzi, M.: Subextremal functions and lattice programming, July 1992. Unpublished Manuscript Veinott, A.F., LiCalzi, M.: Subextremal functions and lattice programming, July 1992. Unpublished Manuscript
19.
go back to reference Wojciechowski, P., Subramani, K.: A certifying algorithm for checking for the presence of unit refutations in horn constraint systems. European Symposium on Programming (Submitted) Wojciechowski, P., Subramani, K.: A certifying algorithm for checking for the presence of unit refutations in horn constraint systems. European Symposium on Programming (Submitted)
20.
go back to reference Yap, C.K.: Some consequences of non-uniform conditions on uniform classes. Theor. Comput. Sci. 26(3), 287–300 (1983)CrossRef Yap, C.K.: Some consequences of non-uniform conditions on uniform classes. Theor. Comput. Sci. 26(3), 287–300 (1983)CrossRef
Metadata
Title
Tree-Like Unit Refutations in Horn Constraint Systems
Authors
K. Subramani
Piotr Wojciechowski
Copyright Year
2021
DOI
https://doi.org/10.1007/978-3-030-68195-1_18

Premium Partner