wiki_research

personal research wiki
git clone https://a3nm.net/git/wiki_research/
Log | Files | Refs

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]