Online Judge | Problem Set | Authors | Online Contests | User | ||||||
---|---|---|---|---|---|---|---|---|---|---|

Web Board Home Page F.A.Qs Statistical Charts | Current Contest Past Contests Scheduled Contests Award Contest |

Language: Horn Clauses
Description Consider some set of boolean variables and a boolean formula. A set of values for the variables is called In general, there is no known algorithm finding the satisfying set of values in polynomial time, although it is not yet proved that such algorithm does not exist. The same holds for determining whether the given formula is unsatisfiable. Despite this there are some particular classes of boolean formulae for which the problem of satisfiability and unsatisfiability can be solved in polynomial time. Now we will define one of such classes, and your task will be to create polynomial time algorithm for it. A Consider some Horn clause ¬ p. It would be more convenient to replace disjunctions with implication: (n_{1}∧n_{2}∧…∧n)⇒_{k}p.For consistency, when Consider a formula which is a conjunction of one or more Horn clauses. In this particular case, satisfiability and unsatisfiability problems can be solved by polynomial time algorithms. Write a program that would do it. Input The file consists of formulae, written according to the following BNF. Here [‹expression›] means that expression may be omitted, {‹expression›} means that expression may occur zero or more times. Characters in quotes denote themselves.
Each formula is specified in a separate line. The total length of the input file does not exceed 20 000 characters. Output Your output must contain either the set of variables with their values that satisfy the corresponding formulae, or word “ Sample Input (A&B&C=>QQQQ)&(=>A) (A=>)&(=>A) Sample Output A=true,C=false,B=false,QQQQ=false unsatisfiable Source Northeastern Europe 2005, Northern Subregion |

[Submit] [Go Back] [Status] [Discuss]

All Rights Reserved 2003-2013 Ying Fuchen,Xu Pengcheng,Xie Di

Any problem, Please Contact Administrator