Autark assignments of Horn CNFs
- 64 Downloads
In this paper, we consider autark and linear autark assignments of Horn CNFs. We first study maximal autark assignments of Horn CNFs and devise a linear time algorithm of computing these assignments. This complements the previous work by Marek which reveals the properties of minimal autark assignments of Horn CNFs. We then consider linear autark assignments of Horn CNFs and give a combinatorial characterization of the existence of such an assignment. By making use of this characterization, we devise a linear time algorithm of finding linear autark assignments of Horn CNFs.
KeywordsBoolean satisfiability problem Autark assignment Horn CNF Combinatorial algorithm
Mathematics Subject Classification68W99 90C99
The authors thank Professor Toshihiro Fujito for his valuable comments on the presentation of the manuscript. The authors are indebted to the reviewers for their valuable comments and suggestions, which have considerably improved the presentation of the results. The first author is supported by JSPS KAKENHI Grant number JP15H06286 and JST ERATO Grant number JPMJER1201, Japan. The second author is supported by JSPS KAKENHI Grant number JP24106002, JP25280004, JP26280001, and JST CREST Grant number JPMJCR1402, Japan.
- 8.Hooker, J.: Optimization methods in logic. In: Crama, Y., Hammer, P.L. (eds.) Boolean Models and Methods in Mathematics, Computer Science, and Engineering. Cambridge University Press, Cambridge (2010)Google Scholar