#automated-reasoning2 articles

2 articles

AINeutralarXiv – CS AI · 6h ago1

🧠

Approximate SMT Counting Beyond Discrete Domains

Researchers introduce pact, a new SMT model counter that can handle hybrid formulas containing both discrete and continuous variables using hashing-based approximate counting. The tool significantly outperforms existing baselines, successfully processing 456 out of 3119 test instances compared to only 83 for the baseline method.

AINeutralarXiv – CS AI · 6h ago1

🧠

A Reduction of Input/Output Logics to SAT

Researchers have developed an automation approach for Input/Output (I/O) Logics, a type of deontic logic used for reasoning about norms and obligations, by reducing them to propositional satisfiability problems. A prototype implementation called 'rio' (reasoner for input/output logics) has been created to demonstrate these procedures with practical examples.