satisfiability (973B)
1 # Satisfiability 2 3 The *satisfiability problem* is a [decision_problem] in [logic]: given a [logical_theory], decide if it has a [model] 4 5 - [first_order_logic] with two variables is decidable also with equality, cf <www.cs.rice.edu/~vardi/papers/dimacs96.ps.gz>, page 10 6 - on trees with ancestor/descendant, difficult [open_problems], cf [bojanczyk2006two] 7 - [vector_addition_tree_automata] ([degroote2004vector]), like [vector_addition_system] 8 - [kontchakov2005undecidability]: [first_order_logic] with three variables is [undecidable] even without [constants] or [equality] 9 - [david2010satisfiability] bottom of p10: even on [data_trees] 10 - [satisfiability_boolean] 11 - [satisfiability_cnf] 12 - [QBF]: http://www.qbflib.org/ 13 - [satisfiability_weighted] 14 15 Tools: [sat_solver] 16 17 See also: [strong_exponential_time_hypothesis], [satisfiability_boolean], [tautology], [automaton_emptiness], [satisfiability_modulo_theory], [equisatisfiability] 18 19 Up: [computational_problem]