Design Space Exploration as Quantified Satisfaction
We present novel algorithms for design and design space exploration. The designs discovered by these algorithms are compositions of function types specified in component libraries. Our algorithms reduce the design problem to quantified satisfiability and use advanced solvers to find solutions that represent useful systems. The algorithms we present in this paper are sound and complete and are guaranteed to discover correct designs of optimal size, if they exist. We apply our method to the design of Boolean systems and discover new and more optimal classical digital and quantum circuits for common arithmetic functions such as addition and multiplication. The performance of our algorithms is evaluated through extensive experimentation. We created a benchmark consisting of specifications of scalable synthetic digital circuits and real-world mirochips. We have generated multiple circuits functionally equivalent to the ones in the benchmark. The quantified satisfiability method shows more than four orders of magnitude speed-up, compared to a generate and test method that enumerates all non-isomorphic circuit topologies. Our approach generalizes circuit optimization. It uses arbitrary component libraries and has applications to areas such as digital circuit design, diagnostics, abductive reasoning, test vector generation, and combinatorial optimization.
Code (0)
등록된 구현이 없습니다.
Tasks
Combinatorial OptimizationSimilar Papers 제목 키워드 기반
Quantified Constraint Handling Rules
We shift the QCSP (Quantified Constraint Satisfaction Problems) framework to the QCHR (Quantified Constraint Handling Rules) framework by enabling dynamic binder and access to user-defined constraints. QCSP offers a natu…
Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction
We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a first-order sentence (not assumed here to be in prenex form) built from conjunction and quantification, whethe…
FormSentenceAutomatic Exploration Process Adjustment for Safe Reinforcement Learning with Joint Chance Constraint Satisfaction
In reinforcement learning (RL) algorithms, exploratory control inputs are used during learning to acquire knowledge for decision making and control, while the true dynamics of a controlled object is unknown. However, thi…
Decision MakingObjectreinforcement-learningReinforcement Learning (RL)+1Solving QSAT problems with neural MCTS
Recent achievements from AlphaZero using self-play has shown remarkable performance on several board games. It is plausible to think that self-play, starting from zero knowledge, can gradually approximate a winning strat…
Board GamesGraph Neural NetworkAn Empirical Analysis on Transparent Algorithmic Exploration in Recommender Systems
All learning algorithms for recommendations face inevitable and critical trade-off between exploiting partial knowledge of a user's preferences for short-term satisfaction and exploring additional user preferences for lo…
Recommendation Systems