Thu, 22 Jan 2026 14:15:15 (Big Ben's timeline)    

 IE 6+   Safari 3+   Opera 9+   Firefox 2+   Chrome+ 

• Reduction of SAT to Horn-SAT
  Coming soon...
• Sudoku Solver
  Demo for presentation on WCECS 2009.
  The articles describe a Sudoku solver based on a reduction of the puzzle to Horn SAT. The reduction uses the compatibility matrix method. The fast browsers are recommended (IE is not recommended).
• Linear model for SAT
  Demo for articles arXiv:0802.2612v2 [cs.DM] and in CS Digital Library.
  The articles describe a O(n⁴)-time reduction of SAT to an asymmetric O(n⁴)-size linear system using the compatibility matrix encoding, where n is the total of literals in all clauses. The encoding maps the conjunctions in that DF, which would be obtained from the given CNF using distributive laws, onto vertices of a polytope. The model actually maps the places in that DF. So, the polytope's form and location depend on order of clauses in the given CNF and on order of literals in the clauses.
• Subgraph Isomorphism
  Demo for articles arXiv:0802.2612v2 [cs.DM] and arXiv:cs/0610042v3 [cs.DM]
  The articles describe a O(n⁴)-time reduction of Subgraph Isomorphism Problem in (multi) digraphs with (multi) loops to an asymmetric O(n⁴)-size linear system using the compatibility matrix encoding, where n is the number of vertices.
• 3SAT Solver (The asynchronous algorithm)
  Demo for aticles arXiv:cs/0701023 [cs.CC] and arXiv:cs/0703146v3 [cs.CC].
  The algorithm encodes 3SAT instances in the contradictions between true assignments for separate clauses. The encoding is called a compatibility matrix. The algorithm is a dynamic programming procedure which performs parallel testing of all guesses and transforms that matrix into a compatibility matrix encoding of satisfying true-assignments. Computational complexity of the algorithm is O(m³), where m is the number of clauses.
• 3SAT Solver (The basic algorithm)
  Demo for article arXiv:cs/0701023 [cs.CC].
  The algorithm encodes 3SAT instances in the contradictions between true assignments for separate clauses. The encoding is called a compatibility matrix. The algorithm is a dynamic programming procedure which performs parallel testing of all guesses and transforms that matrix into a compatibility matrix encoding of satisfying true-assignments. Computational complexity of the algorithm is O(m⁵), where m is the number of clauses.
• Pending...